English
An induction principle for invertible matrices: if a property holds for all invertible diagonal matrices, all transvections, and is stable under products of invertible matrices, then it holds for all invertible matrices.
Русский
Индуктивный принцип для обратимых матриц: если свойство верно для всех обратимых диагональных матриц, всех транспектаций и сохраняется под произведениями обратимых матриц, то оно верно и для всех обратимых матриц.
LaTeX
$$$P(M) \;\Longrightarrow\; (\forall D, \ det(diagonal D) \neq 0 \Rightarrow P(diagonal D)) \land (\forall t, P(t.toMatrix)) \land (\forall A,B, \det A \neq 0 \land \det B \neq 0 \Rightarrow P(A) \land P(B) \Rightarrow P(A B)) \Rightarrow P(M)$$$
Lean4
/-- Induction principle for invertible matrices based on transvections: if a property is true for
all invertible diagonal matrices, all transvections, and is stable under product of invertible
matrices, then it is true for all invertible matrices. This is the useful way to say that
invertible matrices are generated by invertible diagonal matrices and transvections. -/
theorem diagonal_transvection_induction_of_det_ne_zero (P : Matrix n n 𝕜 → Prop) (M : Matrix n n 𝕜) (hMdet : det M ≠ 0)
(hdiag : ∀ D : n → 𝕜, det (diagonal D) ≠ 0 → P (diagonal D))
(htransvec : ∀ t : TransvectionStruct n 𝕜, P t.toMatrix)
(hmul : ∀ A B, det A ≠ 0 → det B ≠ 0 → P A → P B → P (A * B)) : P M :=
by
let Q : Matrix n n 𝕜 → Prop := fun N => det N ≠ 0 ∧ P N
have : Q M := by
apply diagonal_transvection_induction Q M
· grind
· intro t
exact ⟨by simp, htransvec t⟩
· intro A B QA QB
exact ⟨by simp [QA.1, QB.1], hmul A B QA.1 QB.1 QA.2 QB.2⟩
exact this.2
