English
There exist two lists L and L' of transvection structures such that the product (L.map toMatrix).prod * M * (L'.map toMatrix).prod is diagonal, i.e., diagonalizable by transvections.
Русский
Существуют два списка транспектаций, дающих диагонализацию матрицы через их произведение.
LaTeX
$$$\exists L\,L' : List (TransvectionStruct n 𝕜),\; \exists D : n → 𝕜,\; (L.map toMatrix).prod * M * (L'.map toMatrix).prod = diagonal D$$$
Lean4
/-- Any matrix can be reduced to diagonal form by elementary operations. Formulated here on `Type 0`
because we will make an induction using `Fin r`.
See `exists_list_transvec_mul_mul_list_transvec_eq_diagonal` for the general version (which follows
from this one and reindexing). -/
theorem exists_list_transvec_mul_mul_list_transvec_eq_diagonal_aux (n : Type) [Fintype n] [DecidableEq n]
(M : Matrix n n 𝕜) :
∃ (L L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
(L.map toMatrix).prod * M * (L'.map toMatrix).prod = diagonal D :=
by
suffices
∀ cn,
Fintype.card n = cn →
∃ (L L' : List (TransvectionStruct n 𝕜)) (D : n → 𝕜),
(L.map toMatrix).prod * M * (L'.map toMatrix).prod = diagonal D
by exact this _ rfl
intro cn hn
induction cn generalizing n M with
| zero =>
refine ⟨List.nil, List.nil, fun _ => 1, ?_⟩
ext i j
rw [Fintype.card_eq_zero_iff] at hn
exact hn.elim' i
| succ r
IH =>
have e : n ≃ Fin r ⊕ Unit := by
refine Fintype.equivOfCardEq ?_
rw [hn]
rw [@Fintype.card_sum (Fin r) Unit _ _]
simp
apply reindex_exists_list_transvec_mul_mul_list_transvec_eq_diagonal M e
apply exists_list_transvec_mul_mul_list_transvec_eq_diagonal_induction fun N => IH (Fin r) N (by simp)
