self_invAct_invAct_eq — Mathlib

English

The inverse-self-application is stable under left action: (x ◃⁻¹ x) ◃⁻¹ y = x ◃⁻¹ y.

Русский

Левостороннее применение с обратным действием стабильно: (x ◃⁻¹ x) ◃⁻¹ y = x ◃⁻¹ y.

LaTeX

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

Lean4

@[simp]
theorem self_invAct_invAct_eq {x y : R} : (x ◃⁻¹ x) ◃⁻¹ y = x ◃⁻¹ y :=
  by
  have h := @self_act_act_eq _ _ (op x) (op y)
  simpa using h

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