associator_eq_zero_iff_associative

English

An a priori non-associative ring is associative iff its associator vanishes. Equivalently, the ring satisfies (x*y)*z = x*(y*z) for all x,y,z.

Русский

Пусть кольцо без единицы и неассоциативно; оно ассоциативно тогда и только тогда, когда ассоциатор обращается в ноль. Эквивалентно тем же равенствам (x·y)·z = x·(y·z) для всех x,y,z.

LaTeX

$$$\operatorname{associator}(R) = 0 \iff \forall x,y,z \in R,\ (x\cdot y)\cdot z = x\,(y\cdot z).$$$

Lean4

/-- An a priori non-associative ring is associative iff the `AddMonoidHom` version of the
associator vanishes. -/
theorem associator_eq_zero_iff_associative : associator (R := R) = 0 ↔ Std.Associative (fun (x y : R) ↦ x * y) := by
  simp [mulLeft₃_eq_mulRight₃_iff_associative, associator, sub_eq_zero]

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