instAddCommGroup — Mathlib

English

The cusp form space CuspForm(Γ,k) carries the structure of an additive commutative group under pointwise addition: (f+g)(z)=f(z)+g(z), with 0 the zero form and standard additive inverses.

Русский

Пространство cusp-форм CuspForm(Γ,k) наделено структурой аддитивной коммутативной группы по точечному сложению: (f+g)(z)=f(z)+g(z), нулевой элемент — нулевая форма, существуют обратные по отношению к сложению.

LaTeX

$$$\text{CuspForm}(\Gamma,k)\text{ is an AddCommGroup with } (f+g)(z)=f(z)+g(z) \text{ and } 0(z)=0$$$

Lean4

instance : AddCommGroup (CuspForm Γ k) :=
  DFunLike.coe_injective.addCommGroup _ rfl coe_add coe_neg coe_sub coe_smul coe_smul

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