English
A submonoid of a Monoid M naturally inherits a Monoid structure on its carrier; i.e., Submonoid M is a Monoid when viewed inside M.
Русский
Подмономод подмножества Monoid M естественным образом наследует моноидную структуру на носителе; то есть Submonoid M является моноидом как подмножество M.
LaTeX
$$$\text{Submonoid } M \to \text{Monoid}$$$
Lean4
/-- A submonoid of a monoid inherits a monoid structure. -/
@[to_additive /-- An `AddSubmonoid` of an `AddMonoid` inherits an `AddMonoid` structure. -/
]
instance (priority := 75) toMonoid {M : Type*} [Monoid M] {A : Type*} [SetLike A M] [SubmonoidClass A M] (S : A) :
Monoid S :=
fast_instance%Subtype.coe_injective.monoid Subtype.val rfl (fun _ _ => rfl)
(fun _ _ => rfl)
-- Prefer subclasses of `Monoid` over subclasses of `SubmonoidClass`.
