no goals
m : Type ?u.1671111
n : Type u_1
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i j : n
hij : i ≠ j
⊢ det (updateRow A i (A i + A j)) = det A
simp [det_updateRow_add,
  det_zero_of_row_eq hij (updateRow_self.trans (updateRow_ne hij.symm).symm)]