mk_injective — Mathlib

English

If all units of M are the same (Units(M) is subsingleton), then mk: M → Associates(M) is injective.

Русский

Если все элементы единицы в M совпадают (Units(M) является подвх), то mk: M → Associates(M) инъективно.

LaTeX

$$$ [\text{Subsingleton}(\operatorname{Units}(M))] \Rightarrow \text{Function.Injective}(\operatorname{Associates.mk}) $$$

Lean4

theorem mk_injective [Monoid M] [Subsingleton Mˣ] : Function.Injective (@Associates.mk M _) := fun _ _ h =>
  associated_iff_eq.mp (Associates.mk_eq_mk_iff_associated.mp h)

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