instAddCommGroup — Mathlib

English

Modular forms form an additive commutative group under pointwise addition and scalar negation.

Русский

Модульные формы образуют аддитивную коммутативную группу по точечному сложению и отрицанию.

LaTeX

$$$ (f+g) = f+g, \ (0)(z)=0, \ (-f)(z) = -f(z). $$$

Lean4

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

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