listTransvecCol_mul_last_row — Mathlib

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 _)

Похожие утверждения