English
An auxiliary lemma expressing bilinearity of polar without subtraction; polar f (x+x') y equals polar f x y plus polar f x' y given a certain algebraic manipulation.
Русский
Дополнительная лемма об билинейности полярной функции без вычитания; polar f (x+x') y = polar f x y + polar f x' y при определённых преобразованиях.
LaTeX
$$$$ polar f (x + x') y = polar f x y + polar f x' y \\quad\\text{iff}\\quad f(x+x'+y) + (f x + f x' + f y) = f(x+x') + f(x'+y) + f(y+x). $$$$
Lean4
/-- Auxiliary lemma to express bilinearity of `QuadraticMap.polar` without subtraction. -/
theorem polar_add_left_iff {f : M → N} {x x' y : M} :
polar f (x + x') y = polar f x y + polar f x' y ↔
f (x + x' + y) + (f x + f x' + f y) = f (x + x') + f (x' + y) + f (y + x) :=
by
simp only [← add_assoc]
simp only [polar, sub_eq_iff_eq_add, eq_sub_iff_add_eq, sub_add_eq_add_sub, add_sub]
simp only [add_right_comm _ (f y) _, add_right_comm _ (f x') (f x)]
rw [add_comm y x, add_right_comm _ _ (f (x + y)), add_comm _ (f (x + y)), add_right_comm (f (x + y)), add_left_inj]
