Quadratic.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

7 declarations, 0 contain sorry, 0 declared as axioms

Trace and norm in a separable quadratic extension

Proposed new Mathlib file Mathlib.RingTheory.Norm.Quadratic: trace and norm via the nontrivial automorphism of a separable quadratic extension.

Imports (3)

Imported by 2 files

theorem Algebra.IsQuadraticExtension.algebraMap_trace_eq_add In a separable quadratic extension, the trace of x is x + σx, where σ is the nontrivial automorphism line 30 source
Source documentation
In a separable quadratic extension, the trace of x is x + σx, where σ is the nontrivial automorphism.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, AlgEquiv, Ne, OfNat.ofNat, Eq, RingHom, Algebra.algebraMap, LinearMap, RingHom.id, Algebra.trace, HAdd.hAdd
Proof uses: Eq.mpr, Finset.sum, Finset.univ, id, congrArg, trace_eq_sum_automorphisms, Insert.insert, Finset, Classical.propDecidable, Singleton.singleton, Algebra.IsQuadraticExtension.univ_algEquiv, Finset.sum_pair, Ne.symm, of_eq_true, eq_self
63 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem Algebra.IsQuadraticExtension.algebraMap_trace_eq_add {σ : L ≃ₐ[K] L} (hσ : σ ≠ 1)
    (x : L) : algebraMap K L (Algebra.trace K L x) = x + σ x := by
…
```
theorem Algebra.IsQuadraticExtension.algebraMap_norm_eq_mul In a separable quadratic extension, the norm of x is x * σx, where σ is the nontrivial automorphism line 38 source
Source documentation
In a separable quadratic extension, the norm of x is x * σx, where σ is the nontrivial automorphism.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, AlgEquiv, Ne, OfNat.ofNat, Eq, RingHom, Algebra.algebraMap, MonoidHom, Algebra.norm, HMul.hMul
Proof uses: Eq.mpr, Finset.prod, Finset.univ, id, congrArg, Algebra.norm_eq_prod_automorphisms, Insert.insert, Finset, Classical.propDecidable, Singleton.singleton, Algebra.IsQuadraticExtension.univ_algEquiv, Finset.prod_pair, Ne.symm, of_eq_true, eq_self
65 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem Algebra.IsQuadraticExtension.algebraMap_norm_eq_mul {σ : L ≃ₐ[K] L} (hσ : σ ≠ 1)
    (x : L) : algebraMap K L (Algebra.norm K x) = x * σ x := by
…
```
theorem Algebra.IsQuadraticExtension.trace_algebraMap_add_algebraMap_mul The trace of b + aθ in a separable quadratic extension is a·tr(θ) + 2b line 45 source
Source documentation
The trace of b + aθ in a separable quadratic extension is a·tr(θ) + 2b.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, Eq, LinearMap, RingHom.id, Algebra.trace, HAdd.hAdd, RingHom, Algebra.algebraMap, HMul.hMul, OfNat.ofNat, Nat
Proof uses: AlgEquiv, Ne, Exists, Algebra.IsQuadraticExtension.exists_algEquiv_ne_one, FaithfulSMul.algebraMap_injective, Eq.mpr, id, congr, congrArg, Eq.trans, map_add, Algebra.IsQuadraticExtension.algebraMap_trace_eq_add, AlgEquiv.commutes, map_mul, MonoidHom.id, congrFun', map_ofNat, Mathlib.Tactic.Ring.of_eq, HPow.hPow, Nat.rawCast and 25 more
97 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem Algebra.IsQuadraticExtension.trace_algebraMap_add_algebraMap_mul (a b : K) (θ : L) :
    Algebra.trace K L (algebraMap K L b + algebraMap K L a * θ)
      = a * Algebra.trace K L θ + 2 * b := by
