English
There exist two lists L and L' of transvection structures such that the matrix obtained by left-multiplying M by the transvections in L and right-multiplying by those in L' equals a diagonal matrix.
Русский
Существуют два списка транспектаций L и L', таких что произведение слева и справа преобразует M в диагональную матрицу.
LaTeX
$$$\exists L\,L' : List (TransvectionStruct n 𝕜),\; (L.map toMatrix).prod * M * (L'.map toMatrix).prod = diagonal D$$$
Lean4
/-- Multiplying by all the matrices either in `listTransvecCol M` and `listTransvecRow M` turns
the matrix in block-diagonal form. -/
theorem isTwoBlockDiagonal_listTransvecCol_mul_mul_listTransvecRow (hM : M (inr unit) (inr unit) ≠ 0) :
IsTwoBlockDiagonal ((listTransvecCol M).prod * M * (listTransvecRow M).prod) :=
by
constructor
· ext i j
have : j = unit := by simp only
simp [toBlocks₁₂, this, listTransvecCol_mul_mul_listTransvecRow_last_row M hM]
· ext i j
have : i = unit := by simp only
simp [toBlocks₂₁, this, listTransvecCol_mul_mul_listTransvecRow_last_col M hM]
