instCommMonoid — Mathlib

English

OneHom M N carries a commutative monoid structure provided N is commutative.

Русский

OneHom M N имеет структуру коммутативного моноида, если N коммутативен.

LaTeX

$$$\text{OneHom } M N\text{ is a }\mathrm{CommMonoid}$ when $N$ is a CommMonoid.$$

Lean4

/-- `(M →* N)` is a `CommMonoid` if `N` is commutative. -/
@[to_additive /-- `(M →+ N)` is an `AddCommMonoid` if `N` is commutative. -/
    ]
instance instCommMonoid [MulOneClass M] [CommMonoid N] : CommMonoid (M →* N) :=
  fast_instance%DFunLike.coe_injective.commMonoid DFunLike.coe rfl (fun _ _ => rfl) (fun _ _ => rfl)

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