no goals
S : Type ?u.547922
R : Type ?u.547925
R₁ : Type u_1
M : Type ?u.547931
n : Type w
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing R₁
inst✝² : AddCommMonoid M
inst✝¹ : Module R₁ M
inst✝ : Invertible 2
a : R₁
Q : QuadraticForm R₁ (n → R₁)
⊢ toMatrix' (a • Q) = a • toMatrix' Q
simp only [toMatrix', LinearEquiv.map_smul, LinearMap.map_smul]