How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Adjoining one root need not split the polynomial: does not split
Statement refuted
If a field is obtained by adjoining one root of a polynomial, then the polynomial splits over that field.
Facts & Assumptions
Given: The real root of and the field .
For and , the roots of are (The splitting field of over is with ).
The real numbers form an ordered field, and the complex numbers have unique coordinates over (The reals form a totally ordered field, is a field, every element is uniquely , and every nonzero element has inverse ).
Counterexample
The positive real number is a root of , and every element of is real because it is obtained from rational numbers and by field operations inside .
In [F1], the imaginary part of is , while direct multiplication gives the imaginary part of as . Since , the roots and are both nonreal and hence neither lies in .
Therefore contains one root but not all roots of , so the polynomial does not split there.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 73 results over 17 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- T. Judson, Abstract Algebra: Theory and Applications, Example 21.15 (standard reference, not scraped)