Conditionally complete linear ordered fields

This file shows that the reals are unique, or, more formally, given a type satisfying the common axioms of the reals (field, conditionally complete, linearly ordered) that there is an isomorphism preserving these properties to the reals. This is ConditionallyCompleteLinearOrderedField.inducedOrderRingIso. Moreover this isomorphism is unique.

We show all conditionally complete linear ordered fields are archimedean. We also construct the natural map from a LinearOrderedField to such a field.

Main definitions

• ConditionallyCompleteLinearOrderedField.inducedMap: A (unique) map from any archimedean linear ordered field to a conditionally complete linear ordered field. Various bundlings are available.

Main results

• ConditionallyCompleteLinearOrderedField.uniqueOrderRingHom : Uniqueness of OrderRingHoms from an archimedean linear ordered field to a conditionally complete linear ordered field.
• ConditionallyCompleteLinearOrderedField.uniqueOrderRingIso : Uniqueness of OrderRingIsos between two conditionally complete linearly ordered fields.

References

• https://mathoverflow.net/questions/362991/who-first-characterized-the-real-numbers-as-the-unique-complete-ordered-field

Tags

reals, conditionally complete, ordered field, uniqueness

@[deprecated "Use `[Field α] [ConditionallyCompleteLinearOrder α] [IsStrictOrderedRing α]` instead." (since := "2026-02-23")]

structure ConditionallyCompleteLinearOrderedField (α : Type u_5) extends Field α, ConditionallyCompleteLinearOrder α, IsStrictOrderedRing α : Type u_5

A field which is both linearly ordered and conditionally complete with respect to the order. This axiomatizes the reals.

