# Documentation

Mathlib.Algebra.Order.Field.Defs

# 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.

class LinearOrderedSemifield (α : Type u_1) extends , , :
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 () a = a * zpow () a) _auto✝
• a ^ -(n + 1) = (a ^ (n + 1))⁻¹

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

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

Instances
class LinearOrderedField (α : Type u_1) extends , , , :
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 () a = a * zpow () a) _auto✝
• a ^ -(n + 1) = (a ^ (n + 1))⁻¹

zpow_neg' : autoParam (∀ (n : ) (a : α), zpow () a = (zpow (↑()) a)⁻¹) _auto✝
• toRatCast :
• For a nonzero a, a⁻¹ is a right multiplicative inverse.

mul_inv_cancel : ∀ (a : α), a 0a * 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 : ), ↑(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.

Instances
instance LinearOrderedField.toLinearOrderedSemifield {α : Type u_1} [inst : ] :
Equations
• One or more equations did not get rendered due to their size.