no goals
S : Type ?u.154687
R : Type u_1
R₁ : Type ?u.154693
M : Type u_2
inst✝³ : Ring R
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x y : M
⊢ polar (↑Q) (-x) y = -polar (↑Q) x y
rw [← neg_one_smul R x, polar_smul_left, neg_one_mul]