no goals
n : Type u_1
p : Type ?u.1470
R : Type u₂
𝕜 : Type ?u.1475
inst✝³ : Field 𝕜
inst✝² : DecidableEq n
inst✝¹ : DecidableEq p
inst✝ : CommRing R
i j : n
⊢ transvection i j 0 = 1
simp [transvection]