• add : α → α → α
• add_assoc (a b c : α) : a + b + c = a + (b + c)
• zero : α
• zero_add (a : α) : 0 + a = a
• add_zero (a : α) : a + 0 = a
• nsmul : ℕ → α → α
• nsmul_zero (x : α) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : α) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : α) : a + b = b + a
• mul : α → α → α
• left_distrib (a b c : α) : a * (b + c) = a * b + a * c
• right_distrib (a b c : α) : (a + b) * c = a * c + b * c
• zero_mul (a : α) : 0 * a = 0
• mul_zero (a : α) : a * 0 = 0
• mul_assoc (a b c : α) : a * b * c = a * (b * c)
• one : α
• one_mul (a : α) : 1 * a = a
• mul_one (a : α) : a * 1 = a
• natCast : ℕ → α
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → α → α
• npow_zero (x : α) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : α) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg (a b : α) : a - b = a + -b
• zsmul : ℤ → α → α
• zsmul_zero' (a : α) : Ring.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : α) : Ring.zsmul (↑n.succ) a = Ring.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : α) : Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• neg_add_cancel (a : α) : -a + a = 0
• intCast : ℤ → α
• intCast_ofNat (n : ℕ) : IntCast.intCast ↑n = ↑n
• intCast_negSucc (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• mul_comm (a b : α) : a * b = b * a
• inv : α → α
• div : α → α → α
• div_eq_mul_inv (a b : α) : a / b = a * b⁻¹
• zpow : ℤ → α → α
• zpow_zero' (a : α) : Field.zpow 0 a = 1
• zpow_succ' (n : ℕ) (a : α) : Field.zpow (↑n.succ) a = Field.zpow (↑n) a * a
• zpow_neg' (n : ℕ) (a : α) : Field.zpow (Int.negSucc n) a = (Field.zpow (↑n.succ) a)⁻¹
• exists_pair_ne : ∃ (x : α) (y : α), x ≠ y
• nnratCast : ℚ≥0 → α
• ratCast : ℚ → α
• mul_inv_cancel (a : α) : a ≠ 0 → a * a⁻¹ = 1
• inv_zero : 0⁻¹ = 0
• nnratCast_def (q : ℚ≥0) : ↑q = ↑q.num / ↑q.den
• nnqsmul : ℚ≥0 → α → α
• nnqsmul_def (q : ℚ≥0) (a : α) : Field.nnqsmul q a = ↑q * a
• ratCast_def (q : ℚ) : ↑q = ↑q.num / ↑q.den
• qsmul : ℚ → α → α
• qsmul_def (a : ℚ) (x : α) : Field.qsmul a x = ↑a * x
• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_ge (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• sup : α → α → α
• le_sup_left (a b : α) : a ≤ sup a b
• le_sup_right (a b : α) : b ≤ sup a b
• sup_le (a b c : α) : a ≤ c → b ≤ c → sup a b ≤ c
• inf : α → α → α
• inf_le_left (a b : α) : Lattice.inf a b ≤ a
• inf_le_right (a b : α) : Lattice.inf a b ≤ b
• le_inf (a b c : α) : a ≤ b → a ≤ c → a ≤ Lattice.inf b c
• sSup : Set α → α
• sInf : Set α → α
• isLUB_csSup (s : Set α) : s.Nonempty → BddAbove s → IsLUB s (sSup s)
• isGLB_csInf (s : Set α) : s.Nonempty → BddBelow s → IsGLB s (sInf s)
• compare : α → α → Ordering
• le_total (a b : α) : a ≤ b ∨ b ≤ a
• toDecidableLE : DecidableLE α
• toDecidableEq : DecidableEq α
• toDecidableLT : DecidableLT α
• csSup_of_not_bddAbove (s : Set α) : ¬BddAbove s → sSup s = sSup ∅
• csInf_of_not_bddBelow (s : Set α) : ¬BddBelow s → sInf s = sInf ∅
• compare_eq_compareOfLessAndEq (a b : α) : compare a b = compareOfLessAndEq a b
• add_le_add_left (a b : α) : a ≤ b → ∀ (c : α), a + c ≤ b + c
• add_le_add_right (a b : α) : a ≤ b → ∀ (c : α), c + a ≤ c + b
• le_of_add_le_add_left (a b c : α) : a + b ≤ a + c → b ≤ c
• le_of_add_le_add_right (a b c : α) : b + a ≤ c + a → b ≤ c
• zero_le_one : 0 ≤ 1
• mul_lt_mul_of_pos_left ⦃a : α⦄ (ha : 0 < a) ⦃b c : α⦄ (hbc : b < c) : a * b < a * c
• mul_lt_mul_of_pos_right ⦃c : α⦄ (hc : 0 < c) ⦃a b : α⦄ (hab : a < b) : a * c < b * c

theorem ConditionallyCompleteLinearOrderedField.to_archimedean {α : Type u_2} [Field α] [ConditionallyCompleteLinearOrder α] [IsStrictOrderedRing α] : Archimedean α

Any conditionally complete linearly ordered field is archimedean.

Rational cut map

The idea is that a conditionally complete linear ordered field is fully characterized by its copy of the rationals. Hence we define LinearOrderedField.cutMap β : α → Set β which sends a : α to the "rationals in β" that are less than a.

def LinearOrderedField.cutMap {α : Type u_2} (β : Type u_3) [Field α] [LinearOrder α] [DivisionRing β] (a : α) : Set β

The lower cut of rationals inside a linear ordered field that are less than a given element of another linear ordered field.

theorem LinearOrderedField.cutMap_mono {α : Type u_2} (β : Type u_3) [Field α] [LinearOrder α] [DivisionRing β] {a₁ a₂ : α} (h : a₁ ≤ a₂) : cutMap β a₁ ⊆ cutMap β a₂

@[simp]

theorem LinearOrderedField.mem_cutMap_iff {α : Type u_2} {β : Type u_3} [Field α] [LinearOrder α] [DivisionRing β] {a : α} {b : β} : b ∈ cutMap β a ↔ ∃ (q : ℚ), ↑q < a ∧ ↑q = b

theorem LinearOrderedField.coe_mem_cutMap_iff {α : Type u_2} {β : Type u_3} [Field α] [LinearOrder α] [DivisionRing β] {a : α} {q : ℚ} [CharZero β] : ↑q ∈ cutMap β a ↔ ↑q < a

theorem LinearOrderedField.cutMap_self {α : Type u_2} [Field α] [LinearOrder α] (a : α) : cutMap α a = Set.Iio a ∩ Set.range Rat.cast

theorem LinearOrderedField.cutMap_coe {α : Type u_2} (β : Type u_3) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [LinearOrder β] [IsStrictOrderedRing β] (q : ℚ) : cutMap β ↑q = Rat.cast '' {r : ℚ | ↑r < ↑q}

theorem LinearOrderedField.cutMap_nonempty {α : Type u_2} (β : Type u_3) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [Archimedean α] (a : α) : (cutMap β a).Nonempty

theorem LinearOrderedField.cutMap_bddAbove {α : Type u_2} (β : Type u_3) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [LinearOrder β] [IsStrictOrderedRing β] [Archimedean α] (a : α) : BddAbove (cutMap β a)

theorem LinearOrderedField.cutMap_add {α : Type u_2} (β : Type u_3) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [LinearOrder β] [IsStrictOrderedRing β] [Archimedean α] (a b : α) : cutMap β (a + b) = cutMap β a + cutMap β b

Induced map

LinearOrderedField.cutMap spits out a Set β. To get something in β, we now take the supremum.

def ConditionallyCompleteLinearOrderedField.inducedMap (α : Type u_2) (β : Type u_3) [Field α] [LinearOrder α] [Field β] [ConditionallyCompleteLinearOrder β] (x : α) : β

The induced order-preserving function from a linear ordered field to a conditionally complete linear ordered field, defined by taking the Sup in the codomain of all the rationals less than the input.

theorem ConditionallyCompleteLinearOrderedField.inducedMap_mono (α : Type u_2) (β : Type u_3) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] : Monotone (inducedMap α β)

theorem ConditionallyCompleteLinearOrderedField.inducedMap_rat (α : Type u_2) (β : Type u_3) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] (q : ℚ) : inducedMap α β ↑q = ↑q

