uniqueOrderRingHom — Mathlib

English

There exists a unique ordered ring homomorphism from α to β.

Русский

Существует единственный упорядоченный кольцевой гомоморфизм из α в β.

LaTeX

$$$ \exists! f: \alpha \to+*o \beta $$$

Lean4

/-- There is a unique ordered ring homomorphism from an archimedean linear ordered field to a
conditionally complete linear ordered field. -/
instance uniqueOrderRingHom : Unique (α →+*o β) :=
  uniqueOfSubsingleton <| inducedOrderRingHom α β

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