no goals
S : Type ?u.144337
R : Type u_1
R₁ : Type ?u.144343
M : Type u_2
inst✝³ : Ring R
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
y : M
⊢ polar (↑Q) 0 y = 0
simp only [polar, zero_add, QuadraticForm.map_zero, sub_zero, sub_self]