@[simp]

theorem ConditionallyCompleteLinearOrderedField.inducedMap_zero (α : Type u_2) (β : Type u_3) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] : inducedMap α β 0 = 0

@[simp]

theorem ConditionallyCompleteLinearOrderedField.inducedMap_one (α : Type u_2) (β : Type u_3) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] : inducedMap α β 1 = 1

theorem ConditionallyCompleteLinearOrderedField.inducedMap_nonneg {α : Type u_2} {β : Type u_3} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] {a : α} (ha : 0 ≤ a) : 0 ≤ inducedMap α β a

theorem ConditionallyCompleteLinearOrderedField.coe_lt_inducedMap_iff {α : Type u_2} {β : Type u_3} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] {a : α} {q : ℚ} : ↑q < inducedMap α β a ↔ ↑q < a

theorem ConditionallyCompleteLinearOrderedField.lt_inducedMap_iff {α : Type u_2} {β : Type u_3} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] {a : α} {b : β} : b < inducedMap α β a ↔ ∃ (q : ℚ), b < ↑q ∧ ↑q < a

@[simp]

theorem ConditionallyCompleteLinearOrderedField.inducedMap_self {β : Type u_3} [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] (b : β) : inducedMap β β b = b

@[simp]

theorem ConditionallyCompleteLinearOrderedField.inducedMap_inducedMap (α : Type u_2) (β : Type u_3) (γ : Type u_4) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Field γ] [ConditionallyCompleteLinearOrder γ] [IsStrictOrderedRing γ] [Archimedean α] (a : α) : inducedMap β γ (inducedMap α β a) = inducedMap α γ a

theorem ConditionallyCompleteLinearOrderedField.inducedMap_inv_self (β : Type u_3) (γ : Type u_4) [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Field γ] [ConditionallyCompleteLinearOrder γ] [IsStrictOrderedRing γ] (b : β) : inducedMap γ β (inducedMap β γ b) = b

theorem ConditionallyCompleteLinearOrderedField.inducedMap_add (α : Type u_2) (β : Type u_3) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] (x y : α) : inducedMap α β (x + y) = inducedMap α β x + inducedMap α β y

theorem ConditionallyCompleteLinearOrderedField.le_inducedMap_mul_self_of_mem_cutMap {α : Type u_2} {β : Type u_3} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] {a : α} (ha : 0 < a) (b : β) (hb : b ∈ LinearOrderedField.cutMap β (a * a)) : b ≤ inducedMap α β a * inducedMap α β a

Preparatory lemma for inducedOrderRingHom.

theorem ConditionallyCompleteLinearOrderedField.exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self {α : Type u_2} {β : Type u_3} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] {a : α} (ha : 0 < a) (b : β) (hba : b < inducedMap α β a * inducedMap α β a) : ∃ c ∈ LinearOrderedField.cutMap β (a * a), b < c

