Linear ordered (semi)fields

A linear ordered (semi)field is a (semi)field equipped with a linear order such that

• addition respects the order: a ≤ b → c + a ≤ c + b;
• multiplication of positives is positive: 0 < a → 0 < b → 0 < a * b;
• 0 < 1.

Main Definitions

• LinearOrderedSemifield: Typeclass for linear order semifields.
• LinearOrderedField: Typeclass for linear ordered fields.

@[deprecated "Use `[Semifield K] [LinearOrder K] [IsStrictOrderedRing K]` instead." (since := "2025-04-10")]

structure LinearOrderedSemifield (K : Type u_2) extends LinearOrderedCommSemiring K, Semifield K : Type u_2

A linear ordered semifield is a field with a linear order respecting the operations.

• add : K → K → K
• add_assoc (a b c : K) : a + b + c = a + (b + c)
• zero : K
• zero_add (a : K) : 0 + a = a
• add_zero (a : K) : a + 0 = a
• nsmul : ℕ → K → K
• nsmul_zero (x : K) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : K) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : K) : a + b = b + a
• mul : K → K → K
• left_distrib (a b c : K) : a * (b + c) = a * b + a * c
• right_distrib (a b c : K) : (a + b) * c = a * c + b * c
• zero_mul (a : K) : 0 * a = 0
• mul_zero (a : K) : a * 0 = 0
• mul_assoc (a b c : K) : a * b * c = a * (b * c)
• one : K
• one_mul (a : K) : 1 * a = a
• mul_one (a : K) : a * 1 = a
• natCast : ℕ → K
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → K → K
• npow_zero (x : K) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : K) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• le : K → K → Prop
• lt : K → K → Prop
• le_refl (a : K) : a ≤ a
• le_trans (a b c : K) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le (a b : K) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : K) : a ≤ b → b ≤ a → a = b
• add_le_add_left (a b : K) : a ≤ b → ∀ (c : K), c + a ≤ c + b
• le_of_add_le_add_left (a b c : K) : a + b ≤ a + c → b ≤ c
• exists_pair_ne : ∃ (x : K), ∃ (y : K), x ≠ y
• zero_le_one : 0 ≤ 1
• mul_lt_mul_of_pos_left (a b c : K) : a < b → 0 < c → c * a < c * b
• mul_lt_mul_of_pos_right (a b c : K) : a < b → 0 < c → a * c < b * c
• mul_comm (a b : K) : a * b = b * a
• min : K → K → K
• max : K → K → K
• compare : K → K → Ordering
• le_total (a b : K) : a ≤ b ∨ b ≤ a
• toDecidableLE : DecidableLE K
• toDecidableEq : DecidableEq K
• toDecidableLT : DecidableLT K
• min_def (a b : K) : a ⊓ b = if a ≤ b then a else b
• max_def (a b : K) : a ⊔ b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq (a b : K) : compare a b = compareOfLessAndEq a b
• inv : K → K
• div : K → K → K
• div_eq_mul_inv (a b : K) : a / b = a * b⁻¹
• zpow : ℤ → K → K
• zpow_zero' (a : K) : self.zpow 0 a = 1
• zpow_succ' (n : ℕ) (a : K) : self.zpow (↑n.succ) a = self.zpow (↑n) a * a
• zpow_neg' (n : ℕ) (a : K) : self.zpow (Int.negSucc n) a = (self.zpow (↑n.succ) a)⁻¹
• inv_zero : 0⁻¹ = 0
• mul_inv_cancel (a : K) : a ≠ 0 → a * a⁻¹ = 1
• nnratCast : ℚ≥0 → K
• nnratCast_def (q : ℚ≥0) : ↑q = ↑q.num / ↑q.den
• nnqsmul : ℚ≥0 → K → K
• nnqsmul_def (q : ℚ≥0) (a : K) : self.nnqsmul q a = ↑q * a

@[deprecated "Use `[Field K] [LinearOrder K] [IsStrictOrderedRing K]` instead." (since := "2025-04-10")]

structure LinearOrderedField (K : Type u_2) extends LinearOrderedCommRing K, Field K : Type u_2

A linear ordered field is a field with a linear order respecting the operations.

