no goals
n : Type u_1
p : Type ?u.20141
R : Type u₂
𝕜 : Type ?u.20146
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
i j : n
inst✝ : Fintype n
h : i ≠ j
c : R
⊢ det (transvection i j c) = 1
rw [← updateRow_eq_transvection i j, det_updateRow_add_smul_self _ h, det_one]