QuadraticDiscriminant.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

6 declarations, 0 contain sorry, 0 declared as axioms

Separability and splitting criteria for quadratic polynomials

Proposed new Mathlib file Mathlib.Algebra.Polynomial.QuadraticDiscriminant: a quadratic over a field is separable iff its discriminant is nonzero, and splits iff its discriminant is a square (in characteristic 2: iff its Artin–Schreier invariant is in the image of z ↦ z² + z).

Imports (3)

Imported by 2 files

theorem Polynomial.derivative_quadratic The derivative of the quadratic a X² + b X + c is 2 a X + b line 26 source
Source documentation
The derivative of the quadratic a X² + b X + c is 2 a X + b.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommSemiring, Eq, Polynomial, LinearMap, RingHom.id, Polynomial.derivative, HAdd.hAdd, HMul.hMul, RingHom, Polynomial.C, HPow.hPow, Nat, Polynomial.X, OfNat.ofNat
Proof uses: Eq.mpr, id, congrFun', congrArg, Eq.trans, Polynomial.derivative_add, congr, Polynomial.derivative_mul, Polynomial.derivative_C, MulZeroClass.zero_mul, Polynomial.derivative_X_pow_succ, Nat.cast_one, map_add, map_one, pow_one, zero_add, Polynomial.derivative_X, mul_one, add_zero, Mathlib.Tactic.Ring.of_eq and 24 more
74 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem derivative_quadratic {R : Type*} [CommSemiring R] (a b c : R) :
    derivative (C a * X ^ 2 + C b * X + C c) = 2 * C a * X + C b := by
…
```
theorem Polynomial.sq_derivative_quadratic_sub_mul The Bézout-type identity (P')² - 4 a · P = C (b² - 4 a c) for the quadratic P = a X² + b X + c: the discriminant is an explicit combination of P and its derivative line 33 source
Source documentation
The Bézout-type identity (P')² - 4 a · P = C (b² - 4 a c) for the quadratic P = a X² + b X + c: the discriminant is an explicit combination of P and its derivative.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Eq, Polynomial, HSub.hSub, HPow.hPow, Nat, LinearMap, RingHom.id, Polynomial.derivative, HAdd.hAdd, HMul.hMul, RingHom, Polynomial.C, Polynomial.X, OfNat.ofNat
Proof uses: Eq.mpr, id, congrArg, Polynomial.derivative_quadratic, Eq.trans, map_sub, congr, map_pow, map_mul, congrFun', map_ofNat, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.pow_congr, Mathlib.Tactic.Ring.Common.add_congr and 51 more
94 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem sq_derivative_quadratic_sub_mul {R : Type*} [CommRing R] (a b c : R) :
    derivative (C a * X ^ 2 + C b * X + C c) ^ 2
      - 4 * C a * (C a * X ^ 2 + C b * X + C c) = C (b ^ 2 - 4 * a * c) := by
…
```
theorem Polynomial.separable_quadratic_iff A quadratic polynomial a X² + b X + c (with a ≠ 0) over a field is separable exactly when its discriminant b² - 4 a c is nonzero line 45 source
Source documentation
A quadratic polynomial a X² + b X + c (with a ≠ 0) over a field is separable exactly when its discriminant b² - 4 a c is nonzero. The ← direction holds in every characteristic: by the Bézout identity sq_derivative_quadratic_sub_mul, a nonzero (hence invertible) discriminant exhibits P and P' as coprime. The → direction argues that if the discriminant vanishes then P ∣ (P')², forcing the coprimality witness P to be a unit, contradicting deg P = 2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Ne, OfNat.ofNat, Iff, Polynomial.Separable, HAdd.hAdd, Polynomial, HMul.hMul, RingHom, Polynomial.C, HPow.hPow, Nat, Polynomial.X, HSub.hSub
Proof uses: Eq.mpr, id, Eq, congrArg, rfl, LinearMap, RingHom.id, Polynomial.derivative, Polynomial.sq_derivative_quadratic_sub_mul, Iff.intro, Dvd.dvd, Exists.intro, Mathlib.Tactic.LinearCombination.eq_of_eq, Eq.mp, map_zero, Mathlib.Tactic.LinearCombination.eq_rearrange, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.sub_congr, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr and 75 more
136 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
theorem separable_quadratic_iff {k : Type*} [Field k] {a b c : k} (ha : a ≠ 0) :
    (C a * X ^ 2 + C b * X + C c).Separable ↔ b ^ 2 - 4 * a * c ≠ 0 := by
