no goals
n : Type ?u.155183
p : Type ?u.155186
R : Type u₂
𝕜 : Type u_1
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
⊢ (List.prod (listTransvecCol M) ⬝ M) (inr ()) i = M (inr ()) i
simpa using listTransvecCol_mul_last_row_drop M i (zero_le _)