# 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 , , , :
Type u_2

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

• 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 : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) 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 :
• natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) =
• npow : αα
• npow_zero : ∀ (x : α), = 1
• npow_succ : ∀ (n : ) (x : α), Semiring.npow (n + 1) x = * x
• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = 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 + cb c
• exists_pair_ne : ∃ (x : α), ∃ (y : α), x y
• zero_le_one : 0 1
• mul_lt_mul_of_pos_left : ∀ (a b c : α), a < b0 < cc * a < c * b
• mul_lt_mul_of_pos_right : ∀ (a b c : α), a < b0 < ca * 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 :
• 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 =
• 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 : α),

a ^ 0 = 1

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

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

• zpow_neg' : ∀ (n : ) (a : α), = (LinearOrderedSemifield.zpow (n.succ) 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 0a * a⁻¹ = 1

Every nonzero element of a group with zero is invertible.

• nnratCast : ℚ≥0α
• nnratCast_def : ∀ (q : ℚ≥0), q = q.num / q.den

However NNRat.cast is defined, it must be propositionally equal to a / b.

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

• nnqsmul : ℚ≥0αα

Scalar multiplication by a nonnegative rational number.

Unless there is a risk of a Module ℚ≥0 _ instance diamond, write nnqsmul := _. This will set nnqsmul to (NNRat.cast · * ·) thanks to unification in the default proof of nnqsmul_def.

Do not use directly. Instead use the • notation.

• nnqsmul_def : ∀ (q : ℚ≥0) (a : α), = q * a

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

Do not use this lemma directly. Use NNRat.smul_def instead.

Instances
class LinearOrderedField (α : Type u_2) extends , , , , :
Type u_2

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

• 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 : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) 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 :
• natCast_succ : ∀ (n : ), NatCast.natCast (n + 1) =
• npow : αα
• npow_zero : ∀ (x : α), = 1
• npow_succ : ∀ (n : ) (x : α), Semiring.npow (n + 1) x = * x
• neg : αα
• sub : ααα
• sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
• zsmul : αα
• zsmul_zero' : ∀ (a : α), = 0
• zsmul_succ' : ∀ (n : ) (a : α), Ring.zsmul (Int.ofNat n.succ) a = Ring.zsmul () a + a
• zsmul_neg' : ∀ (n : ) (a : α), = -Ring.zsmul (n.succ) a
• add_left_neg : ∀ (a : α), -a + a = 0
• intCast : α
• intCast_ofNat : ∀ (n : ), = n
• intCast_negSucc : ∀ (n : ), = -(n + 1)
• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = 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 < a0 < b0 < a * b
• min : ααα
• max : ααα
• compare : ααOrdering
• le_total : ∀ (a b : α), a b b a
• decidableLE : DecidableRel fun (x x_1 : α) => x x_1
• 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 =
• 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 : α),

a ^ 0 = 1

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

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

• zpow_neg' : ∀ (n : ) (a : α), = (LinearOrderedField.zpow (n.succ) a)⁻¹

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

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

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

• inv_zero : 0⁻¹ = 0

The inverse of 0 is 0 by convention.

• nnratCast_def : ∀ (q : ℚ≥0), q = q.num / q.den

However NNRat.cast is defined, it must be equal to a / b.

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

• nnqsmul : ℚ≥0αα

Scalar multiplication by a nonnegative rational number.

Unless there is a risk of a Module ℚ≥0 _ instance diamond, write nnqsmul := _. This will set nnqsmul to (NNRat.cast · * ·) thanks to unification in the default proof of nnqsmul_def.

Do not use directly. Instead use the • notation.

• nnqsmul_def : ∀ (q : ℚ≥0) (a : α), = q * a

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

Do not use this lemma directly. Use NNRat.smul_def instead.

• ratCast_def : ∀ (q : ), q = q.num / q.den

However Rat.cast q is defined, it must be propositionally equal to q.num / q.den.

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

• qsmul : αα

Scalar multiplication by a rational number.

Unless there is a risk of a Module ℚ _ instance diamond, write qsmul := _. This will set qsmul to (Rat.cast · * ·) thanks to unification in the default proof of qsmul_def.

Do not use directly. Instead use the • notation.

• qsmul_def : ∀ (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.

Instances
@[instance 100]
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem inv_pos {α : Type u_1} {a : α} :
0 < a⁻¹ 0 < a
theorem inv_pos_of_pos {α : Type u_1} {a : α} :
0 < a0 < a⁻¹

Alias of the reverse direction of inv_pos.

@[simp]
theorem inv_nonneg {α : Type u_1} {a : α} :
0 a⁻¹ 0 a
theorem inv_nonneg_of_nonneg {α : Type u_1} {a : α} :
0 a0 a⁻¹

Alias of the reverse direction of inv_nonneg.

@[simp]
theorem inv_lt_zero {α : Type u_1} {a : α} :
a⁻¹ < 0 a < 0
@[simp]
theorem inv_nonpos {α : Type u_1} {a : α} :
a⁻¹ 0 a 0
theorem one_div_pos {α : Type u_1} {a : α} :
0 < 1 / a 0 < a
theorem one_div_neg {α : Type u_1} {a : α} :
1 / a < 0 a < 0
theorem one_div_nonneg {α : Type u_1} {a : α} :
0 1 / a 0 a
theorem one_div_nonpos {α : Type u_1} {a : α} :
1 / a 0 a 0
theorem div_pos {α : Type u_1} {a : α} {b : α} (ha : 0 < a) (hb : 0 < b) :
0 < a / b
theorem div_nonneg {α : Type u_1} {a : α} {b : α} (ha : 0 a) (hb : 0 b) :
0 a / b
theorem div_nonpos_of_nonpos_of_nonneg {α : Type u_1} {a : α} {b : α} (ha : a 0) (hb : 0 b) :
a / b 0
theorem div_nonpos_of_nonneg_of_nonpos {α : Type u_1} {a : α} {b : α} (ha : 0 a) (hb : b 0) :
a / b 0
theorem zpow_nonneg {α : Type u_1} {a : α} (ha : 0 a) (n : ) :
0 a ^ n
theorem zpow_pos_of_pos {α : Type u_1} {a : α} (ha : 0 < a) (n : ) :
0 < a ^ n