English
If a homomorphism g: EnvelGroup(R) →* G fits the same triangle with f, then g equals toEnvelGroup.map f.
Русский
Если гомоморфизм g: EnvelGroup(R) →* G удовлетворяет той же треугольной диаграмме, что и f, то g = toEnvelGroup.map f.
LaTeX
$$$\text{If } f = (\mathrm{Conj.map}\ g) \circ (\mathrm{toEnvelGroup}\ R),\ then\ g = (\mathrm{toEnvelGroup.map}\ f).$$$
Lean4
/-- The induced group homomorphism from the enveloping group into bijections of the rack,
using `Rack.toConj`. Satisfies the property `envelAction_prop`.
This gives the rack `R` the structure of an augmented rack over `EnvelGroup R`.
-/
def envelAction {R : Type*} [Rack R] : EnvelGroup R →* R ≃ R :=
toEnvelGroup.map (toConj R)
