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