English
The action of enveloping group elements on the rack agrees with the rack operation, i.e., envelAction(toEnvelGroup R x) y = x ◃ y.
Русский
Действие элементов обобщающей группы на раке согласуется с операцией рака: envelAction(toEnvelGroup R x) y = x ◃ y.
LaTeX
$$$\\mathrm{envelAction} (\\mathrm{toEnvelGroup}\\ R\ \\, x)\, y = x \\triangleleft y.$$$
Lean4
@[simp]
theorem envelAction_prop {R : Type*} [Rack R] (x y : R) : envelAction (toEnvelGroup R x) y = x ◃ y :=
rfl