English
Let M be a square matrix over a field with rows indexed by Fin r ⊕ Unit. For every i and every k ≤ r, multiplying M on the left by the product of the transvections in listTransvecCol M after dropping the first k elements does not change the value of the last row, i.e., the last row of M is invariant under these partial left multiplications.
Русский
Пусть M — квадратная матрица над телом, строки индексы Fin r ⊕ Unit. Для любого i и любого k ≤ r произведение левых множителей из списка listTransvecCol M после отброса первых k элементов не изменяет последнюю строку M; последняя строка инвариантна по отношению к этим частичным умножениям.
LaTeX
$$$\forall i: Fin\,r \oplus Unit,\; \forall k: \mathbb{N},\; k \le r \;\rightarrow\;(((listTransvecCol\,M).drop\,k).prod * M)(inr\,unit)\,i = M(inr\,unit)\,i$$$
Lean4
/-- Multiplying by some of the matrices in `listTransvecCol M` does not change the last row. -/
theorem listTransvecCol_mul_last_row_drop (i : Fin r ⊕ Unit) {k : ℕ} (hk : k ≤ r) :
(((listTransvecCol M).drop k).prod * M) (inr unit) i = M (inr unit) i := by
induction hk using Nat.decreasingInduction with
| of_succ n hn IH =>
have hn' : n < (listTransvecCol M).length := by simpa [listTransvecCol] using hn
rw [List.drop_eq_getElem_cons hn']
simpa [listTransvecCol, Matrix.mul_assoc]
| self => simp only [length_listTransvecCol, le_refl, List.drop_eq_nil_of_le, List.prod_nil, Matrix.one_mul]
