English
Multiplying M on the left by the entire product of all matrices in listTransvecCol M leaves the last row unchanged.
Русский
Умножение слева на произведение всех матриц из listTransvecCol M оставляет последнюю строку M неизменной.
LaTeX
$$$\forall i: Fin\, r \oplus Unit,\; ((listTransvecCol\,M).prod * M)(inr\,unit)\,i = M(inr\,unit)\,i$$$
Lean4
/-- Multiplying by all the matrices in `listTransvecCol M` does not change the last row. -/
theorem listTransvecCol_mul_last_row (i : Fin r ⊕ Unit) :
((listTransvecCol M).prod * M) (inr unit) i = M (inr unit) i := by
simpa using listTransvecCol_mul_last_row_drop M i (zero_le _)