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

12 declarations, 0 contain sorry, 0 declared as axioms

The Galois theory of separable quadratic extensions

Material for Mathlib.FieldTheory.Galois.Basic: a separable quadratic extension L/K has exactly two automorphisms; trace and norm via the nontrivial automorphism; the quadratic character of Aut(M/K) attached to a normal subextension K ⊆ L ⊆ M.

Imports (3)

Imported by 3 files

theorem forall_apply_algebraMap_iff_restrictNormal_eq_one For a normal subextension K ⊆ L ⊆ M, a K-automorphism σ of M fixes L pointwise if and only if its restriction to L (AlgEquiv.restrictNormal) is the identity line 35 source
Source documentation
For a normal subextension K ⊆ L ⊆ M, a K-automorphism σ of M fixes L pointwise if and only if its restriction to L (AlgEquiv.restrictNormal) is the identity.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsQuadraticExtension, IsScalarTower, AlgEquiv, Iff, Eq, RingHom, Algebra.algebraMap, AlgEquiv.restrictNormal, OfNat.ofNat
Proof uses: Eq.mpr, id, congr, congrArg, forall_congr, congrFun', forall_congr', Function.Injective.eq_iff, FaithfulSMul.algebraMap_injective
47 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem forall_apply_algebraMap_iff_restrictNormal_eq_one (σ : M ≃ₐ[K] M) :
    (∀ x : L, σ (algebraMap L M x) = algebraMap L M x) ↔ σ.restrictNormal L = 1 := by
…
```
theorem Algebra.IsQuadraticExtension.card_algEquiv A separable quadratic extension has exactly two automorphisms line 50 source
Source documentation
A separable quadratic extension has exactly two automorphisms.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, Eq, Nat, Nat.card, AlgEquiv, OfNat.ofNat
Proof uses: Eq.mpr, Module.finrank, id, congrArg, IsGalois.card_aut_eq_finrank, Algebra.IsQuadraticExtension.finrank_eq_two
24 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem Algebra.IsQuadraticExtension.card_algEquiv : Nat.card (L ≃ₐ[K] L) = 2 := by
…
```
theorem Algebra.IsQuadraticExtension.exists_algEquiv_ne_one A separable quadratic extension has a nontrivial automorphism line 55 source
Source documentation
A separable quadratic extension has a nontrivial automorphism.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, Exists, AlgEquiv, Ne, OfNat.ofNat
Proof uses: ExistsUnique.exists, Iff.mp, Eq, Nat, Nat.card, ExistsUnique, Nat.card_eq_two_iff', Algebra.IsQuadraticExtension.card_algEquiv
31 instances, coercions and auxiliary constants left out.
```
theorem Algebra.IsQuadraticExtension.exists_algEquiv_ne_one : ∃ σ : L ≃ₐ[K] L, σ ≠ 1 :=
…
```
theorem Algebra.IsQuadraticExtension.algEquiv_eq_one_or_eq The only automorphisms of a separable quadratic extension are the identity and any given nontrivial automorphism line 60 source
Source documentation
The only automorphisms of a separable quadratic extension are the identity and any given nontrivial automorphism.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, AlgEquiv, Ne, OfNat.ofNat, Or, Eq
Proof uses: eq_or_ne, Or.inl, Or.inr, ExistsUnique.unique, Iff.mp, Nat, Nat.card, ExistsUnique, Nat.card_eq_two_iff', Algebra.IsQuadraticExtension.card_algEquiv
32 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem Algebra.IsQuadraticExtension.algEquiv_eq_one_or_eq {σ : L ≃ₐ[K] L} (hσ : σ ≠ 1)
    (φ : L ≃ₐ[K] L) : φ = 1 ∨ φ = σ := by
