mk_injective — Mathlib

English

If α is a commutative monoid, ConjClasses.mk is injective.

Русский

Если α — коммутативный моноид, отображение mk из α в ConjClasses α инъективно.

LaTeX

$$$\text{Injective}(\mathrm{ConjClasses.mk})$ for commutative monoids: ∀ a,b, \mathrm{ConjClasses.mk}(a) = \mathrm{ConjClasses.mk}(b) \Rightarrow a=b.$$

Lean4

theorem mk_injective : Function.Injective (@ConjClasses.mk α _) := fun _ _ =>
  (mk_eq_mk_iff_isConj.trans isConj_iff_eq).1

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