…
```
theorem Polynomial.splits_quadratic_iff_exists_root A quadratic a X² + b X + c (a ≠ 0) over a field splits exactly when it has a root (Splits.of_natDegree_le_two_of_isRoot) line 66 source
Source documentation
A quadratic a X² + b X + c (a ≠ 0) over a field splits exactly when it has a root (Splits.of_natDegree_le_two_of_isRoot). This is the characteristic-free core of the split criterion.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Ne, OfNat.ofNat, Iff, Polynomial.Splits, HAdd.hAdd, Polynomial, HMul.hMul, RingHom, Polynomial.C, HPow.hPow, Nat, Polynomial.X, Exists, Eq
Proof uses: Eq.mpr, id, congrArg, rfl, Polynomial.natDegree, Polynomial.natDegree_quadratic, False.elim, False, Eq.mp, Eq.trans, congrFun', Iff.intro, Polynomial.eval, Polynomial.Splits.exists_eval_eq_zero, of_eq_true, WithBot, Polynomial.degree, True, Polynomial.degree_eq_natDegree, Not and 64 more
87 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
theorem splits_quadratic_iff_exists_root {k : Type*} [Field k] {a b c : k} (ha : a ≠ 0) :
    (C a * X ^ 2 + C b * X + C c).Splits ↔ ∃ x, a * x ^ 2 + b * x + c = 0 := by
…
```
theorem Polynomial.splits_quadratic_iff Documented declaration: splits_quadratic_iff line 86 source
Source documentation
Over a field of characteristic ≠ 2, a quadratic a X² + b X + c (with a ≠ 0) splits exactly when its discriminant b² - 4 a c is a square: it splits iff it has a root (splits_quadratic_iff_exists_root), and completing the square (discrim_eq_sq_of_quadratic_eq_zero / exists_quadratic_eq_zero) matches roots with square roots of the discriminant. This is the split-multiplicative-reduction criterion; compare separable_quadratic_iff (separable ↔ discriminant nonzero).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NeZero, OfNat.ofNat, Nat, Ne, Iff, Polynomial.Splits, HAdd.hAdd, Polynomial, HMul.hMul, RingHom, Polynomial.C, HPow.hPow, Polynomial.X, IsSquare, discrim
Proof uses: Eq.mpr, Exists, Eq, id, congrArg, propext, Polynomial.splits_quadratic_iff_exists_root, Iff.intro, Exists.intro, discrim_eq_sq_of_quadratic_eq_zero, Mathlib.Tactic.LinearCombination.eq_of_eq, Mathlib.Tactic.LinearCombination.eq_rearrange, Mathlib.Tactic.Ring.of_eq, HSub.hSub, Mathlib.Tactic.Ring.Common.sub_congr, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl and 56 more
83 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
theorem splits_quadratic_iff {k : Type*} [Field k] [NeZero (2 : k)] {a b c : k} (ha : a ≠ 0) :
    (C a * X ^ 2 + C b * X + C c).Splits ↔ IsSquare (discrim a b c) := by
…
```
theorem Polynomial.splits_quadratic_iff_of_two_eq_zero Documented declaration: splits_quadratic_iff_of_two_eq_zero line 102 source
Source documentation
Over a field of characteristic 2, a separable quadratic a X² + b X + c (a, b ≠ 0) splits exactly when its Artin–Schreier invariant a c / b² lies in the image of z ↦ z² + z, written division-free as ∃ z, b² (z² + z) = a c. (Substitute z = a x / b in a root x.) In residue characteristic 2 this replaces the square-class criterion splits_quadratic_iff, since there b² - 4 a c = b², so separability already forces b ≠ 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Eq, OfNat.ofNat, Nat, Ne, Iff, Polynomial.Splits, HAdd.hAdd, Polynomial, HMul.hMul, RingHom, Polynomial.C, HPow.hPow, Polynomial.X, Exists
Proof uses: Eq.mpr, id, congrArg, propext, Polynomial.splits_quadratic_iff_exists_root, Iff.intro, Exists.intro, HDiv.hDiv, inferInstance, CommGroupWithZero, Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq, Mathlib.Tactic.FieldSimp.NF.eval, Mathlib.Tactic.FieldSimp.NF.cons, Prod.mk, Int, List.nil, Prod, Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul, Eq.trans, congr_arg₂ and 94 more
110 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
theorem splits_quadratic_iff_of_two_eq_zero {k : Type*} [Field k] (h2 : (2 : k) = 0)
    {a b c : k} (ha : a ≠ 0) (hb : b ≠ 0) :
    (C a * X ^ 2 + C b * X + C c).Splits ↔ ∃ z, b ^ 2 * (z ^ 2 + z) = a * c := by
…
```