instMonoidUniformFun — Mathlib

English

If β is a Monoid, then the space of uniform functions α →ᵤ β forms a Monoid under pointwise multiplication.

Русский

Если β — моноид, то множество функций uniform α →ᵤ β образует моноид под покомпонентным умножением.

LaTeX

$$$[Monoid\ \beta] \Rightarrow [Monoid\ (\alpha \to^\mathrm{ᵤ}_\mathcal{S} \beta)]$$$

Lean4

@[to_additive]
instance [Monoid β] : Monoid (α →ᵤ β) :=
  Pi.monoid

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