inducedOrderRingIso_symm — Mathlib

English

There is a unique ordered ring isomorphism between any pair of conditionally complete linear ordered fields.

Русский

Существует единственный упорядоченный кольцевой изоморфизм между любой парой условно полноценных линейно упорядоченных полей.

LaTeX

$$$ \exists! \phi: \beta \simeq_{o} \gamma $$$

Lean4

@[simp]
theorem inducedOrderRingIso_symm : (inducedOrderRingIso β γ).symm = inducedOrderRingIso γ β :=
  rfl

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