instAddCommGroup — Mathlib

English

If γ is an additive commutative group, then AEEqFun α γ μ inherits a commutative additive group structure.

Русский

Если γ — коммутативная аддитивная группа, то AEEqFun α γ μ наследует коммутативную аддитивную группу.

LaTeX

$$instAddCommGroup : AddCommGroup (α →ₘ[μ] γ)$$

Lean4

instance instAddCommGroup [AddCommGroup γ] [IsTopologicalAddGroup γ] : AddCommGroup (α →ₘ[μ] γ) :=
  { add_comm := add_comm }

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