Theorems · Theorem · linear algebra

Matrix.diagonal_transvection_induction

∀ {n : Type u_1} {𝕜 : Type u_3} [inst : Field 𝕜] [inst_1 : DecidableEq n] [inst_2 : Fintype n] (P : Matrix n n 𝕜 → Prop)
  (M : Matrix n n 𝕜),
  (∀ (D : n → 𝕜), (Matrix.diagonal D).det = M.det → P (Matrix.diagonal D)) →
    (∀ (t : Matrix.TransvectionStruct n 𝕜), P t.toMatrix) → (∀ (A B : Matrix n n 𝕜), P A → P B → P (A * B)) → P M

Induction principle for matrices based on transvections: if a property is true for all diagonal matrices, all transvections, and is stable under product, then it is true for all matrices. This is the useful way to say that matrices are generated by diagonal matrices and transvections. We state a slightly more general version: to prove a property for a matrix M, it suffices to assume that the diagonal matrices we consider have the same determinant as M. This is useful to obtain similar principles for SLₙ or GLₙ.

Defined in

Mathlib.LinearAlgebra.Matrix.Transvection

Cited by

1 results in Mathlib

Foundations

Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldDecidableEqFintype