instAddCommGroup — Mathlib

English

The collection of formal 𝕜-multilinear series with values in E → F carries a natural additive commutative group structure, defined termwise by (f + g)(n) = f(n) + g(n) and (-f)(n) = -f(n).

Русский

Множество формальных 𝕜-мультиляйнерных рядов с значениями в E → F имеет естественную структуру аддитивной коммутативной группы: (f+g)(n) = f(n) + g(n), а (-f)(n) = -f(n).

LaTeX

$$$((f+g))_n = f_n + g_n\\quad\\text{и}\\quad ((-f))_n = -f_n$$$

Lean4

instance : AddCommGroup (FormalMultilinearSeries 𝕜 E F) :=
  inferInstanceAs <| AddCommGroup <| ∀ n : ℕ, E [×n]→L[𝕜] F

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