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.
Repeated roots in extension fields and separable polynomials
Definition
Let be a field, let be an extension field in which is a subfield (Subfield: a subring of a field closed under inverses of its nonzero elements, and therefore a field with the restricted operations), and let . The coefficient inclusion induces a homomorphism by the universal property (Universal property of : a coefficient homomorphism and the image of determine a unique ring homomorphism).
An element is a repeated root of in when divides the image of in . It is a root in the ordinary sense of Evaluation and roots of a polynomial in a commutative target ring, and Factor theorem over a commutative ring identifies divisibility by with vanishing at .
The polynomial is separable over when it has no repeated root in any extension field of . A nonzero constant polynomial is therefore separable. The zero polynomial is not called separable under this convention.
Depends on
- Subfield: a subring of a field closed under inverses of its nonzero elements, and therefore a field with the restricted operations
- Evaluation and roots of a polynomial in a commutative target ring
- Factor theorem over a commutative ring
- Universal property of $R[x]$: a coefficient homomorphism and the image of $x$ determine a unique ring homomorphism
Used by
- Perfect fields: every irreducible polynomial is separable Definition
- Semisimple endomorphisms as endomorphisms diagonalisable over an algebraic closure, and nilpotent endomorphisms Definition
- Separable algebraic elements and separable extensions Definition
- Over F₂, x⁴+x²+1=(x²+x+1)² has two distinct roots, each repeated, in its four-element splitting field Example
- If p is a prime not dividing n, a rational minimal polynomial of a primitive n-th root of unity also kills its p-th power Lemma
- A root is repeated exactly when it is also a root of the formal derivative Theorem
- For gcd(n,q)=1 the reduction of Φₙ in F_q[t] is a product of distinct monic irreducibles, each of degree the order of [q] modulo n Theorem
- K(μₘ)K(μₙ)=K(μ_lcm(m,n)) Theorem
- Over a field whose characteristic does not divide n, the roots of Φₙ are exactly the primitive roots of unity Theorem
- The recursion defines a unique monic Φₙ∈ℤ[t], of degree φ(n) Theorem
- tⁿ-1 is separable over K exactly when the characteristic does not divide n, and then a splitting field carries n distinct n-th roots of unity Theorem
Dependency tree · two levels
18 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Brian Conrad, Differential Criterion and Primitivity, Section 1 (standard reference, not scraped)