English
For any rack R, the enveloping group EnvelGroup(R) is equipped with a group structure extending the rack operation, i.e., EnvelGroup(R) is a group.
Русский
Для любого рака (rack) R образуется обобщающая (оболочка) группа EnvelGroup(R) с групповой структурой, расширяющей раковую операцию.
LaTeX
$$$\mathrm{EnvelGroup}(R) \text{ is a group with multiplication } \cdot, \ e, \cdot^{-1}.$$$
Lean4
instance (R : Type*) [Rack R] : Group (EnvelGroup R) :=
{ inv_mul_cancel := fun a => Quotient.inductionOn a fun a => Quotient.sound (PreEnvelGroupRel'.inv_mul_cancel a).rel }