associator_eq_zero

Mathlib.Algebra.Ring.Associator

URI: https://scilib.ai/kg/mathlib#AddMonoidHom.associator_eq_zero

English

For a (not necessarily unital) ring, the associator vanishes: associator (R := R) = 0, i.e., multiplication is associative.

Русский

Для кольца без единицы ассоциатор обращается в ноль; то есть умножение ассоциативно.

LaTeX

$$$\operatorname{associator}(R) = 0$$$

Lean4

@[simp]
theorem associator_eq_zero : associator (R := R) = 0 :=
  associator_eq_zero_iff_associative.mpr inferInstance

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru