instMonoid — Mathlib

English

OneHom M N is a Monoid whenever M is endowed with One and N a Monoid.

Русский

OneHom M N образует моноид, если у M есть единица и N является моноидом.

LaTeX

$$$\text{OneHom } M N\text{ is a Monoid if }M\text{ has }1\text{ and }N\text{ is a Monoid}$$$

Lean4

/-- `OneHom M N` is a `Monoid` if `N` is. -/
@[to_additive /-- `ZeroHom M N` is an `AddMonoid` if `N` is. -/
    ]
instance instMonoid [One M] [Monoid N] : Monoid (OneHom M N) :=
  fast_instance%DFunLike.coe_injective.monoid DFunLike.coe rfl (fun _ _ => rfl) (fun _ _ => rfl)

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