FLT/Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/Defs.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

11 declarations, 0 contain sorry, 0 declared as axioms

Defs

Material destined for Mathlib.

Imports (1)
Imported by 3 files
  1. def Matrix.GeneralLinearGroup.diagonal The invertible diagonal matrix associated to a vector of units (the diagonal entries) line 24 source

    Source documentation

    The invertible diagonal matrix associated to a vector of units (the diagonal entries).

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

    Statement uses: DecidableEq, Fintype, CommRing, Units, Matrix.GeneralLinearGroup

    Proof uses: Units.mk, Matrix, Matrix.diagonal, Inv.inv

    13 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

    def diagonal (d : n → Rˣ) : GL n R :=
…
  2. lemma Matrix.GeneralLinearGroup.val_diagonal line 29 source

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

    Statement uses: DecidableEq, Fintype, CommRing, Units, Eq, Matrix, Matrix.GeneralLinearGroup.diagonal, Matrix.diagonal

    Proof uses: rfl

    12 instances, coercions and auxiliary constants left out.

  3. lemma Matrix.GeneralLinearGroup.diagonal_one line 33 source

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

    Statement uses: DecidableEq, Fintype, CommRing, Eq, Matrix.GeneralLinearGroup, Matrix.GeneralLinearGroup.diagonal, OfNat.ofNat, Units, Matrix

    Proof uses: Units.ext, Matrix.ext, of_eq_true, Eq.trans, True, congrFun', congrArg, Units.mk, Matrix.diagonal, HMul.hMul, Inv.inv, funext, inv_one, id, Eq.refl, Units.mk.congr_simp, eq_self

    34 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  4. def Matrix.GeneralLinearGroup.GL2.unipotent The unipotent matrix element !![1, t; 0, 1] line 40 source

    Source documentation

    The unipotent matrix element !![1, t; 0, 1].

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

    Statement uses: CommRing, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat

    Proof uses: Units.mk, Matrix, Equiv, Matrix.of, Matrix.vecCons, Matrix.vecEmpty, Neg.neg

    31 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

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

    noncomputable def unipotent (t : R) : GL (Fin 2) R :=
…
  5. lemma Matrix.GeneralLinearGroup.GL2.unipotent_def line 45 source

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

    Statement uses: CommRing, Eq, Matrix, Fin, OfNat.ofNat, Nat, Matrix.GeneralLinearGroup.GL2.unipotent, Equiv, Matrix.of, Matrix.vecCons, Matrix.vecEmpty

    Proof uses: rfl

    27 instances, coercions and auxiliary constants left out.

  6. lemma Matrix.GeneralLinearGroup.GL2.unipotent_zero_zero line 48 source

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

    Statement uses: CommRing, Eq, Matrix, Fin, OfNat.ofNat, Nat, Matrix.GeneralLinearGroup.GL2.unipotent

    Proof uses: rfl

    25 instances, coercions and auxiliary constants left out.

  7. lemma Matrix.GeneralLinearGroup.GL2.unipotent_zero_one line 49 source

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

    Statement uses: CommRing, Eq, Matrix, Fin, OfNat.ofNat, Nat, Matrix.GeneralLinearGroup.GL2.unipotent

    Proof uses: rfl

    20 instances, coercions and auxiliary constants left out.

  8. lemma Matrix.GeneralLinearGroup.GL2.unipotent_one_zero line 50 source

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

    Statement uses: CommRing, Eq, Matrix, Fin, OfNat.ofNat, Nat, Matrix.GeneralLinearGroup.GL2.unipotent

    Proof uses: rfl

    23 instances, coercions and auxiliary constants left out.

  9. lemma Matrix.GeneralLinearGroup.GL2.unipotent_one_one line 51 source

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

    Statement uses: CommRing, Eq, Matrix, Fin, OfNat.ofNat, Nat, Matrix.GeneralLinearGroup.GL2.unipotent

    Proof uses: rfl

    25 instances, coercions and auxiliary constants left out.

  10. lemma Matrix.GeneralLinearGroup.GL2.unipotent_inv line 54 source

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

    Statement uses: CommRing, Eq, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, Inv.inv, Matrix, Matrix.GeneralLinearGroup.GL2.unipotent, Neg.neg

    Proof uses: Units.ext, Eq.refl

    31 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  11. lemma Matrix.GeneralLinearGroup.GL2.unipotent_mul line 57 source

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

    Statement uses: CommRing, Eq, Matrix.GeneralLinearGroup, Fin, OfNat.ofNat, Nat, HMul.hMul, Matrix, Matrix.GeneralLinearGroup.GL2.unipotent, HAdd.hAdd

    Proof uses: Units.ext, Matrix.ext, List, List.Mem, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil, of_eq_true, Eq.trans, True, congrFun' and 38 more

    70 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

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