English
If G is a commutative monoid, then the space C^n⟮I,N; I', G⟯ is a commutative monoid under coordinatewise multiplication.
Русский
Если G коммутативна моноид, то C^n⟮I,N; I', G⟯ образует коммутативный моноид при по точечному умножению.
LaTeX
$$$\text{If }G\text{ is a commutative monoid, then }C^n(I,N;I',G)\text{ is a commutative monoid under }(f\cdot g)(x)=f(x)g(x).$$$
Lean4
/-- Coercion to a function as a `MonoidHom`. Similar to `MonoidHom.coeFn`. -/
@[to_additive (attr := simps) /-- Coercion to a function as an `AddMonoidHom`.
Similar to `AddMonoidHom.coeFn`. -/
]
def coeFnMonoidHom {G : Type*} [Monoid G] [TopologicalSpace G] [ChartedSpace H' G] [ContMDiffMul I' n G] :
C^n⟮I, N; I', G⟯ →* N → G where
toFun := DFunLike.coe
map_one' := coe_one
map_mul' := coe_mul
