n : Type ?u.185522
p : Type ?u.185525
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
A : List.length (listTransvecRow M) = r
⊢ (M ⬝ List.prod (listTransvecRow M)) i (inr ()) = M i (inr ())
n : Type ?u.185522
p : Type ?u.185525
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
⊢ (M ⬝ List.prod (listTransvecRow M)) i (inr ()) = M i (inr ())
have A : (listTransvecRow M).length = r := by simp [listTransvecRow]
n : Type ?u.185522
p : Type ?u.185525
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
A : List.length (listTransvecRow M) = r
⊢ (M ⬝ List.prod (List.take r (listTransvecRow M))) i (inr ()) = M i (inr ())
n : Type ?u.185522
p : Type ?u.185525
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
A : List.length (listTransvecRow M) = r
⊢ (M ⬝ List.prod (listTransvecRow M)) i (inr ()) = M i (inr ())
rw [← List.take_length (listTransvecRow M), A]
no goals
n : Type ?u.185522
p : Type ?u.185525
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
A : List.length (listTransvecRow M) = r
⊢ (M ⬝ List.prod (List.take r (listTransvecRow M))) i (inr ()) = M i (inr ())
simpa using mul_listTransvecRow_last_col_take M i le_rfl
no goals
n : Type ?u.185522
p : Type ?u.185525
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.length (listTransvecRow M) = r
simp [listTransvecRow]