map_add — Mathlib

English

For any two maps f, g : M → N, the polar form is additive in the first argument: polar(f+g, x, y) = polar(f, x, y) + polar(g, x, y) for all x, y ∈ M.

Русский

Для любых отображений f,g: M → N полярная форма аддитивна по первому аргументов: polar(f+g, x, y) = polar(f, x, y) + polar(g, x, y) для всех x,y ∈ M.

LaTeX

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

Lean4

protected theorem map_add (f : M → N) (x y : M) : f (x + y) = f x + f y + polar f x y :=
  by
  rw [polar]
  abel

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