English
There exist two lists of transvections L and L' such that the matrix obtained by left-multiplying M by the transvections from L and right-multiplying by those from L' is block-diagonal, provided the bottom-right entry of M is nonzero.
Русский
Существуют два списка транспектаций L и L', такие что левая и правая их умножение приводят матрицу к блочно-диагональному виду, если нижний правый элемент M не равен нулю.
LaTeX
$$$\exists L\,L' : List (TransvectionStruct (Fin r ⊕ Unit) 𝕜),\; IsTwoBlockDiagonal ((L.map toMatrix).prod * M * (L'.map toMatrix).prod)$$$
Lean4
/-- Multiplying by all the matrices in `listTransvecRow M` does not change the last column. -/
theorem mul_listTransvecRow_last_col (i : Fin r ⊕ Unit) :
(M * (listTransvecRow M).prod) i (inr unit) = M i (inr unit) :=
by
have A : (listTransvecRow M).length = r := by simp [listTransvecRow]
rw [← List.take_length (l := listTransvecRow M), A]
simpa using mul_listTransvecRow_last_col_take M i le_rfl
