instCommMonoid — Mathlib

English

OneHom M N inherits commutative monoid structure from N when N is commutative.

Русский

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

LaTeX

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

Lean4

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

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