English
There exist two lists L and L' of transvection structures such that the two-sided product (L.map toMatrix).prod * M * (L'.map toMatrix).prod is diagonal, i.e., M can be brought to diagonal form by elementary row/column operations represented by transvections.
Русский
Существуют два списка транспектаций, таких что двустороннее произведение приводит M к диагональному виду через элементарные операции слева и справа.
LaTeX
$$$\exists L\,L' : List (TransvectionStruct n 𝕜),\; (L.map toMatrix).prod * M * (L'.map toMatrix).prod = diagonal D$$$
Lean4
/-- There exist two lists of `TransvectionStruct` such that multiplying by them on the left and
on the right makes a matrix block-diagonal, when the last coefficient is nonzero. -/
theorem exists_isTwoBlockDiagonal_of_ne_zero (hM : M (inr unit) (inr unit) ≠ 0) :
∃ L L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜),
IsTwoBlockDiagonal ((L.map toMatrix).prod * M * (L'.map toMatrix).prod) :=
by
let L : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
List.ofFn fun i : Fin r => ⟨inl i, inr unit, by simp, -M (inl i) (inr unit) / M (inr unit) (inr unit)⟩
let L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜) :=
List.ofFn fun i : Fin r => ⟨inr unit, inl i, by simp, -M (inr unit) (inl i) / M (inr unit) (inr unit)⟩
refine ⟨L, L', ?_⟩
have A : L.map toMatrix = listTransvecCol M := by simp [L, listTransvecCol, Function.comp_def]
have B : L'.map toMatrix = listTransvecRow M := by simp [L', listTransvecRow, Function.comp_def]
rw [A, B]
exact isTwoBlockDiagonal_listTransvecCol_mul_mul_listTransvecRow M hM
