instCommMonoid — Mathlib

English

If γ is CommMonoid and ContinuousMul, then AEEqFun is a commutative monoid with respect to pointwise multiplication.

Русский

Если γ — коммутативный моноид и непрерывное умножение, тогда AEEqFun образует коммутативный моноид относительно точечного умножения.

LaTeX

$$$\text{CommMonoid}(α \to_{μ} γ)$$$

Lean4

@[to_additive existing]
instance instCommMonoid [CommMonoid γ] [ContinuousMul γ] : CommMonoid (α →ₘ[μ] γ) :=
  toGerm_injective.commMonoid toGerm one_toGerm mul_toGerm pow_toGerm

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