English
The adjoint action ad_conj states that act'(x ◃ y) equals act'(x) act'(y) act'(x)^{-1}, i.e., the adjoint action is given by conjugation of the two actions.
Русский
Сопряжённое действие ad_conj: act'(x ◃ y) = act'(x) act'(y) act'(x)^{-1}, то есть adjoint-действие задаётся конъюгацией.
LaTeX
$$$\text{act}'(x \triangleleft y) = \text{act}' x \cdot \text{act}' y \cdot (\text{act}' x)^{-1}$$$
Lean4
/-- The *adjoint action* of a rack on itself is `op'`, and the adjoint
action of `x ◃ y` is the conjugate of the action of `y` by the action
of `x`. It is another way to understand the self-distributivity axiom.
This is used in the natural rack homomorphism `toConj` from `R` to
`Conj (R ≃ R)` defined by `op'`.
-/
theorem ad_conj {R : Type*} [Rack R] (x y : R) : act' (x ◃ y) = act' x * act' y * (act' x)⁻¹ :=
by
rw [eq_mul_inv_iff_mul_eq]; ext z
apply self_distrib.symm
