act_invAct_eq — Mathlib

English

For all x,y, x ◃ x ◃⁻¹ y = x ◃⁻¹ y, expressing cancellation of a self-action with its inverse.

Русский

Для всех x,y выполняется x ◃ x ◃⁻¹ y = x ◃⁻¹ y, отображающее исчезновение двойного действия и обратного действия.

LaTeX

$$$x \triangleleft x \triangleleft^{-1} y = x \triangleleft^{-1} y$$$

Lean4

@[simp]
theorem act_invAct_eq (x y : R) : x ◃ x ◃⁻¹ y = y :=
  right_inv x y

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