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