no goals
S : Type u_3
R : Type u_1
R₁ : Type ?u.185856
M : Type u_2
inst✝⁷ : Ring R
inst✝⁶ : CommRing R₁
inst✝⁵ : AddCommGroup 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 y : M
⊢ polar (↑Q) (a • x) y = a • polar (↑Q) x y
rw [← IsScalarTower.algebraMap_smul R a x, polar_smul_left, Algebra.smul_def]