mul_assoc — Mathlib

English

If X has two unital binary operations that distribute over each other, then the second operation is associative.

Русский

Если X имеет две единичные бинарные операции, которые дистрибутивны друг над другом, то вторая операция ассоциативна.

LaTeX

$$$\\forall a,b,c\\in X,\\ m_2(m_2(a,b),c)=m_2(a,m_2(b,c))$$$

Lean4

/-- If a type carries two unital binary operations that distribute over each other,
then these operations are associative.

In fact, they give a commutative monoid structure, see `eckmann_hilton.CommMonoid`. -/
theorem mul_assoc : Std.Associative m₂ :=
  ⟨fun a b c => by simpa [mul h₁ h₂ distrib, h₂.left_id, h₂.right_id] using distrib a b e₂ c⟩

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