assoc_symm — Mathlib

English

In a RightPreLie ring, the associator is symmetric in the last two arguments: associator(x,y,z) = associator(x,z,y).

Русский

В правом пред-структурном кольце ассоциатор симметричен относительно последних двух аргументов: associator(x,y,z) = associator(x,z,y).

LaTeX

$$$$\operatorname{associator}(x,y,z) = \operatorname{associator}(x,z,y).$$$$

Lean4

theorem assoc_symm (x y z : L) : associator x y z = associator x z y :=
  RightPreLieRing.assoc_symm' x y z

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