no goals
S : Type u_1
R : Type u_2
R₁ : Type ?u.131813
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
Q : QuadraticForm R M
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
a : S
x : M
⊢ ↑Q (a • x) = (a * a) • ↑Q x
rw [← IsScalarTower.algebraMap_smul R a x, map_smul, ← RingHom.map_mul, Algebra.smul_def]