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.

class LinearOrderedSemifield (α : Type u_2) extends LinearOrderedCommSemiring , Inv , Div : Type u_2

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

• 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 = x + AddMonoid.nsmul n 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 : NatCast.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = x * Semiring.npow n 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_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b
• le_of_add_le_add_left : ∀ (a b c : α), a + b ≤ a + c → b ≤ c
• exists_pair_ne : ∃ (x : α), ∃ (y : α), x ≠ y
• zero_le_one : 0 ≤ 1
• mul_lt_mul_of_pos_left : ∀ (a b c : α), a < b → 0 < c → c * a < c * b
• mul_lt_mul_of_pos_right : ∀ (a b c : α), a < b → 0 < c → a * c < b * c
• mul_comm : ∀ (a b : α), a * b = b * a
• min : α → α → α
• max : α → α → α
• compare : α → α → Ordering
• le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
• decidableLE : DecidableRel fun (x x_1 : α) => x ≤ x_1
• decidableEq : DecidableEq α
• decidableLT : DecidableRel fun (x x_1 : α) => x < x_1
• min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
• max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b = compareOfLessAndEq a b
• inv : α → α
• div : α → α → α
• div_eq_mul_inv : ∀ (a b : α), a / b = a * b⁻¹

  a / b := a * b⁻¹

• zpow : ℤ → α → α

  The power operation: a ^ n = a * ··· * a; a ^ (-n) = a⁻¹ * ··· a⁻¹ (n times)

• zpow_zero' : ∀ (a : α), LinearOrderedSemifield.zpow 0 a = 1

  a ^ 0 = 1

• zpow_succ' : ∀ (n : ℕ) (a : α), LinearOrderedSemifield.zpow (Int.ofNat (Nat.succ n)) a = a * LinearOrderedSemifield.zpow (Int.ofNat n) a

  a ^ (n + 1) = a * a ^ n

• zpow_neg' : ∀ (n : ℕ) (a : α), LinearOrderedSemifield.zpow (Int.negSucc n) a = (LinearOrderedSemifield.zpow (↑(Nat.succ n)) a)⁻¹

  a ^ -(n + 1) = (a ^ (n + 1))⁻¹

• inv_zero : 0⁻¹ = 0

  The inverse of 0 in a group with zero is 0.

• mul_inv_cancel : ∀ (a : α), a ≠ 0 → a * a⁻¹ = 1

  Every nonzero element of a group with zero is invertible.

class LinearOrderedField (α : Type u_2) extends LinearOrderedCommRing , Inv , Div , RatCast : Type u_2

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

