associator_eq_zero_iff_associative

English

In a nonunital nonassoc ring, the associator satisfies a cocycle identity: a certain linear combination of products involving associator equals zero.

Русский

В кольце без единицы и без ассоциативности выполняется кокаталитическое тождество для ассоциатора: заданная линейная комбинация произведений с участием ассоциатора равна нулю.

LaTeX

$$$a \\cdot \\text{associator}(b,c,d) - \\text{associator}(a b,c,d) + \\text{associator}(a,b c,d) - \\text{associator}(a,b, c d) + \\text{associator}(a,b,c) \\cdot d = 0$$$

Lean4

theorem associator_eq_zero_iff_associative : associator (R := R) = 0 ↔ Std.Associative (fun (x y : R) ↦ x * y)
    where
  mp h := ⟨fun x y z ↦ sub_eq_zero.mp <| congr_fun₃ h x y z⟩
  mpr h := by ext x y z; simp [associator, Std.Associative.assoc]

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