m : Type ?u.1649973
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
s : R
u : n → R
⊢ s * det (updateRow Mᵀ j u) = s * det (updateColumn M j u)
m : Type ?u.1649973
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
s : R
u : n → R
⊢ det (updateColumn M j (s • u)) = s * det (updateColumn M j u)
rw [← det_transpose, ← updateRow_transpose, det_updateRow_smul]
no goals
m : Type ?u.1649973
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
s : R
u : n → R
⊢ s * det (updateRow Mᵀ j u) = s * det (updateColumn M j u)
simp [updateRow_transpose, det_transpose]