FLT/Mathlib/LinearAlgebra/Dimension/IsQuadraticExtension.lean

GitHub source file

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

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

4 declarations, 0 contain sorry, 0 declared as axioms

Elements of a quadratic field extension

Proposed new Mathlib file Mathlib.LinearAlgebra.Dimension.IsQuadraticExtension: basic lemmas about elements of a quadratic extension lying outside the base field.

Imports (3)
Imported by 3 files
  1. theorem linearIndependent_one_of_notMem_range_algebraMap 1 and any element lying outside the base field are linearly independent over the base field line 27 source

    Source documentation

    1 and any element lying outside the base field are linearly independent over the base field.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Field, Algebra, Not, Membership.mem, Set, Set.range, RingHom, Algebra.algebraMap, LinearIndependent, Fin, Nat.succ, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty

    Proof uses: Iff.mpr, Ne, HSMul.hSMul, LinearIndependent.pair_iff', one_ne_zero, Eq, Exists.intro, Eq.mpr, id, congrArg, Algebra.algebraMap_eq_smul_one

    58 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem linearIndependent_one_of_notMem_range_algebraMap {θ : L}
    (hθ : θ ∉ Set.range (algebraMap K L)) : LinearIndependent K ![(1 : L), θ] :=
…
  2. theorem Algebra.IsQuadraticExtension.exists_notMem_range_algebraMap A quadratic extension contains an element not in the base field line 36 source

    Source documentation

    A quadratic extension contains an element not in the base field. (Used to choose a generator of L/K in the definition of the quadratic twist below.)

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Field, Algebra, Algebra.IsQuadraticExtension, Exists, Not, Membership.mem, Set, Set.range, RingHom, Algebra.algebraMap

    Proof uses: Classical.byContradiction, Eq, Subalgebra, Bot.bot, Top.top, Iff.mpr, Algebra.eq_top_iff, Algebra.mem_bot, Eq.mp, Eq.trans, binderNameHint, forall_congr, Nat, Module.finrank, OfNat.ofNat, Iff.mp, Subalgebra.bot_eq_top_iff_finrank_eq_one, Algebra.IsQuadraticExtension.finrank_eq_two

    46 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

    Open to load the checked before-and-after goal states.

    theorem Algebra.IsQuadraticExtension.exists_notMem_range_algebraMap :
    ∃ θ : L, θ ∉ Set.range (algebraMap K L) := by
…
  3. theorem Algebra.IsQuadraticExtension.exists_eq_algebraMap_add_algebraMap_mul Any element of a quadratic extension L/K is a K-linear combination of 1 and a given generator θ, and the θ-coefficient is nonzero if the element also lies outside K line 47 source

    Source documentation

    Any element of a quadratic extension L/K is a K-linear combination of 1 and a given generator θ, and the θ-coefficient is nonzero if the element also lies outside K.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Field, Algebra, Algebra.IsQuadraticExtension, Not, Membership.mem, Set, Set.range, RingHom, Algebra.algebraMap, Exists, And, Ne, OfNat.ofNat, Eq, HAdd.hAdd, HMul.hMul

    Proof uses: LinearIndependent, Fin, Nat.succ, Nat, Matrix.vecCons, Matrix.vecEmpty, linearIndependent_one_of_notMem_range_algebraMap, Submodule, Submodule.span, Eq.mpr, Top.top, id, congrArg, LinearIndependent.span_eq_top_of_card_eq_finrank, Fintype.card, Module.finrank, Fintype.card_fin, Eq.symm, Algebra.IsQuadraticExtension.finrank_eq_two, True.intro and 15 more

    87 instances, coercions and auxiliary constants left out.

    Tactic trace: 13 steps

    Open to load the checked before-and-after goal states.

    theorem Algebra.IsQuadraticExtension.exists_eq_algebraMap_add_algebraMap_mul {θ θ' : L}
    (hθ : θ ∉ Set.range (algebraMap K L)) (hθ' : θ' ∉ Set.range (algebraMap K L)) :
    ∃ a b : K, a ≠ 0 ∧ θ' = algebraMap K L b + algebraMap K L a * θ := by
…
  4. lemma notMem_range_algebraMap_of_not_isSquare An element whose square is (the image of) a nonsquare of K lies outside K line 68 source

    Source documentation

    An element whose square is (the image of) a nonsquare of K lies outside K.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Field, Algebra, Not, IsSquare, Eq, HPow.hPow, Nat, OfNat.ofNat, RingHom, Algebra.algebraMap, Membership.mem, Set, Set.range

    Proof uses: False, Exists.intro, HMul.hMul, FaithfulSMul.algebraMap_injective, Eq.mpr, id, congrArg, map_mul, Eq.symm, sq

    47 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

    Open to load the checked before-and-after goal states.

    lemma notMem_range_algebraMap_of_not_isSquare {d : K} (hd : ¬IsSquare d) {α : L}
    (hα : α ^ 2 = algebraMap K L d) : α ∉ Set.range (algebraMap K L) := by
…