• 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 = x + AddMonoid.nsmul n 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 : NatCast.natCast 0 = 0
• natCast_succ : ∀ (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero : ∀ (x : α), Semiring.npow 0 x = 1
• npow_succ : ∀ (n : ℕ) (x : α), Semiring.npow (n + 1) x = x * Semiring.npow n 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 (Int.ofNat (Nat.succ n)) a = a + Ring.zsmul (Int.ofNat n) a
• zsmul_neg' : ∀ (n : ℕ) (a : α), Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑(Nat.succ n)) a
• add_left_neg : ∀ (a : α), -a + a = 0
• intCast : ℤ → α
• intCast_ofNat : ∀ (n : ℕ), IntCast.intCast ↑n = ↑n
• intCast_negSucc : ∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b
• exists_pair_ne : ∃ (x : α), ∃ (y : α), x ≠ y
• zero_le_one : 0 ≤ 1
• mul_pos : ∀ (a b : α), 0 < a → 0 < b → 0 < a * b
• min : α → α → α
• max : α → α → α
• compare : α → α → Ordering
• le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
• decidableLE : DecidableRel fun (x x_1 : α) => x ≤ x_1
• decidableEq : DecidableEq α
• decidableLT : DecidableRel fun (x x_1 : α) => x < x_1
• min_def : ∀ (a b : α), min a b = if a ≤ b then a else b
• max_def : ∀ (a b : α), max a b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b = compareOfLessAndEq a b
• mul_comm : ∀ (a b : α), a * b = b * a
• inv : α → α
• div : α → α → α
• div_eq_mul_inv : ∀ (a b : α), a / b = a * b⁻¹

  a / b := a * b⁻¹

• zpow : ℤ → α → α

  The power operation: a ^ n = a * ··· * a; a ^ (-n) = a⁻¹ * ··· a⁻¹ (n times)

• zpow_zero' : ∀ (a : α), LinearOrderedField.zpow 0 a = 1

  a ^ 0 = 1

• zpow_succ' : ∀ (n : ℕ) (a : α), LinearOrderedField.zpow (Int.ofNat (Nat.succ n)) a = a * LinearOrderedField.zpow (Int.ofNat n) a

  a ^ (n + 1) = a * a ^ n

• zpow_neg' : ∀ (n : ℕ) (a : α), LinearOrderedField.zpow (Int.negSucc n) a = (LinearOrderedField.zpow (↑(Nat.succ n)) a)⁻¹

  a ^ -(n + 1) = (a ^ (n + 1))⁻¹

• ratCast : ℚ → α
• mul_inv_cancel : ∀ (a : α), a ≠ 0 → a * a⁻¹ = 1

  For a nonzero a, a⁻¹ is a right multiplicative inverse.

• inv_zero : 0⁻¹ = 0

  The inverse of 0 is 0 by convention.

• ratCast_mk : ∀ (a : ℤ) (b : ℕ) (h1 : b ≠ 0) (h2 : Nat.Coprime (Int.natAbs a) b), ↑{ num := a, den := b, den_nz := h1, reduced := h2 } = ↑a * (↑b)⁻¹

  However Rat.cast is defined, it must be propositionally equal to a * b⁻¹.

  Do not use this lemma directly. Use Rat.cast_def instead.

• qsmul : ℚ → α → α

  Scalar multiplication by a rational number.

  Set this to qsmulRec _ unless there is a risk of a Module ℚ _ instance diamond.

  Do not use directly. Instead use the • notation.

• qsmul_eq_mul' : ∀ (a : ℚ) (x : α), LinearOrderedField.qsmul a x = ↑a * x

  However qsmul is defined, it must be propositionally equal to multiplication by Rat.cast.

  Do not use this lemma directly. Use Rat.cast_def instead.

instance LinearOrderedField.toLinearOrderedSemifield {α : Type u_1} [LinearOrderedField α] : LinearOrderedSemifield α

Equations

• LinearOrderedField.toLinearOrderedSemifield = let __src := LinearOrderedRing.toLinearOrderedSemiring; let __src_1 := inst; LinearOrderedSemifield.mk ⋯ LinearOrderedField.zpow ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem inv_pos {α : Type u_1} [LinearOrderedSemifield α] {a : α} : 0 < a⁻¹ ↔ 0 < a

theorem inv_pos_of_pos {α : Type u_1} [LinearOrderedSemifield α] {a : α} : 0 < a → 0 < a⁻¹

Alias of the reverse direction of inv_pos.

@[simp]

theorem inv_nonneg {α : Type u_1} [LinearOrderedSemifield α] {a : α} : 0 ≤ a⁻¹ ↔ 0 ≤ a

theorem inv_nonneg_of_nonneg {α : Type u_1} [LinearOrderedSemifield α] {a : α} : 0 ≤ a → 0 ≤ a⁻¹

Alias of the reverse direction of inv_nonneg.

@[simp]

theorem inv_lt_zero {α : Type u_1} [LinearOrderedSemifield α] {a : α} : a⁻¹ < 0 ↔ a < 0

@[simp]

theorem inv_nonpos {α : Type u_1} [LinearOrderedSemifield α] {a : α} : a⁻¹ ≤ 0 ↔ a ≤ 0

theorem one_div_pos {α : Type u_1} [LinearOrderedSemifield α] {a : α} : 0 < 1 / a ↔ 0 < a

theorem one_div_neg {α : Type u_1} [LinearOrderedSemifield α] {a : α} : 1 / a < 0 ↔ a < 0

theorem one_div_nonneg {α : Type u_1} [LinearOrderedSemifield α] {a : α} : 0 ≤ 1 / a ↔ 0 ≤ a

theorem one_div_nonpos {α : Type u_1} [LinearOrderedSemifield α] {a : α} : 1 / a ≤ 0 ↔ a ≤ 0

theorem div_pos {α : Type u_1} [LinearOrderedSemifield α] {a : α} {b : α} (ha : 0 < a) (hb : 0 < b) : 0 < a / b

theorem div_nonneg {α : Type u_1} [LinearOrderedSemifield α] {a : α} {b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a / b

theorem div_nonpos_of_nonpos_of_nonneg {α : Type u_1} [LinearOrderedSemifield α] {a : α} {b : α} (ha : a ≤ 0) (hb : 0 ≤ b) : a / b ≤ 0

theorem div_nonpos_of_nonneg_of_nonpos {α : Type u_1} [LinearOrderedSemifield α] {a : α} {b : α} (ha : 0 ≤ a) (hb : b ≤ 0) : a / b ≤ 0

theorem zpow_nonneg {α : Type u_1} [LinearOrderedSemifield α] {a : α} (ha : 0 ≤ a) (n : ℤ) : 0 ≤ a ^ n

theorem zpow_pos_of_pos {α : Type u_1} [LinearOrderedSemifield α] {a : α} (ha : 0 < a) (n : ℤ) : 0 < a ^ n