ext — Mathlib

English

Two RightCancelMonoid structures are equal if their multiplications agree.

Русский

Две структуры RightCancelMonoid равны, если их умножения совпадают.

LaTeX

$$$(\\forall x,y \in M), x *_{m_1} y = x *_{m_2} y \Rightarrow m_1 = m_2$$$

Lean4

@[to_additive (attr := ext)]
theorem ext {M : Type u} ⦃m₁ m₂ : LeftCancelMonoid M⦄
    (h_mul :
      (letI := m₁;
          HMul.hMul :
          M → M → M) =
        (letI := m₂;
          HMul.hMul :
          M → M → M)) :
    m₁ = m₂ :=
  LeftCancelMonoid.toMonoid_injective <| Monoid.ext h_mul

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