English
The actual Subgroup obtained from an element of a SubgroupClass is given by ofClass s.
Русский
Фактическая подгруппа, получаемая из элемента SubgroupClass, задаётся через ofClass s.
LaTeX
$$$$ \\mathrm{Subgroup.ofClass}(s) = \\langle \\langle s, \\text{MulMemClass.mul_mem} \\rangle, \\text{OneMemClass.one_mem } s \\rangle, \\text{InvMemClass.inv_mem} \\rangle. $$$$
Lean4
/-- The actual `Subgroup` obtained from an element of a `SubgroupClass` -/
@[to_additive (attr := simps) /-- The actual `AddSubgroup` obtained from an element of a
`AddSubgroupClass` -/
]
def ofClass {S G : Type*} [Group G] [SetLike S G] [SubgroupClass S G] (s : S) : Subgroup G :=
⟨⟨⟨s, MulMemClass.mul_mem⟩, OneMemClass.one_mem s⟩, InvMemClass.inv_mem⟩
