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.discrete_linear_ordered_field: the class of linear ordered fields where the inequality is decidable.
- 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
- neg : α → α
- 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
- 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
- exists_pair_ne : ∃ (x y : α), x ≠ y
- mul_pos : ∀ (a b : α), 0 < a → 0 < b → 0 < a * b
- le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
- zero_lt_one : linear_ordered_field.zero < linear_ordered_field.one
- mul_comm : ∀ (a b : α), a * b = b * a
- inv : α → α
- 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
Equations
- 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
- neg : α → α
- 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
- 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
- exists_pair_ne : ∃ (x y : α), x ≠ y
- mul_pos : ∀ (a b : α), 0 < a → 0 < b → 0 < a * b
- le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
- zero_lt_one : discrete_linear_ordered_field.zero < discrete_linear_ordered_field.one
- mul_comm : ∀ (a b : α), a * b = b * a
- inv : α → α
- mul_inv_cancel : ∀ {a : α}, a ≠ 0 → a * a⁻¹ = 1
- inv_zero : 0⁻¹ = 0
- decidable_le : decidable_rel has_le.le
- decidable_eq : decidable_eq α
- decidable_lt : decidable_rel has_lt.lt
A discrete linear ordered field is a field with a decidable linear order respecting the operations.