subsingleton_right — Mathlib

English

There is a subsingleton instance for FiniteMulArchimedeanClass M given MulArchimedean M.

Русский

Существует экземпляр subsingleton для FiniteMulArchimedeanClass M при условии MulArchimedean M.

LaTeX

$$$\text{Subsingleton } (FiniteMulArchimedeanClass M)$$$

Lean4

/-- There is at most one ordered ring isomorphism between a linear ordered field and an archimedean
linear ordered field. -/
instance subsingleton_right [IsStrictOrderedRing β] [Archimedean β] : Subsingleton (α ≃+*o β) :=
  OrderRingIso.toOrderRingHom_injective.subsingleton

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