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

10 declarations, 0 contain sorry, 0 declared as axioms

Variant of Matrix.diagonal_transvection_induction_of_det_ne_zero that works over a commutative ring. Note that we have to assume that the matrix is a product of transvections and a diagonal matrix; this is not true in general (I believe; I think there's some obstruction in SK₁(R), the kernel of det:K₁(R) → Rˣ)

Imports (1)

Mathlib.LinearAlgebra.Matrix.Transvection

Imported by 2 files

def Matrix.Pivot.ExistsListTransvecMulDiagonalMulListTransvec The claim that a matrix is a product of transvections, a diagonal matrix, and more transvections line 27 source
Source documentation
The claim that a matrix is a product of transvections, a diagonal matrix, and more transvections. Always true if the base ring is a field.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Fintype, DecidableEq, Matrix
Proof uses: Exists, List, Matrix.TransvectionStruct, Eq, HMul.hMul, List.prod, List.map, Matrix.TransvectionStruct.toMatrix, Matrix.diagonal
14 instances, coercions and auxiliary constants left out.
```
def Pivot.ExistsListTransvecMulDiagonalMulListTransvec {n : Type*} {R : Type*} [CommRing R]
    [Fintype n] [DecidableEq n] (M : Matrix n n R) : Prop :=
…
```
lemma Matrix.Pivot.exists_list_transvec_mul_diagonal_mul_list_transvec' line 32 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, DecidableEq, Fintype, Matrix, Matrix.Pivot.ExistsListTransvecMulDiagonalMulListTransvec
Proof uses: Matrix.Pivot.exists_list_transvec_mul_diagonal_mul_list_transvec
1 instances, coercions and auxiliary constants left out.
def Matrix.TransvectionStruct.map Base change of a TransvectionStruct along a ring homomorphism line 43 source
Source documentation
Base change of a TransvectionStruct along a ring homomorphism.

no axioms what this means
Statement uses: CommRing, RingHom, Matrix.TransvectionStruct
Proof uses: Matrix.TransvectionStruct.mk, Matrix.TransvectionStruct.i, Matrix.TransvectionStruct.j, Matrix.TransvectionStruct.hij, Matrix.TransvectionStruct.c
8 instances, coercions and auxiliary constants left out.
```
def TransvectionStruct.map {n : Type*} {R S : Type*} [CommRing R] [CommRing S]
    (f : R →+* S) (t : TransvectionStruct n R) :
    TransvectionStruct n S where
…
```
lemma Matrix.TransvectionStruct.toMatrix_map line 51 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, DecidableEq, RingHom, Fintype, Matrix.TransvectionStruct, Eq, Matrix, Function.comp, Matrix.TransvectionStruct.toMatrix, Matrix.TransvectionStruct.map, RingHom.mapMatrix
Proof uses: of_eq_true, HAdd.hAdd, OfNat.ofNat, Matrix.single, Matrix.TransvectionStruct.i, Matrix.TransvectionStruct.j, Matrix.TransvectionStruct.c, Eq.trans, True, congrArg, map_add, congr, Matrix.map, RingHom.mapMatrix_apply, Matrix.map_one, congrFun', map_zero, eq_self, map_one, Matrix.map_single
40 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Matrix.TransvectionStruct.map_toMatrix line 56 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, DecidableEq, RingHom, Finite, Matrix.TransvectionStruct, Eq, Matrix, Matrix.TransvectionStruct.toMatrix, Matrix.TransvectionStruct.map, Matrix.map
Proof uses: Fintype, Fintype.ofFinite, Matrix.TransvectionStruct.toMatrix_map
8 instances, coercions and auxiliary constants left out.
lemma Matrix.TransvectionStruct.mapMatrix_map_toMatrix_prod line 61 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, DecidableEq, RingHom, Fintype, List, Matrix.TransvectionStruct, Eq, Matrix, RingHom.mapMatrix, List.prod, List.map, Matrix.TransvectionStruct.toMatrix, Function.comp, Matrix.TransvectionStruct.map
Proof uses: Eq.mpr, id, congrArg, map_list_prod, Mul, One, Eq.rec, Eq.refl, of_eq_true, Eq.trans, Membership.mem, True, congrFun', List.map_map, forall_congr, implies_congr, Matrix.map, congr, RingHom.mapMatrix_apply, Matrix.TransvectionStruct.map_toMatrix and 2 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Matrix.TransvectionStruct.mapMatrix_map_toMatrix_prod' line 70 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, DecidableEq, RingHom, Fintype, List, Matrix.TransvectionStruct, Eq, Matrix, Matrix.map, List.prod, List.map, Matrix.TransvectionStruct.toMatrix, Function.comp, Matrix.TransvectionStruct.map
Proof uses: Matrix.TransvectionStruct.mapMatrix_map_toMatrix_prod
19 instances, coercions and auxiliary constants left out.
lemma Matrix.Pivot.baseChange_existsListTransvecEtc line 78 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Fintype, DecidableEq, Matrix, Matrix.Pivot.ExistsListTransvecMulDiagonalMulListTransvec, RingHom, RingHom.mapMatrix
Proof uses: List, Matrix.TransvectionStruct, Exists, Eq, HMul.hMul, List.prod, List.map, Matrix.TransvectionStruct.toMatrix, Matrix.diagonal, Exists.intro, Matrix.TransvectionStruct.map, of_eq_true, Eq.trans, Function.comp, True, congr, congrArg, Matrix.map, RingHom.mapMatrix_apply, Matrix.map_mul and 8 more
38 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Matrix.diagonal_transvection_induction' Documented declaration: diagonal_transvection_induction' line 95 source
Source documentation
Variant of Matrix.diagonal_transvection_induction for commutative rings under the extra assumption ExistsListTransvecMulDiagonalMulListTransvec M (which is automatic for matrices over fields).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, DecidableEq, Fintype, Matrix, Matrix.Pivot.ExistsListTransvecMulDiagonalMulListTransvec, Eq, Matrix.det, Matrix.diagonal, Matrix.TransvectionStruct, Matrix.TransvectionStruct.toMatrix, HMul.hMul
Proof uses: List, Exists, List.prod, List.map, of_eq_true, Eq.trans, Finset.prod, Finset.univ, True, congr, congrArg, Matrix.det_diagonal, Matrix.det.congr_simp, Matrix.det_mul, OfNat.ofNat, Matrix.TransvectionStruct.det_toMatrix_prod, one_mul, mul_one, eq_self, List.rec and 9 more
37 instances, coercions and auxiliary constants left out.

Tactic trace: 17 steps
Open to load the checked before-and-after goal states.
```
theorem diagonal_transvection_induction' (P : Matrix n n R → Prop) (M : Matrix n n R)
    (hM : ExistsListTransvecMulDiagonalMulListTransvec M)
    (hdiag : ∀ D : n → R, det (diagonal D) = det M → P (diagonal D))
    (htransvec : ∀ t : TransvectionStruct n R, P t.toMatrix) (hmul : ∀ A B, P A → P B → P (A * B)) :
    P M := by
…
```
theorem Matrix.diagonal_transvection_induction_of_det_unit this proof is literally cut and pasted from mathlib with ≠ 0 changed to IsUnit and 𝕜 changed to R and addition of (hM : ExistsListTransvecMulDiagonalMulListTransvec M) line 124 source
Source comment
this proof is literally cut and pasted from mathlib with `≠ 0` changed to `IsUnit` and 𝕜 changed to R and addition of `(hM : ExistsListTransvecMulDiagonalMulListTransvec M)`

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, DecidableEq, Fintype, Matrix, Matrix.Pivot.ExistsListTransvecMulDiagonalMulListTransvec, IsUnit, Matrix.det, Matrix.diagonal, Matrix.TransvectionStruct, Matrix.TransvectionStruct.toMatrix, HMul.hMul
Proof uses: And, Matrix.diagonal_transvection_induction', And.intro, of_eq_true, Eq.trans, OfNat.ofNat, True, congrArg, Matrix.TransvectionStruct.det, Matrix.det_mul, congr, eq_true, And.left, and_self, And.right
29 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
theorem diagonal_transvection_induction_of_det_unit (P : Matrix n n R → Prop) (M : Matrix n n R)
    (hM : ExistsListTransvecMulDiagonalMulListTransvec M)
    (hMdet : IsUnit (det M)) (hdiag : ∀ D : n → R, IsUnit (det (diagonal D)) → P (diagonal D))
    (htransvec : ∀ t : TransvectionStruct n R, P t.toMatrix)
    (hmul : ∀ A B, IsUnit (det A) → IsUnit (det B) → P A → P B → P (A * B)) : P M := by
…
```