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.
In characteristic , every irreducible polynomial is uniquely with irreducible and separable
Statement
Let have characteristic and let be nonconstant and irreducible. There are unique and such that
is irreducible and separable, and is maximal with this property. The case occurs exactly when is separable.
Facts & Assumptions
Given: A field of characteristic and a nonconstant irreducible polynomial .
A nonzero polynomial is separable exactly when it is coprime to its formal derivative (A nonzero polynomial over a field is separable exactly when its gcd with its derivative is ).
In characteristic , Frobenius is an injective endomorphism and (Frobenius is an injective endomorphism in characteristic , and an automorphism for finite fields).
Every nonzero nonunit polynomial over a field factors into irreducibles (Every nonzero nonunit polynomial over a field factors into irreducible polynomials).
Proof
The derivative is zero exactly when every exponent occurring in is divisible by ; in that case there is a unique with . Repeating this finite descent in degree gives a unique maximal and a polynomial with and .
If with both factors nonconstant, then , contradicting irreducibility of ; hence is irreducible.
Since , any nonunit common divisor of and has an irreducible factor by [L3], which would divide the irreducible and hence force , impossible by degree; thus and [L1] makes separable.
The exponents occurring in determine their largest common power , so and then the coefficient-preserving core are unique. Moreover exactly when , which for irreducible is equivalent to separability by [L1].
Depends on
Used by
- If a is not a pth power in a characteristic-p field, then x^pⁿ-a is irreducible for every n≥1 Lemma
- A field is perfect exactly when it has characteristic zero or its Frobenius map is surjective Theorem
- An algebraic extension is purely inseparable over its separable closure Theorem
- Pure inseparability and its conjugate, embedding, and separable-degree criteria Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 66 results over 12 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
- P. L. Clark, Field Theory, Chapters 3 to 5 (standard reference, not scraped)
- J. S. Milne, Fields and Galois Theory, Chapters 2, 3, and 5 (standard reference, not scraped)