inducedOrderRingIso — Mathlib

English

There exists a unique order-preserving ring isomorphism between β and γ.

Русский

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

LaTeX

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

Lean4

/-- The isomorphism of ordered rings between two conditionally complete linearly ordered fields. -/
def inducedOrderRingIso : β ≃+*o γ :=
  { inducedOrderRingHom β γ with
    invFun := inducedMap γ β
    left_inv := inducedMap_inv_self _ _
    right_inv := inducedMap_inv_self _ _
    map_le_map_iff' := by
      dsimp
      refine ⟨fun h => ?_, fun h => inducedMap_mono _ _ h⟩
      convert inducedMap_mono γ β h <;>
        · rw [inducedOrderRingHom, AddMonoidHom.coe_fn_mkRingHomOfMulSelfOfTwoNeZero, inducedAddHom]
          dsimp
          rw [inducedMap_inv_self β γ _] }

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