…
```
theorem Algebra.IsQuadraticExtension.norm_algebraMap_add_algebraMap_mul The norm of b + aθ in a separable quadratic extension is b² + ab·tr(θ) + a²·N(θ) line 54 source
Source documentation
The norm of b + aθ in a separable quadratic extension is b² + ab·tr(θ) + a²·N(θ).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, Eq, MonoidHom, Algebra.norm, HAdd.hAdd, RingHom, Algebra.algebraMap, HMul.hMul, HPow.hPow, Nat, OfNat.ofNat, LinearMap, RingHom.id, Algebra.trace
Proof uses: AlgEquiv, Ne, Exists, Algebra.IsQuadraticExtension.exists_algEquiv_ne_one, FaithfulSMul.algebraMap_injective, Eq.mpr, id, congr, congrArg, Eq.trans, Algebra.IsQuadraticExtension.algebraMap_norm_eq_mul, map_add, AlgEquiv.commutes, map_mul, MonoidHom.id, congrFun', map_pow, Algebra.IsQuadraticExtension.algebraMap_trace_eq_add, Mathlib.Tactic.Ring.of_eq, Nat.rawCast and 30 more
107 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem Algebra.IsQuadraticExtension.norm_algebraMap_add_algebraMap_mul (a b : K) (θ : L) :
    Algebra.norm K (algebraMap K L b + algebraMap K L a * θ)
      = b ^ 2 + a * b * Algebra.trace K L θ + a ^ 2 * Algebra.norm K θ := by
…
```
theorem Algebra.IsQuadraticExtension.discrim_ne_zero Documented declaration: discrim_ne_zero line 68 source
Source documentation
If θ generates a separable quadratic extension of K — that is, lies outside K — and t, n denote its trace and norm, so that θ² = tθ - n, then the discriminant t² - 4n of the minimal polynomial of θ is nonzero. (Over the nontrivial automorphism σ it equals (θ - σθ)² with σθ ≠ θ. In characteristic 2 the statement says t ≠ 0: separable quadratic extensions are Artin–Schreier extensions.)

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, Not, Membership.mem, Set, Set.range, RingHom, Algebra.algebraMap, Ne, HSub.hSub, HPow.hPow, Nat, LinearMap, RingHom.id, Algebra.trace, OfNat.ofNat, HMul.hMul, MonoidHom and 1 more
Proof uses: AlgEquiv, Exists, Algebra.IsQuadraticExtension.exists_algEquiv_ne_one, Eq, congrArg, Mathlib.Tactic.LinearCombination.eq_of_eq, HAdd.hAdd, Eq.mp, congr, Eq.trans, map_sub, map_pow, congrFun', Algebra.IsQuadraticExtension.algebraMap_trace_eq_add, map_mul, map_ofNat, Algebra.IsQuadraticExtension.algebraMap_norm_eq_mul, map_zero, Mathlib.Tactic.LinearCombination.eq_rearrange, Mathlib.Tactic.Ring.of_eq and 67 more
133 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem Algebra.IsQuadraticExtension.discrim_ne_zero {θ : L}
    (hθ : θ ∉ Set.range (algebraMap K L)) :
    Algebra.trace K L θ ^ 2 - 4 * Algebra.norm K θ ≠ 0 := by
…
```
theorem Algebra.IsQuadraticExtension.trace_eq_zero_of_sq_eq A square root α ∉ K of an element of K has trace 0: the nontrivial automorphism sends α to -α (Algebra.IsQuadraticExtension.algEquiv_apply_eq_neg_of_sq_eq) line 83 source
Source documentation
A square root α ∉ K of an element of K has trace 0: the nontrivial automorphism sends α to -α (Algebra.IsQuadraticExtension.algEquiv_apply_eq_neg_of_sq_eq).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, Not, Membership.mem, Set, Set.range, RingHom, Algebra.algebraMap, Eq, HPow.hPow, Nat, OfNat.ofNat, LinearMap, RingHom.id, Algebra.trace
Proof uses: AlgEquiv, Ne, Exists, Algebra.IsQuadraticExtension.exists_algEquiv_ne_one, FaithfulSMul.algebraMap_injective, Eq.mpr, HAdd.hAdd, id, congrArg, Algebra.IsQuadraticExtension.algebraMap_trace_eq_add, Neg.neg, Algebra.IsQuadraticExtension.algEquiv_apply_eq_neg_of_sq_eq, map_zero, add_neg_cancel, Eq.refl
84 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem Algebra.IsQuadraticExtension.trace_eq_zero_of_sq_eq {α : L} {d : K}
    (hαK : α ∉ Set.range (algebraMap K L)) (hα : α ^ 2 = algebraMap K L d) :
    Algebra.trace K L α = 0 := by
…
```
theorem Algebra.IsQuadraticExtension.norm_eq_neg_of_sq_eq A square root α ∉ K of d ∈ K has norm -d: the nontrivial automorphism sends α to -α (Algebra.IsQuadraticExtension.algEquiv_apply_eq_neg_of_sq_eq) line 93 source
Source documentation
A square root α ∉ K of d ∈ K has norm -d: the nontrivial automorphism sends α to -α (Algebra.IsQuadraticExtension.algEquiv_apply_eq_neg_of_sq_eq).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, Not, Membership.mem, Set, Set.range, RingHom, Algebra.algebraMap, Eq, HPow.hPow, Nat, OfNat.ofNat, MonoidHom, Algebra.norm, Neg.neg
Proof uses: AlgEquiv, Ne, Exists, Algebra.IsQuadraticExtension.exists_algEquiv_ne_one, FaithfulSMul.algebraMap_injective, Eq.mpr, HMul.hMul, id, congrArg, Algebra.IsQuadraticExtension.algebraMap_norm_eq_mul, Algebra.IsQuadraticExtension.algEquiv_apply_eq_neg_of_sq_eq, map_neg, Eq.symm, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, Nat.rawCast, Int.rawCast, inferInstance, Ring, Int.negOfNat and 35 more
92 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem Algebra.IsQuadraticExtension.norm_eq_neg_of_sq_eq {α : L} {d : K}
    (hαK : α ∉ Set.range (algebraMap K L)) (hα : α ^ 2 = algebraMap K L d) :
    Algebra.norm K α = -d := by
…
```