no goals
S : Type ?u.2804
R : Type u_1
R₁ : Type ?u.2810
M : Type u_2
inst✝² : Ring R
inst✝¹ : CommRing R₁
inst✝ : AddCommGroup M
f : M → R
x y : M
⊢ polar (-f) x y = -polar f x y
simp only [polar, Pi.neg_apply, sub_eq_add_neg, neg_add]