• add : K → K → K
• add_assoc (a b c : K) : a + b + c = a + (b + c)
• zero : K
• zero_add (a : K) : 0 + a = a
• add_zero (a : K) : a + 0 = a
• nsmul : ℕ → K → K
• nsmul_zero (x : K) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : K) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : K) : a + b = b + a
• mul : K → K → K
• left_distrib (a b c : K) : a * (b + c) = a * b + a * c
• right_distrib (a b c : K) : (a + b) * c = a * c + b * c
• zero_mul (a : K) : 0 * a = 0
• mul_zero (a : K) : a * 0 = 0
• mul_assoc (a b c : K) : a * b * c = a * (b * c)
• one : K
• one_mul (a : K) : 1 * a = a
• mul_one (a : K) : a * 1 = a
• natCast : ℕ → K
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• npow : ℕ → K → K
• npow_zero (x : K) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : K) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : K → K
• sub : K → K → K
• sub_eq_add_neg (a b : K) : a - b = a + -b
• zsmul : ℤ → K → K
• zsmul_zero' (a : K) : Ring.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : K) : Ring.zsmul (↑n.succ) a = Ring.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : K) : Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• neg_add_cancel (a : K) : -a + a = 0
• intCast : ℤ → K
• intCast_ofNat (n : ℕ) : IntCast.intCast ↑n = ↑n
• intCast_negSucc (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• le : K → K → Prop
• lt : K → K → Prop
• le_refl (a : K) : a ≤ a
• le_trans (a b c : K) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le (a b : K) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : K) : a ≤ b → b ≤ a → a = b
• add_le_add_left (a b : K) : a ≤ b → ∀ (c : K), c + a ≤ c + b
• exists_pair_ne : ∃ (x : K), ∃ (y : K), x ≠ y
• zero_le_one : 0 ≤ 1
• mul_pos (a b : K) : 0 < a → 0 < b → 0 < a * b
• min : K → K → K
• max : K → K → K
• compare : K → K → Ordering
• le_total (a b : K) : a ≤ b ∨ b ≤ a
• toDecidableLE : DecidableLE K
• toDecidableEq : DecidableEq K
• toDecidableLT : DecidableLT K
• min_def (a b : K) : a ⊓ b = if a ≤ b then a else b
• max_def (a b : K) : a ⊔ b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq (a b : K) : compare a b = compareOfLessAndEq a b
• mul_comm (a b : K) : a * b = b * a
• inv : K → K
• div : K → K → K
• div_eq_mul_inv (a b : K) : a / b = a * b⁻¹
• zpow : ℤ → K → K
• zpow_zero' (a : K) : self.zpow 0 a = 1
• zpow_succ' (n : ℕ) (a : K) : self.zpow (↑n.succ) a = self.zpow (↑n) a * a
• zpow_neg' (n : ℕ) (a : K) : self.zpow (Int.negSucc n) a = (self.zpow (↑n.succ) a)⁻¹
• nnratCast : ℚ≥0 → K
• ratCast : ℚ → K
• mul_inv_cancel (a : K) : a ≠ 0 → a * a⁻¹ = 1
• inv_zero : 0⁻¹ = 0
• nnratCast_def (q : ℚ≥0) : ↑q = ↑q.num / ↑q.den
• nnqsmul : ℚ≥0 → K → K
• nnqsmul_def (q : ℚ≥0) (a : K) : self.nnqsmul q a = ↑q * a
• ratCast_def (q : ℚ) : ↑q = ↑q.num / ↑q.den
• qsmul : ℚ → K → K
• qsmul_def (a : ℚ) (x : K) : self.qsmul a x = ↑a * x

theorem mul_inv_le_one {K : Type u_1} [Semifield K] [LinearOrder K] {a : K} [ZeroLEOneClass K] : a * a⁻¹ ≤ 1

Equality holds when a ≠ 0. See mul_inv_cancel.

theorem inv_mul_le_one {K : Type u_1} [Semifield K] [LinearOrder K] {a : K} [ZeroLEOneClass K] : a⁻¹ * a ≤ 1

Equality holds when a ≠ 0. See inv_mul_cancel.

theorem mul_inv_left_le {K : Type u_1} [Semifield K] [LinearOrder K] {a b : K} (hb : 0 ≤ b) : a * (a⁻¹ * b) ≤ b

Equality holds when a ≠ 0. See mul_inv_cancel_left.

theorem le_mul_inv_left {K : Type u_1} [Semifield K] [LinearOrder K] {a b : K} (hb : b ≤ 0) : b ≤ a * (a⁻¹ * b)

Equality holds when a ≠ 0. See mul_inv_cancel_left.

theorem inv_mul_left_le {K : Type u_1} [Semifield K] [LinearOrder K] {a b : K} (hb : 0 ≤ b) : a⁻¹ * (a * b) ≤ b

Equality holds when a ≠ 0. See inv_mul_cancel_left.

theorem le_inv_mul_left {K : Type u_1} [Semifield K] [LinearOrder K] {a b : K} (hb : b ≤ 0) : b ≤ a⁻¹ * (a * b)

Equality holds when a ≠ 0. See inv_mul_cancel_left.

theorem mul_inv_right_le {K : Type u_1} [Semifield K] [LinearOrder K] {a b : K} (ha : 0 ≤ a) : a * b * b⁻¹ ≤ a

Equality holds when b ≠ 0. See mul_inv_cancel_right.

theorem le_mul_inv_right {K : Type u_1} [Semifield K] [LinearOrder K] {a b : K} (ha : a ≤ 0) : a ≤ a * b * b⁻¹

Equality holds when b ≠ 0. See mul_inv_cancel_right.

theorem inv_mul_right_le {K : Type u_1} [Semifield K] [LinearOrder K] {a b : K} (ha : 0 ≤ a) : a * b⁻¹ * b ≤ a

Equality holds when b ≠ 0. See inv_mul_cancel_right.

theorem le_inv_mul_right {K : Type u_1} [Semifield K] [LinearOrder K] {a b : K} (ha : a ≤ 0) : a ≤ a * b⁻¹ * b

Equality holds when b ≠ 0. See inv_mul_cancel_right.

theorem mul_div_mul_left_le {K : Type u_1} [Semifield K] [LinearOrder K] {a b c : K} (h : 0 ≤ a / b) : c * a / (c * b) ≤ a / b

Equality holds when c ≠ 0. See mul_div_mul_left.

theorem le_mul_div_mul_left {K : Type u_1} [Semifield K] [LinearOrder K] {a b c : K} (h : a / b ≤ 0) : a / b ≤ c * a / (c * b)

Equality holds when c ≠ 0. See mul_div_mul_left.

theorem mul_div_mul_right_le {K : Type u_1} [Semifield K] [LinearOrder K] {a b c : K} (h : 0 ≤ a / b) : a * c / (b * c) ≤ a / b

Equality holds when c ≠ 0. See mul_div_mul_right.

theorem le_mul_div_mul_right {K : Type u_1} [Semifield K] [LinearOrder K] {a b c : K} (h : a / b ≤ 0) : a / b ≤ a * c / (b * c)

Equality holds when c ≠ 0. See mul_div_mul_right.