self_distrib_inv — Mathlib

English

For all x,y,z in the rack, x ◃⁻¹ y ◃⁻¹ z = (x ◃⁻¹ y) ◃⁻¹ x ◃⁻¹ z, i.e., inverse action distributes with respect to itself.

Русский

Для всех x,y,z в раке верно x ◃⁻¹ y ◃⁻¹ z = (x ◃⁻¹ y) ◃⁻¹ x ◃⁻¹ z, то есть обратное действие самораспределимо.

LaTeX

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

Lean4

theorem self_distrib_inv {x y z : R} : x ◃⁻¹ y ◃⁻¹ z = (x ◃⁻¹ y) ◃⁻¹ x ◃⁻¹ z :=
  by
  rw [← left_cancel (x ◃⁻¹ y), right_inv, ← left_cancel x, right_inv, self_distrib]
  repeat' rw [right_inv]

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