# mathlib3documentation

algebra.order.field.defs

# Linear ordered (semi)fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• linear_ordered_semifield: Typeclass for linear order semifields.
• linear_ordered_field: Typeclass for linear ordered fields.

## Implementation details #

For olean caching reasons, this file is separate to the main file, algebra.order.field.basic. The lemmata are instead located there.

@[class]
structure linear_ordered_semifield (α : Type u_2) :
Type u_2
• 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 : α), . "try_refl_tac"
• nsmul_succ' : ( (n : ) (x : α), . "try_refl_tac"
• 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
• nat_cast : α
• nat_cast_zero : . "control_laws_tac"
• nat_cast_succ : ( (n : ), . "control_laws_tac"
• npow : α α
• npow_zero' : ( (x : α), . "try_refl_tac"
• npow_succ' : ( (n : ) (x : α), . "try_refl_tac"
• 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) . "order_laws_tac"
• 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
• le_total : (a b : α), a b b a
• decidable_le :
• decidable_eq :
• decidable_lt :
• max : α α α
• max_def : . "reflexivity"
• min : α α α
• min_def : . "reflexivity"
• inv : α α
• div : α α α
• div_eq_mul_inv : ( (a b : α), a / b = a * b⁻¹) . "try_refl_tac"
• zpow : α α
• zpow_zero' : ( (a : α), . "try_refl_tac"
• zpow_succ' : ( (n : ) (a : α), . "try_refl_tac"
• zpow_neg' : ( (n : ) (a : α), . "try_refl_tac"
• inv_zero : 0⁻¹ = 0
• mul_inv_cancel : (a : α), a 0 a * a⁻¹ = 1

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

Instances of this typeclass
Instances of other typeclasses for linear_ordered_semifield
• linear_ordered_semifield.has_sizeof_inst
@[instance]
@[instance]
@[class]
structure linear_ordered_field (α : Type u_2) :
Type u_2

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

Instances of this typeclass
Instances of other typeclasses for linear_ordered_field
• linear_ordered_field.has_sizeof_inst
@[protected, instance]
Equations