English
From an element of a submonoid-like class S into M, one obtains the submonoid of M whose carrier is exactly the element considered as a set.
Русский
Из элемента класса S, представляющего подмономоиду, получаем подмономод M, чей носитель равен элементу как множеству.
LaTeX
$$$$ \\text{ofClass}(s) \\text{ defines a Submonoid of } M \\text{ with carrier } s $$$$
Lean4
/-- The actual `Submonoid` obtained from an element of a `SubmonoidClass` -/
@[to_additive (attr := simps) /-- The actual `AddSubmonoid` obtained from an element of a
`AddSubmonoidClass` -/
]
def ofClass {S M : Type*} [Monoid M] [SetLike S M] [SubmonoidClass S M] (s : S) : Submonoid M :=
⟨⟨s, MulMemClass.mul_mem⟩, OneMemClass.one_mem s⟩
