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.
has Galois group over
Example
The polynomial has Galois group over .
Facts & Assumptions
Given: The reduction-modulo-a-prime irreducibility test (Irreducibility after reduction modulo a prime implies irreducibility over when the leading coefficient survives), the rational-root theorem (Rational root theorem), and the resolvent formula of The coefficient formula and discriminant of the quartic resolvent.
A monic irreducible separable quartic over a field of characteristic not two, with irreducible resolvent cubic and nonsquare discriminant, has Galois group (The five-case resolvent classification of an irreducible quartic Galois group).
An irreducible polynomial is separable if and only if its derivative is nonzero (An irreducible polynomial over a field is separable exactly when its derivative is nonzero).
Verification
Modulo the polynomial is . It has no root in , and the only irreducible quadratic does not divide it, so the reduction is irreducible. The reduction test makes irreducible over .
The resolvent formula gives . Its only possible rational roots are and , neither of which is a root, so the resolvent cubic is irreducible.
The discriminant is the resolvent discriminant , a negative nonsquare in and in particular nonzero.
The derivative of is , a nonzero element of , and has characteristic zero, hence not two.
Steps 1.1 and 1.4 with [L2] make separable. The hypotheses of [L1] are then supplied by steps 1.1, 1.2, 1.3, and 1.4, so the Galois group is .
Depends on
- Irreducibility after reduction modulo a prime implies irreducibility over $\mathbb Q$ when the leading coefficient survives
- Rational root theorem
- The coefficient formula and discriminant of the quartic resolvent
- An irreducible polynomial over a field is separable exactly when its derivative is nonzero
- The five-case resolvent classification of an irreducible quartic Galois group
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
28 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
- K. Conrad, Galois Groups of Cubics and Quartics, Example 3.2 (standard reference, not scraped)