monoid — Mathlib

English

If G has a unit element, then the set of C^n-maps from N to G forms a monoid under pointwise multiplication with identity given by the constant map x ↦ 1_G.

Русский

Если G имеет единицу, то множество C^n-отображений из N в G образует моноид; тождественный элемент задаётся константной картой x ↦ 1_G.

LaTeX

$$$f,g\in C^n\langle I,N; I',G\rangle \implies (f\cdot g) \,\text{ is in } C^n\langle I,N; I',G\rangle,\quad \mathbf{1}(x)=1_G,\; (f\cdot \mathbf{1})=f= (\mathbf{1}\cdot f).$$$

Lean4

@[to_additive]
instance monoid {G : Type*} [Monoid G] [TopologicalSpace G] [ChartedSpace H' G] [ContMDiffMul I' n G] :
    Monoid C^n⟮I, N; I', G⟯ :=
  DFunLike.coe_injective.monoid _ coe_one coe_mul coe_pow

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