instCommGroup — Mathlib

English

If γ is a commutative group, then AEEqFun α γ μ is a commutative group under the induced structure.

Русский

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

LaTeX

$$instCommGroup : CommGroup (α →ₘ[μ] γ)$$

Lean4

@[to_additive existing]
instance instCommGroup [CommGroup γ] [IsTopologicalGroup γ] : CommGroup (α →ₘ[μ] γ) :=
  { mul_comm := mul_comm }

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