S : Type ?u.1072
R : Type u_1
R₁ : Type ?u.1078
M : Type u_2
inst✝² : Ring R
inst✝¹ : CommRing R₁
inst✝ : AddCommGroup M
f g : M → R
x y : M
⊢ f (x + y) + g (x + y) - (f x + g x) - (f y + g y) = f (x + y) - f x - f y + (g (x + y) - g x - g y)
S : Type ?u.1072
R : Type u_1
R₁ : Type ?u.1078
M : Type u_2
inst✝² : Ring R
inst✝¹ : CommRing R₁
inst✝ : AddCommGroup M
f g : M → R
x y : M
⊢ polar (f + g) x y = polar f x y + polar g x y
simp only [polar, Pi.add_apply]
no goals
S : Type ?u.1072
R : Type u_1
R₁ : Type ?u.1078
M : Type u_2
inst✝² : Ring R
inst✝¹ : CommRing R₁
inst✝ : AddCommGroup M
f g : M → R
x y : M
⊢ f (x + y) + g (x + y) - (f x + g x) - (f y + g y) = f (x + y) - f x - f y + (g (x + y) - g x - g y)
abel