instCommGroupUniformOnFun — Mathlib

English

If β is a CommMonoid, UniformOnFun α β 𝔖 inherits a commutative monoid structure by pointwise operations.

Русский

Если β — коммутативный моноид, UniformOnFun α β 𝔖 наследует коммутативный моноид по точкам.

LaTeX

$$$\text{CommMonoid}(\text{UniformOnFun}_{\mathfrak{S}}(\alpha,\beta)) \text{ when } \text{CommMonoid}(\beta).$$$

Lean4

@[to_additive]
instance [CommGroup β] : CommGroup (α →ᵤ[𝔖] β) :=
  Pi.commGroup

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