Preparatory lemma for inducedOrderRingHom.

def ConditionallyCompleteLinearOrderedField.inducedAddHom (α : Type u_2) (β : Type u_3) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] : α →+ β

inducedMap as an additive homomorphism.

def ConditionallyCompleteLinearOrderedField.inducedOrderRingHom (α : Type u_2) (β : Type u_3) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] : α →+*o β

inducedMap as an OrderRingHom.

@[simp]

theorem ConditionallyCompleteLinearOrderedField.inducedOrderRingHom_toFun (α : Type u_2) (β : Type u_3) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] (a✝ : α) : (inducedOrderRingHom α β) a✝ = (inducedAddHom α β) a✝

def ConditionallyCompleteLinearOrderedField.inducedOrderRingIso (β : Type u_3) (γ : Type u_4) [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Field γ] [ConditionallyCompleteLinearOrder γ] [IsStrictOrderedRing γ] : β ≃+*o γ

The isomorphism of ordered rings between two conditionally complete linearly ordered fields.

@[simp]

theorem ConditionallyCompleteLinearOrderedField.coe_inducedOrderRingIso (β : Type u_3) (γ : Type u_4) [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Field γ] [ConditionallyCompleteLinearOrder γ] [IsStrictOrderedRing γ] : ⇑(inducedOrderRingIso β γ) = inducedMap β γ

@[simp]

theorem ConditionallyCompleteLinearOrderedField.inducedOrderRingIso_symm (β : Type u_3) (γ : Type u_4) [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Field γ] [ConditionallyCompleteLinearOrder γ] [IsStrictOrderedRing γ] : (inducedOrderRingIso β γ).symm = inducedOrderRingIso γ β

@[simp]

theorem ConditionallyCompleteLinearOrderedField.inducedOrderRingIso_self (β : Type u_3) [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] : inducedOrderRingIso β β = OrderRingIso.refl β

@[implicit_reducible]

def ConditionallyCompleteLinearOrderedField.uniqueOrderRingHom (α : Type u_2) (β : Type u_3) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] : Unique (α →+*o β)

There is a unique ordered ring homomorphism from an archimedean linear ordered field to a conditionally complete linear ordered field.

@[implicit_reducible]

def ConditionallyCompleteLinearOrderedField.uniqueOrderRingIso (β : Type u_3) (γ : Type u_4) [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Field γ] [ConditionallyCompleteLinearOrder γ] [IsStrictOrderedRing γ] : Unique (β ≃+*o γ)

There is a unique ordered ring isomorphism between two conditionally complete linear ordered fields.

@[deprecated ConditionallyCompleteLinearOrderedField.inducedMap (since := "2026-02-24")]

def LinearOrderedField.inducedMap (α : Type u_2) (β : Type u_3) [Field α] [LinearOrder α] [Field β] [ConditionallyCompleteLinearOrder β] (x : α) : β

Alias of ConditionallyCompleteLinearOrderedField.inducedMap.

---

The induced order-preserving function from a linear ordered field to a conditionally complete linear ordered field, defined by taking the Sup in the codomain of all the rationals less than the input.

@[deprecated ConditionallyCompleteLinearOrderedField.inducedMap_mono (since := "2026-02-24")]

theorem LinearOrderedField.inducedMap_mono (α : Type u_2) (β : Type u_3) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] : Monotone (ConditionallyCompleteLinearOrderedField.inducedMap α β)

Alias of ConditionallyCompleteLinearOrderedField.inducedMap_mono.

@[deprecated ConditionallyCompleteLinearOrderedField.inducedMap_rat (since := "2026-02-24")]

theorem LinearOrderedField.inducedMap_rat (α : Type u_2) (β : Type u_3) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] (q : ℚ) : ConditionallyCompleteLinearOrderedField.inducedMap α β ↑q = ↑q

Alias of ConditionallyCompleteLinearOrderedField.inducedMap_rat.

@[deprecated ConditionallyCompleteLinearOrderedField.inducedMap_zero (since := "2026-02-24")]

theorem LinearOrderedField.inducedMap_zero (α : Type u_2) (β : Type u_3) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] : ConditionallyCompleteLinearOrderedField.inducedMap α β 0 = 0

