English
There exist two lists L and L' of transvections for the size r+1 case, reducing the matrix M to diagonal form provided the corresponding IH hypothesis holds for size r, i.e., the inductive step of reducing matrices to diagonal form via transvections.
Русский
Существуют два списка транспектаций для случая размера r+1, приводящие матрицу к диагональному виду при условии, что гипотеза IH верна для размера r — это индукционный шаг диагонализации матриц транспектациями.
LaTeX
$$$\exists L\,L' : List (TransvectionStruct (Fin (r+1) ⊕ Unit) 𝕜),\; \exists D : Fin (r+1) ⊕ Unit → 𝕜,\; (L.map toMatrix).prod * M * (L'.map toMatrix).prod = diagonal D$$$
Lean4
/-- Multiplying by all the matrices either in `listTransvecCol M` and `listTransvecRow M` kills
all the coefficients in the last column but the last one. -/
theorem listTransvecCol_mul_mul_listTransvecRow_last_row (hM : M (inr unit) (inr unit) ≠ 0) (i : Fin r) :
((listTransvecCol M).prod * M * (listTransvecRow M).prod) (inl i) (inr unit) = 0 :=
by
have : listTransvecCol M = listTransvecCol (M * (listTransvecRow M).prod) := by
simp [listTransvecCol, mul_listTransvecRow_last_col]
rw [this, Matrix.mul_assoc]
apply listTransvecCol_mul_last_col
simpa [mul_listTransvecRow_last_col] using hM
