English
There is an induction principle for reducing any matrix to diagonal form by elementary transvections: if every size r matrix can be reduced to diagonal form by transvections, then every size r+1 matrix can be reduced in the same way.
Русский
Существует индуктивный принцип сведения любой матрицы к диагональному виду с помощью элементарных транспектаций: если матрицы размера r можно свести к диагонали транспектациями, то и матрицы размера r+1 можно свести таким же образом.
LaTeX
$$$\forall M : Matrix (Fin\, r ⊕ Unit) (Fin\, r ⊕ Unit) 𝕜,\; \exists L,L',D:\, List (TransvectionStruct (Fin r ⊕ Unit) 𝕜),\; M = (L.map toMatrix).prod * M * (L'.map toMatrix).prod$$$
Lean4
/-- Any matrix can be reduced to diagonal form by elementary operations. -/
theorem exists_list_transvec_mul_mul_list_transvec_eq_diagonal (M : Matrix n n 𝕜) :
∃ (L L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
(L.map toMatrix).prod * M * (L'.map toMatrix).prod = diagonal D :=
by
have e : n ≃ Fin (Fintype.card n) := Fintype.equivOfCardEq (by simp)
apply reindex_exists_list_transvec_mul_mul_list_transvec_eq_diagonal M e
apply exists_list_transvec_mul_mul_list_transvec_eq_diagonal_aux