Alias of ConditionallyCompleteLinearOrderedField.inducedMap_zero.

@[deprecated ConditionallyCompleteLinearOrderedField.inducedMap_one (since := "2026-02-24")]

theorem LinearOrderedField.inducedMap_one (α : Type u_2) (β : Type u_3) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] : ConditionallyCompleteLinearOrderedField.inducedMap α β 1 = 1

Alias of ConditionallyCompleteLinearOrderedField.inducedMap_one.

@[deprecated ConditionallyCompleteLinearOrderedField.inducedMap_nonneg (since := "2026-02-24")]

theorem LinearOrderedField.inducedMap_nonneg {α : Type u_2} {β : Type u_3} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] {a : α} (ha : 0 ≤ a) : 0 ≤ ConditionallyCompleteLinearOrderedField.inducedMap α β a

Alias of ConditionallyCompleteLinearOrderedField.inducedMap_nonneg.

@[deprecated ConditionallyCompleteLinearOrderedField.coe_lt_inducedMap_iff (since := "2026-02-24")]

theorem LinearOrderedField.coe_lt_inducedMap_iff {α : Type u_2} {β : Type u_3} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] {a : α} {q : ℚ} : ↑q < ConditionallyCompleteLinearOrderedField.inducedMap α β a ↔ ↑q < a

Alias of ConditionallyCompleteLinearOrderedField.coe_lt_inducedMap_iff.

@[deprecated ConditionallyCompleteLinearOrderedField.lt_inducedMap_iff (since := "2026-02-24")]

theorem LinearOrderedField.lt_inducedMap_iff {α : Type u_2} {β : Type u_3} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] {a : α} {b : β} : b < ConditionallyCompleteLinearOrderedField.inducedMap α β a ↔ ∃ (q : ℚ), b < ↑q ∧ ↑q < a

Alias of ConditionallyCompleteLinearOrderedField.lt_inducedMap_iff.

@[deprecated ConditionallyCompleteLinearOrderedField.inducedMap_self (since := "2026-02-24")]

theorem LinearOrderedField.inducedMap_self {β : Type u_3} [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] (b : β) : ConditionallyCompleteLinearOrderedField.inducedMap β β b = b

Alias of ConditionallyCompleteLinearOrderedField.inducedMap_self.

@[deprecated ConditionallyCompleteLinearOrderedField.inducedMap_inducedMap (since := "2026-02-24")]

theorem LinearOrderedField.inducedMap_inducedMap (α : Type u_2) (β : Type u_3) (γ : Type u_4) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Field γ] [ConditionallyCompleteLinearOrder γ] [IsStrictOrderedRing γ] [Archimedean α] (a : α) : ConditionallyCompleteLinearOrderedField.inducedMap β γ (ConditionallyCompleteLinearOrderedField.inducedMap α β a) = ConditionallyCompleteLinearOrderedField.inducedMap α γ a

Alias of ConditionallyCompleteLinearOrderedField.inducedMap_inducedMap.

@[deprecated ConditionallyCompleteLinearOrderedField.inducedMap_inv_self (since := "2026-02-24")]

theorem LinearOrderedField.inducedMap_inv_self (β : Type u_3) (γ : Type u_4) [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Field γ] [ConditionallyCompleteLinearOrder γ] [IsStrictOrderedRing γ] (b : β) : ConditionallyCompleteLinearOrderedField.inducedMap γ β (ConditionallyCompleteLinearOrderedField.inducedMap β γ b) = b

Alias of ConditionallyCompleteLinearOrderedField.inducedMap_inv_self.

@[deprecated ConditionallyCompleteLinearOrderedField.inducedMap_add (since := "2026-02-24")]

theorem LinearOrderedField.inducedMap_add (α : Type u_2) (β : Type u_3) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] (x y : α) : ConditionallyCompleteLinearOrderedField.inducedMap α β (x + y) = ConditionallyCompleteLinearOrderedField.inducedMap α β x + ConditionallyCompleteLinearOrderedField.inducedMap α β y

Alias of ConditionallyCompleteLinearOrderedField.inducedMap_add.

@[deprecated ConditionallyCompleteLinearOrderedField.le_inducedMap_mul_self_of_mem_cutMap (since := "2026-02-24")]

