self_invAct_act_eq — Mathlib

English

The inverse-self action composed with a right action yields the same outcome: (x ◃⁻¹ x) ◃ y = x ◃ y.

Русский

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

LaTeX

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

Lean4

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

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