English
If M is MulOneClass and N is a commutative group, then MonoidHom M N forms a commutative group under pointwise multiplication.
Русский
Если M — моноид с единицей, а N — коммутативная группа, то множество моноидных гомоморфизмов M → N образует коммутативную группу по точечному умножению.
LaTeX
$$$$ \text{CommGroup} (\mathrm{MonoidHom}(M,N)). $$$$
Lean4
/-- If `G` is a commutative group, then `M →* G` is a commutative group too. -/
@[to_additive /-- If `G` is an additive commutative group, then `M →+ G` is an additive commutative
group too. -/
]
instance instCommGroup [MulOneClass M] [CommGroup N] : CommGroup (M →* N) :=
fast_instance%DFunLike.coe_injective.commGroup DFunLike.coe rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
(fun _ _ => rfl) (fun _ _ => rfl)
