mul — Mathlib

English

Under the same hypotheses as the previous statement, the two binary operations are equal: m1 = m2.

Русский

При тех же предположениях две бинарные операции совпадают: m1 = m2.

LaTeX

$$$m_1 = m_2$$$

Lean4

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

In fact, they give a commutative monoid structure, see `eckmann_hilton.CommMonoid`. -/
theorem mul : m₁ = m₂ := by
  funext a b
  calc
    m₁ a b = m₁ (m₂ a e₁) (m₂ e₁ b) := by { simp only [one h₁ h₂ distrib, h₂.left_id, h₂.right_id]
    }
    _ = m₂ a b := by simp only [distrib, h₁.left_id, h₁.right_id]

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