theorem LinearOrderedField.le_inducedMap_mul_self_of_mem_cutMap {α : Type u_2} {β : Type u_3} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] {a : α} (ha : 0 < a) (b : β) (hb : b ∈ cutMap β (a * a)) : b ≤ ConditionallyCompleteLinearOrderedField.inducedMap α β a * ConditionallyCompleteLinearOrderedField.inducedMap α β a

Alias of ConditionallyCompleteLinearOrderedField.le_inducedMap_mul_self_of_mem_cutMap.

---

Preparatory lemma for inducedOrderRingHom.

@[deprecated ConditionallyCompleteLinearOrderedField.exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self (since := "2026-02-24")]

theorem LinearOrderedField.exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self {α : Type u_2} {β : Type u_3} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] {a : α} (ha : 0 < a) (b : β) (hba : b < ConditionallyCompleteLinearOrderedField.inducedMap α β a * ConditionallyCompleteLinearOrderedField.inducedMap α β a) : ∃ c ∈ cutMap β (a * a), b < c

Alias of ConditionallyCompleteLinearOrderedField.exists_mem_cutMap_mul_self_of_lt_inducedMap_mul_self.

---

Preparatory lemma for inducedOrderRingHom.

@[deprecated ConditionallyCompleteLinearOrderedField.inducedAddHom (since := "2026-02-24")]

def LinearOrderedField.inducedAddHom (α : Type u_2) (β : Type u_3) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] : α →+ β

Alias of ConditionallyCompleteLinearOrderedField.inducedAddHom.

---

inducedMap as an additive homomorphism.

@[deprecated ConditionallyCompleteLinearOrderedField.inducedOrderRingHom (since := "2026-02-24")]

def LinearOrderedField.inducedOrderRingHom (α : Type u_2) (β : Type u_3) [Field α] [LinearOrder α] [IsStrictOrderedRing α] [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] : α →+*o β

Alias of ConditionallyCompleteLinearOrderedField.inducedOrderRingHom.

---

inducedMap as an OrderRingHom.

@[deprecated ConditionallyCompleteLinearOrderedField.inducedOrderRingIso (since := "2026-02-24")]

def LinearOrderedField.inducedOrderRingIso (β : Type u_3) (γ : Type u_4) [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Field γ] [ConditionallyCompleteLinearOrder γ] [IsStrictOrderedRing γ] : β ≃+*o γ

Alias of ConditionallyCompleteLinearOrderedField.inducedOrderRingIso.

---

The isomorphism of ordered rings between two conditionally complete linearly ordered fields.

@[deprecated ConditionallyCompleteLinearOrderedField.coe_inducedOrderRingIso (since := "2026-02-24")]

theorem LinearOrderedField.coe_inducedOrderRingIso (β : Type u_3) (γ : Type u_4) [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Field γ] [ConditionallyCompleteLinearOrder γ] [IsStrictOrderedRing γ] : ⇑(ConditionallyCompleteLinearOrderedField.inducedOrderRingIso β γ) = ConditionallyCompleteLinearOrderedField.inducedMap β γ

Alias of ConditionallyCompleteLinearOrderedField.coe_inducedOrderRingIso.

@[deprecated ConditionallyCompleteLinearOrderedField.inducedOrderRingIso_symm (since := "2026-02-24")]

theorem LinearOrderedField.inducedOrderRingIso_symm (β : Type u_3) (γ : Type u_4) [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Field γ] [ConditionallyCompleteLinearOrder γ] [IsStrictOrderedRing γ] : (ConditionallyCompleteLinearOrderedField.inducedOrderRingIso β γ).symm = ConditionallyCompleteLinearOrderedField.inducedOrderRingIso γ β

Alias of ConditionallyCompleteLinearOrderedField.inducedOrderRingIso_symm.

@[deprecated ConditionallyCompleteLinearOrderedField.inducedOrderRingIso_self (since := "2026-02-24")]

theorem LinearOrderedField.inducedOrderRingIso_self (β : Type u_3) [Field β] [ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] : ConditionallyCompleteLinearOrderedField.inducedOrderRingIso β β = OrderRingIso.refl β

Alias of ConditionallyCompleteLinearOrderedField.inducedOrderRingIso_self.