no goals
S : Type ?u.165922
R : Type u_1
R₁ : Type ?u.165928
M : Type u_2
inst✝³ : Ring R
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
a : R
x y : M
⊢ polar (↑Q) x (a • y) = a * polar (↑Q) x y
rw [polar_comm Q x, polar_comm Q x, polar_smul_left]