Linear ordered fields #
A linear ordered field is a 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_field
: the class of linear ordered fields.
- add : α → α → α
- add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
- zero : α
- zero_add : ∀ (a : α), 0 + a = a
- add_zero : ∀ (a : α), a + 0 = a
- nsmul : ℕ → α → α
- nsmul_zero' : (∀ (x : α), linear_ordered_field.nsmul 0 x = 0) . "try_refl_tac"
- nsmul_succ' : (∀ (n : ℕ) (x : α), linear_ordered_field.nsmul n.succ x = x + linear_ordered_field.nsmul n x) . "try_refl_tac"
- neg : α → α
- sub : α → α → α
- sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
- gsmul : ℤ → α → α
- gsmul_zero' : (∀ (a : α), linear_ordered_field.gsmul 0 a = 0) . "try_refl_tac"
- gsmul_succ' : (∀ (n : ℕ) (a : α), linear_ordered_field.gsmul (int.of_nat n.succ) a = a + linear_ordered_field.gsmul (int.of_nat n) a) . "try_refl_tac"
- gsmul_neg' : (∀ (n : ℕ) (a : α), linear_ordered_field.gsmul -[1+ n] a = -linear_ordered_field.gsmul ↑(n.succ) a) . "try_refl_tac"
- add_left_neg : ∀ (a : α), -a + a = 0
- add_comm : ∀ (a b : α), a + b = b + a
- mul : α → α → α
- mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
- one : α
- one_mul : ∀ (a : α), 1 * a = a
- mul_one : ∀ (a : α), a * 1 = a
- npow : ℕ → α → α
- npow_zero' : (∀ (x : α), linear_ordered_field.npow 0 x = 1) . "try_refl_tac"
- npow_succ' : (∀ (n : ℕ) (x : α), linear_ordered_field.npow n.succ x = x * linear_ordered_field.npow n x) . "try_refl_tac"
- left_distrib : ∀ (a b c_1 : α), a * (b + c_1) = a * b + a * c_1
- right_distrib : ∀ (a b c_1 : α), (a + b) * c_1 = a * c_1 + b * c_1
- le : α → α → Prop
- lt : α → α → Prop
- le_refl : ∀ (a : α), a ≤ a
- le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
- 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_1 : α), c_1 + a ≤ c_1 + b
- zero_le_one : 0 ≤ 1
- mul_pos : ∀ (a b : α), 0 < a → 0 < b → 0 < a * b
- le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
- decidable_le : decidable_rel has_le.le
- decidable_eq : decidable_eq α
- decidable_lt : decidable_rel has_lt.lt
- exists_pair_ne : ∃ (x y : α), x ≠ y
- mul_comm : ∀ (a b : α), a * b = b * a
- inv : α → α
- div : α → α → α
- div_eq_mul_inv : (∀ (a b : α), a / b = a * b⁻¹) . "try_refl_tac"
- gpow : ℤ → α → α
- gpow_zero' : (∀ (a : α), linear_ordered_field.gpow 0 a = 1) . "try_refl_tac"
- gpow_succ' : (∀ (n : ℕ) (a : α), linear_ordered_field.gpow (int.of_nat n.succ) a = a * linear_ordered_field.gpow (int.of_nat n) a) . "try_refl_tac"
- gpow_neg' : (∀ (n : ℕ) (a : α), linear_ordered_field.gpow -[1+ n] a = (linear_ordered_field.gpow ↑(n.succ) a)⁻¹) . "try_refl_tac"
- mul_inv_cancel : ∀ {a : α}, a ≠ 0 → a * a⁻¹ = 1
- inv_zero : 0⁻¹ = 0
A linear ordered field is a field with a linear order respecting the operations.
Lemmas about pos, nonneg, nonpos, neg #
Relating one division with another term. #
One direction of div_le_iff
where b
is allowed to be 0
(but c
must be nonnegative)
Bi-implications of inequalities using inversions #
See inv_le_inv_of_le
for the implication from right-to-left with one fewer assumption.
Relating two divisions. #
Relating one division and involving 1
#
Relating two divisions, involving 1
#
For the single implications with fewer assumptions, see one_div_le_one_div_of_le
and
le_of_one_div_le_one_div
For the single implications with fewer assumptions, see one_div_lt_one_div_of_lt
and
lt_of_one_div_lt_one_div
For the single implications with fewer assumptions, see one_div_lt_one_div_of_neg_of_lt
and
lt_of_one_div_lt_one_div
For the single implications with fewer assumptions, see one_div_lt_one_div_of_lt
and
lt_of_one_div_lt_one_div
Results about halving. #
The equalities also hold in fields of characteristic 0
.
Miscellaneous lemmas #
Pullback a linear_ordered_field
under an injective map.
Equations
- function.injective.linear_ordered_field f hf zero one add mul neg sub inv div = {add := linear_ordered_ring.add (function.injective.linear_ordered_ring f hf zero one add mul neg sub), add_assoc := _, zero := linear_ordered_ring.zero (function.injective.linear_ordered_ring f hf zero one add mul neg sub), zero_add := _, add_zero := _, nsmul := linear_ordered_ring.nsmul (function.injective.linear_ordered_ring f hf zero one add mul neg sub), nsmul_zero' := _, nsmul_succ' := _, neg := linear_ordered_ring.neg (function.injective.linear_ordered_ring f hf zero one add mul neg sub), sub := linear_ordered_ring.sub (function.injective.linear_ordered_ring f hf zero one add mul neg sub), sub_eq_add_neg := _, gsmul := linear_ordered_ring.gsmul (function.injective.linear_ordered_ring f hf zero one add mul neg sub), gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := linear_ordered_ring.mul (function.injective.linear_ordered_ring f hf zero one add mul neg sub), mul_assoc := _, one := linear_ordered_ring.one (function.injective.linear_ordered_ring f hf zero one add mul neg sub), one_mul := _, mul_one := _, npow := linear_ordered_ring.npow (function.injective.linear_ordered_ring f hf zero one add mul neg sub), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := linear_ordered_ring.le (function.injective.linear_ordered_ring f hf zero one add mul neg sub), lt := linear_ordered_ring.lt (function.injective.linear_ordered_ring f hf zero one add mul neg sub), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_pos := _, le_total := _, decidable_le := linear_ordered_ring.decidable_le (function.injective.linear_ordered_ring f hf zero one add mul neg sub), decidable_eq := linear_ordered_ring.decidable_eq (function.injective.linear_ordered_ring f hf zero one add mul neg sub), decidable_lt := linear_ordered_ring.decidable_lt (function.injective.linear_ordered_ring f hf zero one add mul neg sub), exists_pair_ne := _, mul_comm := _, inv := field.inv (function.injective.field f hf zero one add mul neg sub inv div), div := field.div (function.injective.field f hf zero one add mul neg sub inv div), div_eq_mul_inv := _, gpow := field.gpow (function.injective.field f hf zero one add mul neg sub inv div), gpow_zero' := _, gpow_succ' := _, gpow_neg' := _, mul_inv_cancel := _, inv_zero := _}
Alias of mul_sub_mul_div_mul_neg_iff
.
Alias of mul_sub_mul_div_mul_neg_iff
.
Alias of mul_sub_mul_div_mul_nonpos_iff
.
Alias of mul_sub_mul_div_mul_nonpos_iff
.