English
Multiplying M on the right by the prefix of listTransvecRow M does not change the last column entries of M.
Русский
Правое умножение матрицы M на префикс списка listTransvecRow M не изменяет элементы последнего столбца M.
LaTeX
$$$\forall i: Fin\,r,\; (M * ((listTransvecRow\,M).take\,k).prod)(i)(inr\,unit) = M(i)(inr\,unit)\quad(\text{for } k \le r)$$$
Lean4
/-- Multiplying by some of the matrices in `listTransvecRow M` does not change the last column. -/
theorem mul_listTransvecRow_last_col_take (i : Fin r ⊕ Unit) {k : ℕ} (hk : k ≤ r) :
(M * ((listTransvecRow M).take k).prod) i (inr unit) = M i (inr unit) := by
induction k with
| zero => simp only [Matrix.mul_one, List.prod_nil, List.take, Matrix.mul_one]
| succ k IH =>
have hkr : k < r := hk
let k' : Fin r := ⟨k, hkr⟩
have :
(listTransvecRow M)[k]? =
↑(transvection (inr Unit.unit) (inl k') (-M (inr Unit.unit) (inl k') / M (inr Unit.unit) (inr Unit.unit))) :=
by simp only [k', listTransvecRow, hkr, dif_pos, List.getElem?_ofFn]
simp only [List.take_succ, ← Matrix.mul_assoc, this, List.prod_append, Matrix.mul_one, List.prod_cons,
List.prod_nil, Option.toList_some]
rw [mul_transvection_apply_of_ne, IH hkr.le]
simp only [Ne, not_false_iff, reduceCtorEq]
