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.

Implementation details

For olean caching reasons, this file is separate to the main file, Mathlib.Algebra.Order.Field.Basic. The lemmata are instead located there.

ink

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

• a / b := a * b⁻¹

  div_eq_mul_inv : autoParam (∀ (a b : α), a / b = a * b⁻¹) _auto✝

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

  zpow : ℤ → α → α

• a ^ 0 = 1

  zpow_zero' : autoParam (∀ (a : α), zpow 0 a = 1) _auto✝

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

  zpow_succ' : autoParam (∀ (n : ℕ) (a : α), zpow (Int.ofNat (Nat.succ n)) a = a * zpow (Int.ofNat n) a) _auto✝

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

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

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

  inv_zero : 0⁻¹ = 0

• Every nonzero element of a group with zero is invertible.

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

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

ink

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

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

  zpow : ℤ → α → α

• a ^ 0 = 1

  zpow_zero' : autoParam (∀ (a : α), zpow 0 a = 1) _auto✝

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

  zpow_succ' : autoParam (∀ (n : ℕ) (a : α), zpow (Int.ofNat (Nat.succ n)) a = a * zpow (Int.ofNat n) a) _auto✝

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

  zpow_neg' : autoParam (∀ (n : ℕ) (a : α), zpow (Int.negSucc n) a = (zpow (↑(Nat.succ n)) a)⁻¹) _auto✝
• toRatCast : RatCast α

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

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

• We define the inverse of 0 to be 0.

  inv_zero : 0⁻¹ = 0

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

  ratCast_mk : autoParam (∀ (a : ℤ) (b : ℕ) (h1 : b ≠ 0) (h2 : Nat.coprime (Int.natAbs a) b), ↑(Rat.mk' a b) = ↑a * (↑b)⁻¹) _auto✝

• Multiplication by a rational number.

  qsmul : ℚ → α → α

• However qsmul is defined, propositionally it must be equal to multiplication by ratCast.

  qsmul_eq_mul' : autoParam (∀ (a : ℚ) (x : α), qsmul a x = ↑a * x) _auto✝

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

ink

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

Equations

• One or more equations did not get rendered due to their size.