n : Type ?u.209504
p : Type ?u.209507
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
this : listTransvecCol M = listTransvecCol (M ⬝ List.prod (listTransvecRow M))
⊢ (List.prod (listTransvecCol M) ⬝ M ⬝ List.prod (listTransvecRow M)) (inl i) (inr ()) = 0
n : Type ?u.209504
p : Type ?u.209507
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
⊢ (List.prod (listTransvecCol M) ⬝ M ⬝ List.prod (listTransvecRow M)) (inl i) (inr ()) = 0
have : listTransvecCol M = listTransvecCol (M ⬝ (listTransvecRow M).prod) := by
  simp [listTransvecCol, mul_listTransvecRow_last_col]
n : Type ?u.209504
p : Type ?u.209507
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
this : listTransvecCol M = listTransvecCol (M ⬝ List.prod (listTransvecRow M))
⊢ (List.prod (listTransvecCol (M ⬝ List.prod (listTransvecRow M))) ⬝ (M ⬝ List.prod (listTransvecRow M))) (inl i)
      (inr ()) =
    0
n : Type ?u.209504
p : Type ?u.209507
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
this : listTransvecCol M = listTransvecCol (M ⬝ List.prod (listTransvecRow M))
⊢ (List.prod (listTransvecCol M) ⬝ M ⬝ List.prod (listTransvecRow M)) (inl i) (inr ()) = 0
rw [this, Matrix.mul_assoc]
case hM
n : Type ?u.209504
p : Type ?u.209507
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
this : listTransvecCol M = listTransvecCol (M ⬝ List.prod (listTransvecRow M))
⊢ (M ⬝ List.prod (listTransvecRow M)) (inr ()) (inr ()) ≠ 0
n : Type ?u.209504
p : Type ?u.209507
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
this : listTransvecCol M = listTransvecCol (M ⬝ List.prod (listTransvecRow M))
⊢ (List.prod (listTransvecCol (M ⬝ List.prod (listTransvecRow M))) ⬝ (M ⬝ List.prod (listTransvecRow M))) (inl i)
      (inr ()) =
    0
apply listTransvecCol_mul_last_col
no goals
case hM
n : Type ?u.209504
p : Type ?u.209507
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
this : listTransvecCol M = listTransvecCol (M ⬝ List.prod (listTransvecRow M))
⊢ (M ⬝ List.prod (listTransvecRow M)) (inr ()) (inr ()) ≠ 0
simpa [mul_listTransvecRow_last_col] using hM
no goals
n : Type ?u.209504
p : Type ?u.209507
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) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
⊢ listTransvecCol M = listTransvecCol (M ⬝ List.prod (listTransvecRow M))
simp [listTransvecCol, mul_listTransvecRow_last_col]