assoc_iff_id — Mathlib

English

For any rack R and x,y,z, x ◃ y ◃ z = (x ◃ y) ◃ z if and only if x ◃ z = z.

Русский

Для любого рака R и элементов x,y,z выполнено: x ◃ y ◃ z = (x ◃ y) ◃ z тогда и только тогда, когда x ◃ z = z.

LaTeX

$$$x \triangleleft y \triangleleft z = (x \triangleleft y) \triangleleft z \iff x \triangleleft z = z$$$

Lean4

/-- Associative racks are uninteresting.
-/
theorem assoc_iff_id {R : Type*} [Rack R] {x y z : R} : x ◃ y ◃ z = (x ◃ y) ◃ z ↔ x ◃ z = z :=
  by
  rw [self_distrib]
  rw [left_cancel]

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