no goals
n : Type u_1
p : Type ?u.18322
R : Type u₂
𝕜 : Type ?u.18327
inst✝⁴ : Field 𝕜
inst✝³ : DecidableEq n
inst✝² : DecidableEq p
inst✝¹ : CommRing R
i j : n
inst✝ : Fintype n
a b : n
hb : b ≠ j
c : R
M : Matrix n n R
⊢ (M ⬝ transvection i j c) a b = M a b
simp [transvection, Matrix.mul_add, hb]