English
If two monoid structures have the same multiplication, then they are equal.
Русский
Если две моноидальные структуры имеют одинаковую операцию умножения, то они равны.
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₂ : Monoid M⦄
(h_mul :
(letI := m₁;
HMul.hMul :
M → M → M) =
(letI := m₂;
HMul.hMul :
M → M → M)) :
m₁ = m₂ := by
have : m₁.toMulOneClass = m₂.toMulOneClass := MulOneClass.ext h_mul
have h₁ : m₁.one = m₂.one := congr_arg (·.one) this
let f : @MonoidHom M M m₁.toMulOne m₂.toMulOne :=
@MonoidHom.mk _ _ (_) _ (@OneHom.mk _ _ (_) _ id h₁) (fun x y => congr_fun (congr_fun h_mul x) y)
have : m₁.npow = m₂.npow := by
ext n x
exact @MonoidHom.map_pow M M m₁ m₂ f x n
rcases m₁ with @⟨@⟨⟨_⟩⟩, ⟨_⟩⟩
congr