…
```
theorem Algebra.IsQuadraticExtension.algEquiv_mul_self The nontrivial automorphism of a separable quadratic extension is an involution line 67 source
Source documentation
The nontrivial automorphism of a separable quadratic extension is an involution.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, AlgEquiv, Ne, OfNat.ofNat, Eq, HMul.hMul
Proof uses: Or.resolve_right, Algebra.IsQuadraticExtension.algEquiv_eq_one_or_eq, absurd, False, Iff.mp, mul_eq_left
47 instances, coercions and auxiliary constants left out.
```
theorem Algebra.IsQuadraticExtension.algEquiv_mul_self {σ : L ≃ₐ[K] L} (hσ : σ ≠ 1) :
    σ * σ = 1 :=
…
```
theorem Algebra.IsQuadraticExtension.mem_range_algebraMap_of_apply_eq An element fixed by a nontrivial automorphism — hence, Gal(L/K) having order two, by all of Gal(L/K) — lies in the base field line 73 source
Source documentation
An element fixed by a nontrivial automorphism — hence, Gal(L/K) having order two, by all of Gal(L/K) — lies in the base field.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, AlgEquiv, Ne, OfNat.ofNat, Eq, Membership.mem, Set, Set.range, RingHom, Algebra.algebraMap
Proof uses: Eq.mpr, id, congrArg, propext, IsGalois.mem_range_algebraMap_iff_fixed, Or, Algebra.IsQuadraticExtension.algEquiv_eq_one_or_eq, AlgEquiv.one_apply, Eq.symm
44 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem Algebra.IsQuadraticExtension.mem_range_algebraMap_of_apply_eq {σ : L ≃ₐ[K] L}
    (hσ : σ ≠ 1) {x : L} (hx : σ x = x) : x ∈ Set.range (algebraMap K L) := by
…
```
theorem Algebra.IsQuadraticExtension.univ_algEquiv The automorphism group of a separable quadratic extension consists of the identity and one nontrivial element line 84 source
Source documentation
The automorphism group of a separable quadratic extension consists of the identity and one nontrivial element.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, AlgEquiv, Ne, OfNat.ofNat, Eq, Finset, Finset.univ, Insert.insert, Classical.propDecidable, Singleton.singleton
Proof uses: Eq.symm, Finset.eq_univ_of_forall, Eq.mpr, Membership.mem, Or, id, Eq.trans, congrArg, Algebra.IsQuadraticExtension.algEquiv_eq_one_or_eq
42 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem Algebra.IsQuadraticExtension.univ_algEquiv {σ : L ≃ₐ[K] L} (hσ : σ ≠ 1) :
    (Finset.univ : Finset (L ≃ₐ[K] L)) = {1, σ} :=
…
```
theorem Algebra.IsQuadraticExtension.algEquiv_apply_ne The nontrivial automorphism of a separable quadratic extension moves every element lying outside the base field line 90 source
Source documentation
The nontrivial automorphism of a separable quadratic extension moves every element lying outside the base field.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, AlgEquiv, Ne, OfNat.ofNat, Not, Membership.mem, Set, Set.range, RingHom, Algebra.algebraMap
Proof uses: Eq, Algebra.IsQuadraticExtension.mem_range_algebraMap_of_apply_eq
40 instances, coercions and auxiliary constants left out.
```
theorem Algebra.IsQuadraticExtension.algEquiv_apply_ne {σ : L ≃ₐ[K] L} (hσ : σ ≠ 1) {x : L}
    (hx : x ∉ Set.range (algebraMap K L)) : σ x ≠ x :=
