mul_comm — Mathlib

English

If two unital binary operations distribute in the required way, the second operation is commutative.

Русский

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

LaTeX

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

Lean4

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

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

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