no goals
n : Type u_1
p : Type ?u.9953
R : Type u₂
𝕜 : Type ?u.9958
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
i j : n
inst✝ : Fintype n
h : i ≠ j
c d : R
⊢ transvection i j c ⬝ transvection i j d = transvection i j (c + d)
simp [transvection, Matrix.add_mul, Matrix.mul_add, h, h.symm, add_smul, add_assoc,
  stdBasisMatrix_add]