…
```
theorem Algebra.IsQuadraticExtension.algEquiv_apply_eq_neg_of_sq_eq The nontrivial automorphism of a separable quadratic extension sends a square root α ∉ K of an element of K to -α line 96 source
Source documentation
The nontrivial automorphism of a separable quadratic extension sends a square root α ∉ K of an element of K to -α.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsQuadraticExtension, Algebra.IsSeparable, AlgEquiv, Ne, OfNat.ofNat, Not, Membership.mem, Set, Set.range, RingHom, Algebra.algebraMap, Eq, HPow.hPow, Nat, Neg.neg
Proof uses: Algebra.IsQuadraticExtension.algEquiv_apply_ne, HMul.hMul, HSub.hSub, HAdd.hAdd, Eq.mpr, id, congrArg, Eq.symm, map_pow, AlgEquiv.commutes, Eq.refl, Mathlib.Tactic.LinearCombination.eq_of_eq, Mathlib.Tactic.LinearCombination.eq_rearrange, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.sub_congr, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Int.rawCast, inferInstance, Ring and 51 more
98 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
theorem Algebra.IsQuadraticExtension.algEquiv_apply_eq_neg_of_sq_eq {σ : L ≃ₐ[K] L} (hσ : σ ≠ 1)
    {α : L} {d : K} (hαK : α ∉ Set.range (algebraMap K L)) (hα : α ^ 2 = algebraMap K L d) :
    σ α = -α := by
…
```
def quadraticCharacter The quadratic character of Aut(M/K) attached to a separable quadratic subextension K ⊆ L ⊆ M: it sends σ to 1 if σ fixes L pointwise, and to -1 otherwise line 116 source
Source documentation
The quadratic character of Aut(M/K) attached to a separable quadratic subextension K ⊆ L ⊆ M: it sends σ to 1 if σ fixes L pointwise, and to -1 otherwise.
Since L/K is normal, every K-automorphism of M maps L to L, and multiplicativity (map_mul') follows because restriction to L is a homomorphism to the order 2 group Gal(L/K). Taking M = L gives the quadratic character of Gal(L/K) itself; if M/K is normal then this character is the composite of the restriction Aut(M/K) → Gal(L/K) with the unique isomorphism Gal(L/K) ≃ {±1}, and in particular is surjective (quadraticCharacter_surjective).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsQuadraticExtension, IsScalarTower, Algebra.IsSeparable, MonoidHom, AlgEquiv, Units, Int
Proof uses: MonoidHom.mk, OneHom.mk, ite, Eq, RingHom, Algebra.algebraMap, Classical.propDecidable, OfNat.ofNat, Neg.neg
47 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
noncomputable def quadraticCharacter : (M ≃ₐ[K] M) →* ℤˣ where
…
```
theorem quadraticCharacter_eq_one_iff line 133 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsQuadraticExtension, IsScalarTower, Algebra.IsSeparable, AlgEquiv, Iff, Eq, Units, Int, MonoidHom, quadraticCharacter, OfNat.ofNat, RingHom, Algebra.algebraMap
Proof uses: id, MonoidHom.mk, OneHom.mk, ite, Classical.propDecidable, Neg.neg, dite, Eq.mpr, congrFun', congrArg, ite_eq_left, iff_of_true, rfl, Not, ite_eq_right, iff_of_false, False.elim, False, Eq.mp, eq_false' and 2 more
61 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
theorem quadraticCharacter_surjective Documented declaration: quadraticCharacter_surjective line 145 source
Source documentation
If M/K is normal (for example M = L, or M a separable closure of K) then the nontrivial element of Gal(L/K) extends to an automorphism of M, so the quadratic character of Aut(M/K) attached to L/K is surjective.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, Algebra.IsQuadraticExtension, IsScalarTower, Algebra.IsSeparable, Normal, Function.Surjective, AlgEquiv, Units, Int, MonoidHom, quadraticCharacter
Proof uses: Eq, OfNat.ofNat, Neg.neg, Or, Exists, Int.units_eq_one_or, Exists.intro, map_one, Eq.symm, Ne, Algebra.IsQuadraticExtension.exists_algEquiv_ne_one, AlgEquiv.restrictNormalHom, AlgEquiv.restrictNormalHom_surjective, Or.resolve_left, Eq.mpr, id, congrArg, Iff.mp, RingHom, Algebra.algebraMap and 3 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
theorem quadraticCharacter_surjective [Normal K M] :
    Function.Surjective (quadraticCharacter K L M) := by
…
```
Mentions: quadraticCharacter