English
The combination of left transvections from listTransvecCol M and right transvections from listTransvecRow M yields a two-block diagonal form of the matrix, killing off the off-block coefficients in the last row and column.
Русский
Сочетание левых транспектаций из listTransvecCol M и правых транспектаций из listTransvecRow M приводит матрицу к двум блокам диагонального вида, уничтожая коэффициенты за пределами блоков.
LaTeX
$$$IsTwoBlockDiagonal\left( (listTransvecCol\,M).prod * M * (listTransvecRow\,M).prod \right)$$$
Lean4
/-- Multiplying by all the matrices either in `listTransvecCol M` and `listTransvecRow M` kills
all the coefficients in the last row but the last one. -/
theorem listTransvecCol_mul_mul_listTransvecRow_last_col (hM : M (inr unit) (inr unit) ≠ 0) (i : Fin r) :
((listTransvecCol M).prod * M * (listTransvecRow M).prod) (inr unit) (inl i) = 0 :=
by
have : listTransvecRow M = listTransvecRow ((listTransvecCol M).prod * M) := by
simp [listTransvecRow, listTransvecCol_mul_last_row]
rw [this]
apply mul_listTransvecRow_last_row
simpa [listTransvecCol_mul_last_row] using hM
