associator_op — Mathlib

English

A simplification for associator on opposite ring elements: associator x y z = -op (associator (unop z) (unop y) (unop x)).

Русский

Упрощение выражения для ассоциатора на элементах противоположного кольца: associator x y z = -op (associator (unop z) (unop y) (unop x)).

LaTeX

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

Lean4

@[simp]
theorem associator_op (x y z : Rᵐᵒᵖ) : associator x y z = -op (associator (unop z) (unop y) (unop x)) := by
  simp only [associator_apply, ← unop_mul, ← unop_sub, op_unop, neg_sub]

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