polar_add — Mathlib

English

The polar form is linear with respect to addition of the argument f: polar (f + g) x y = polar f x y + polar g x y.

Русский

Полярная форма линейна по сложению функции: polar(f+g) x y = polar f x y + polar g x y.

LaTeX

$$$$ polar(f+g)\\,x\\,y = polar f\\,x\\,y + polar g\\,x\\,y. $$$$

Lean4

theorem polar_add (f g : M → N) (x y : M) : polar (f + g) x y = polar f x y + polar g x y :=
  by
  simp only [polar, Pi.add_apply]
  abel

Похожие утверждения