mulLeft₃_eq_mulRight₃

Mathlib.Algebra.Ring.Associator

URI: https://scilib.ai/kg/mathlib#AddMonoidHom.mulLeft₃_eq_mulRight₃

English

In a nonunital semiring R, the left and right three-fold multiplications agree: mulLeft₃ = mulRight₃.

Русский

В полугруппе без единицы R левые и правые троичные умножения совпадают: mulLeft₃ = mulRight₃.

LaTeX

$$$mulLeft_3\,(R := R) = mulRight_3$$$

Lean4

theorem mulLeft₃_eq_mulRight₃ : mulLeft₃ (R := R) = mulRight₃ :=
  mulLeft₃_eq_mulRight₃_iff_associative.2 inferInstance

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

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

Разделы

Аффилиация

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