envelAction_prop — Mathlib

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

Похожие утверждения