m : Type ?u.1639172
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
u v : n → R
⊢ det (updateRow Mᵀ j u) + det (updateRow Mᵀ j v) = det (updateColumn M j u) + det (updateColumn M j v)
m : Type ?u.1639172
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
u v : n → R
⊢ det (updateColumn M j (u + v)) = det (updateColumn M j u) + det (updateColumn M j v)
rw [← det_transpose, ← updateRow_transpose, det_updateRow_add]
no goals
m : Type ?u.1639172
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
u v : n → R
⊢ det (updateRow Mᵀ j u) + det (updateRow Mᵀ j v) = det (updateColumn M j u) + det (updateColumn M j v)
simp [updateRow_transpose, det_transpose]