associator_cocycle — Mathlib

English

For a nonunital nonassoc ring R, the associator on the opposite ring equals a negated and opposite of the associator on the original ring.

Русский

Для кольца без единицы и без ассоциативности над противоположным кольцом ассоциатор равен отрицанию и противоположному умножению относительно исходного кольца.

LaTeX

$$$\\text{associator}(x,y,z) = -\\mathrm{op}(\\text{associator}(\\mathrm{unop}(z),\\mathrm{unop}(y),\\mathrm{unop}(x)))$$$

Lean4

theorem associator_cocycle (a b c d : R) :
    a * associator b c d - associator (a * b) c d + associator a (b * c) d - associator a b (c * d) +
        (associator a b c) * d =
      0 :=
  by
  simp only [associator, mul_sub, sub_mul]
  abel1

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