mathlib documentation

algebra.ordered_field

Linear ordered fields

A linear ordered field is a field equipped with a linear order such that

Main Definitions

@[instance]
def linear_ordered_field.to_field (α : Type u_2) [s : linear_ordered_field α] :

@[class]
structure linear_ordered_field  :
Type u_2Type u_2
  • 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 bb c_1a c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = 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 < a0 < b0 < 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 : α → α
  • mul_inv_cancel : ∀ {a : α}, a 0a * a⁻¹ = 1
  • inv_zero : 0⁻¹ = 0

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

Instances

Lemmas about pos, nonneg, nonpos, neg

@[simp]
theorem inv_pos {α : Type u_1} [linear_ordered_field α] {a : α} :
0 < a⁻¹ 0 < a

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

@[simp]
theorem inv_lt_zero {α : Type u_1} [linear_ordered_field α] {a : α} :
a⁻¹ < 0 a < 0

@[simp]
theorem inv_nonpos {α : Type u_1} [linear_ordered_field α] {a : α} :
a⁻¹ 0 a 0

theorem one_div_pos {α : Type u_1} [linear_ordered_field α] {a : α} :
0 < 1 / a 0 < a

theorem one_div_neg {α : Type u_1} [linear_ordered_field α] {a : α} :
1 / a < 0 a < 0

theorem one_div_nonneg {α : Type u_1} [linear_ordered_field α] {a : α} :
0 1 / a 0 a

theorem one_div_nonpos {α : Type u_1} [linear_ordered_field α] {a : α} :
1 / a 0 a 0

theorem div_pos_iff {α : Type u_1} [linear_ordered_field α] {a b : α} :
0 < a / b 0 < a 0 < b a < 0 b < 0

theorem div_neg_iff {α : Type u_1} [linear_ordered_field α] {a b : α} :
a / b < 0 0 < a b < 0 a < 0 0 < b

theorem div_nonneg_iff {α : Type u_1} [linear_ordered_field α] {a b : α} :
0 a / b 0 a 0 b a 0 b 0

theorem div_nonpos_iff {α : Type u_1} [linear_ordered_field α] {a b : α} :
a / b 0 0 a b 0 a 0 0 b

theorem div_pos {α : Type u_1} [linear_ordered_field α] {a b : α} :
0 < a0 < b0 < a / b

theorem div_pos_of_neg_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} :
a < 0b < 00 < a / b

theorem div_neg_of_neg_of_pos {α : Type u_1} [linear_ordered_field α] {a b : α} :
a < 00 < ba / b < 0

theorem div_neg_of_pos_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} :
0 < ab < 0a / b < 0

theorem div_nonneg {α : Type u_1} [linear_ordered_field α] {a b : α} :
0 a0 b0 a / b

theorem div_nonneg_of_nonpos {α : Type u_1} [linear_ordered_field α] {a b : α} :
a 0b 00 a / b

theorem div_nonpos_of_nonpos_of_nonneg {α : Type u_1} [linear_ordered_field α] {a b : α} :
a 00 ba / b 0

theorem div_nonpos_of_nonneg_of_nonpos {α : Type u_1} [linear_ordered_field α] {a b : α} :
0 ab 0a / b 0

Relating one division with another term.

theorem le_div_iff {α : Type u_1} [linear_ordered_field α] {a b c : α} :
0 < c(a b / c a * c b)

theorem le_div_iff' {α : Type u_1} [linear_ordered_field α] {a b c : α} :
0 < c(a b / c c * a b)

theorem div_le_iff {α : Type u_1} [linear_ordered_field α] {a b c : α} :
0 < b(a / b c a c * b)

theorem div_le_iff' {α : Type u_1} [linear_ordered_field α] {a b c : α} :
0 < b(a / b c a b * c)

theorem lt_div_iff {α : Type u_1} [linear_ordered_field α] {a b c : α} :
0 < c(a < b / c a * c < b)

theorem lt_div_iff' {α : Type u_1} [linear_ordered_field α] {a b c : α} :
0 < c(a < b / c c * a < b)

theorem div_lt_iff {α : Type u_1} [linear_ordered_field α] {a b c : α} :
0 < c(b / c < a b < a * c)

theorem div_lt_iff' {α : Type u_1} [linear_ordered_field α] {a b c : α} :
0 < c(b / c < a b < c * a)

theorem inv_mul_le_iff {α : Type u_1} [linear_ordered_field α] {a b c : α} :
0 < b(b⁻¹ * a c a b * c)

theorem inv_mul_le_iff' {α : Type u_1} [linear_ordered_field α] {a b c : α} :
0 < b(b⁻¹ * a c a c * b)

theorem mul_inv_le_iff {α : Type u_1} [linear_ordered_field α] {a b c : α} :
0 < b(a * b⁻¹ c a b * c)

theorem mul_inv_le_iff' {α : Type u_1} [linear_ordered_field α] {a b c : α} :
0 < b(a * b⁻¹ c a c * b)

theorem inv_mul_lt_iff {α : Type u_1} [linear_ordered_field α] {a b c : α} :
0 < b(b⁻¹ * a < c a < b * c)

theorem inv_mul_lt_iff' {α : Type u_1} [linear_ordered_field α] {a b c : α} :
0 < b(b⁻¹ * a < c a < c * b)

theorem mul_inv_lt_iff {α : Type u_1} [linear_ordered_field α] {a b c : α} :
0 < b(a * b⁻¹ < c a < b * c)

theorem mul_inv_lt_iff' {α : Type u_1} [linear_ordered_field α] {a b c : α} :
0 < b(a * b⁻¹ < c a < c * b)

theorem div_le_iff_of_neg {α : Type u_1} [linear_ordered_field α] {a b c : α} :
c < 0(b / c a a * c b)

theorem div_le_iff_of_neg' {α : Type u_1} [linear_ordered_field α] {a b c : α} :
c < 0(b / c a c * a b)

theorem le_div_iff_of_neg {α : Type u_1} [linear_ordered_field α] {a b c : α} :
c < 0(a b / c b a * c)

theorem le_div_iff_of_neg' {α : Type u_1} [linear_ordered_field α] {a b c : α} :
c < 0(a b / c b c * a)

theorem div_lt_iff_of_neg {α : Type u_1} [linear_ordered_field α] {a b c : α} :
c < 0(b / c < a a * c < b)

theorem div_lt_iff_of_neg' {α : Type u_1} [linear_ordered_field α] {a b c : α} :
c < 0(b / c < a c * a < b)

theorem lt_div_iff_of_neg {α : Type u_1} [linear_ordered_field α] {a b c : α} :
c < 0(a < b / c b < a * c)

theorem lt_div_iff_of_neg' {α : Type u_1} [linear_ordered_field α] {a b c : α} :
c < 0(a < b / c b < c * a)

theorem div_le_iff_of_nonneg_of_le {α : Type u_1} [linear_ordered_field α] {a b c : α} :
0 b0 ca c * ba / b c

One direction of div_le_iff where b is allowed to be 0 (but c must be nonnegative)

Bi-implications of inequalities using inversions

theorem inv_le_inv_of_le {α : Type u_1} [linear_ordered_field α] {a b : α} :
0 < aa bb⁻¹ a⁻¹

theorem inv_le_inv {α : Type u_1} [linear_ordered_field α] {a b : α} :
0 < a0 < b(a⁻¹ b⁻¹ b a)

See inv_le_inv_of_le for the implication from right-to-left with one fewer assumption.

theorem inv_le {α : Type u_1} [linear_ordered_field α] {a b : α} :
0 < a0 < b(a⁻¹ b b⁻¹ a)

theorem le_inv {α : Type u_1} [linear_ordered_field α] {a b : α} :
0 < a0 < b(a b⁻¹ b a⁻¹)

theorem inv_lt_inv {α : Type u_1} [linear_ordered_field α] {a b : α} :
0 < a0 < b(a⁻¹ < b⁻¹ b < a)

theorem inv_lt {α : Type u_1} [linear_ordered_field α] {a b : α} :
0 < a0 < b(a⁻¹ < b b⁻¹ < a)

theorem lt_inv {α : Type u_1} [linear_ordered_field α] {a b : α} :
0 < a0 < b(a < b⁻¹ b < a⁻¹)

theorem inv_le_inv_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} :
a < 0b < 0(a⁻¹ b⁻¹ b a)

theorem inv_le_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} :
a < 0b < 0(a⁻¹ b b⁻¹ a)

theorem le_inv_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} :
a < 0b < 0(a b⁻¹ b a⁻¹)

theorem inv_lt_inv_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} :
a < 0b < 0(a⁻¹ < b⁻¹ b < a)

theorem inv_lt_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} :
a < 0b < 0(a⁻¹ < b b⁻¹ < a)

theorem lt_inv_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} :
a < 0b < 0(a < b⁻¹ b < a⁻¹)

theorem inv_lt_one {α : Type u_1} [linear_ordered_field α] {a : α} :
1 < aa⁻¹ < 1

theorem one_lt_inv {α : Type u_1} [linear_ordered_field α] {a : α} :
0 < aa < 11 < a⁻¹

theorem inv_le_one {α : Type u_1} [linear_ordered_field α] {a : α} :
1 aa⁻¹ 1

theorem one_le_inv {α : Type u_1} [linear_ordered_field α] {a : α} :
0 < aa 11 a⁻¹

theorem inv_lt_one_iff_of_pos {α : Type u_1} [linear_ordered_field α] {a : α} :
0 < a(a⁻¹ < 1 1 < a)

theorem inv_lt_one_iff {α : Type u_1} [linear_ordered_field α] {a : α} :
a⁻¹ < 1 a 0 1 < a

theorem one_lt_inv_iff {α : Type u_1} [linear_ordered_field α] {a : α} :
1 < a⁻¹ 0 < a a < 1

theorem inv_le_one_iff {α : Type u_1} [linear_ordered_field α] {a : α} :
a⁻¹ 1 a 0 1 a

theorem one_le_inv_iff {α : Type u_1} [linear_ordered_field α] {a : α} :
1 a⁻¹ 0 < a a 1

Relating two divisions.

theorem div_le_div_of_le {α : Type u_1} [linear_ordered_field α] {a b c : α} :
0 ca ba / c b / c

theorem div_le_div_of_le_left {α : Type u_1} [linear_ordered_field α] {a b c : α} :
0 a0 < cc ba / b a / c

theorem div_le_div_of_le_of_nonneg {α : Type u_1} [linear_ordered_field α] {a b c : α} :
a b0 ca / c b / c

theorem div_le_div_of_nonpos_of_le {α : Type u_1} [linear_ordered_field α] {a b c : α} :
c 0b aa / c b / c

theorem div_lt_div_of_lt {α : Type u_1} [linear_ordered_field α] {a b c : α} :
0 < ca < ba / c < b / c

theorem div_lt_div_of_neg_of_lt {α : Type u_1} [linear_ordered_field α] {a b c : α} :
c < 0b < aa / c < b / c

theorem div_le_div_right {α : Type u_1} [linear_ordered_field α] {a b c : α} :
0 < c(a / c b / c a b)

theorem div_le_div_right_of_neg {α : Type u_1} [linear_ordered_field α] {a b c : α} :
c < 0(a / c b / c b a)

theorem div_lt_div_right {α : Type u_1} [linear_ordered_field α] {a b c : α} :
0 < c(a / c < b / c a < b)

theorem div_lt_div_right_of_neg {α : Type u_1} [linear_ordered_field α] {a b c : α} :
c < 0(a / c < b / c b < a)

theorem div_lt_div_left {α : Type u_1} [linear_ordered_field α] {a b c : α} :
0 < a0 < b0 < c(a / b < a / c c < b)

theorem div_le_div_left {α : Type u_1} [linear_ordered_field α] {a b c : α} :
0 < a0 < b0 < c(a / b a / c c b)

theorem div_lt_div_iff {α : Type u_1} [linear_ordered_field α] {a b c d : α} :
0 < b0 < d(a / b < c / d a * d < c * b)

theorem div_le_div_iff {α : Type u_1} [linear_ordered_field α] {a b c d : α} :
0 < b0 < d(a / b c / d a * d c * b)

theorem div_le_div {α : Type u_1} [linear_ordered_field α] {a b c d : α} :
0 ca c0 < dd ba / b c / d

theorem div_lt_div {α : Type u_1} [linear_ordered_field α] {a b c d : α} :
a < cd b0 c0 < da / b < c / d

theorem div_lt_div' {α : Type u_1} [linear_ordered_field α] {a b c d : α} :
a cd < b0 < c0 < da / b < c / d

theorem div_lt_div_of_lt_left {α : Type u_1} [linear_ordered_field α] {a b c : α} :
0 < bb < a0 < cc / a < c / b

Relating one division and involving 1

theorem one_le_div {α : Type u_1} [linear_ordered_field α] {a b : α} :
0 < b(1 a / b b a)

theorem div_le_one {α : Type u_1} [linear_ordered_field α] {a b : α} :
0 < b(a / b 1 a b)

theorem one_lt_div {α : Type u_1} [linear_ordered_field α] {a b : α} :
0 < b(1 < a / b b < a)

theorem div_lt_one {α : Type u_1} [linear_ordered_field α] {a b : α} :
0 < b(a / b < 1 a < b)

theorem one_le_div_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} :
b < 0(1 a / b a b)

theorem div_le_one_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} :
b < 0(a / b 1 b a)

theorem one_lt_div_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} :
b < 0(1 < a / b a < b)

theorem div_lt_one_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} :
b < 0(a / b < 1 b < a)

theorem one_div_le {α : Type u_1} [linear_ordered_field α] {a b : α} :
0 < a0 < b(1 / a b 1 / b a)

theorem one_div_lt {α : Type u_1} [linear_ordered_field α] {a b : α} :
0 < a0 < b(1 / a < b 1 / b < a)

theorem le_one_div {α : Type u_1} [linear_ordered_field α] {a b : α} :
0 < a0 < b(a 1 / b b 1 / a)

theorem lt_one_div {α : Type u_1} [linear_ordered_field α] {a b : α} :
0 < a0 < b(a < 1 / b b < 1 / a)

theorem one_div_le_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} :
a < 0b < 0(1 / a b 1 / b a)

theorem one_div_lt_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} :
a < 0b < 0(1 / a < b 1 / b < a)

theorem le_one_div_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} :
a < 0b < 0(a 1 / b b 1 / a)

theorem lt_one_div_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} :
a < 0b < 0(a < 1 / b b < 1 / a)

theorem one_lt_div_iff {α : Type u_1} [linear_ordered_field α] {a b : α} :
1 < a / b 0 < b b < a b < 0 a < b

theorem one_le_div_iff {α : Type u_1} [linear_ordered_field α] {a b : α} :
1 a / b 0 < b b a b < 0 a b

theorem div_lt_one_iff {α : Type u_1} [linear_ordered_field α] {a b : α} :
a / b < 1 0 < b a < b b = 0 b < 0 b < a

theorem div_le_one_iff {α : Type u_1} [linear_ordered_field α] {a b : α} :
a / b 1 0 < b a b b = 0 b < 0 b a

Relating two divisions, involving 1

theorem one_div_le_one_div_of_le {α : Type u_1} [linear_ordered_field α] {a b : α} :
0 < aa b1 / b 1 / a

theorem one_div_lt_one_div_of_lt {α : Type u_1} [linear_ordered_field α] {a b : α} :
0 < aa < b1 / b < 1 / a

theorem one_div_le_one_div_of_neg_of_le {α : Type u_1} [linear_ordered_field α] {a b : α} :
b < 0a b1 / b 1 / a

theorem one_div_lt_one_div_of_neg_of_lt {α : Type u_1} [linear_ordered_field α] {a b : α} :
b < 0a < b1 / b < 1 / a

theorem le_of_one_div_le_one_div {α : Type u_1} [linear_ordered_field α] {a b : α} :
0 < a1 / a 1 / bb a

theorem lt_of_one_div_lt_one_div {α : Type u_1} [linear_ordered_field α] {a b : α} :
0 < a1 / a < 1 / bb < a

theorem le_of_neg_of_one_div_le_one_div {α : Type u_1} [linear_ordered_field α] {a b : α} :
b < 01 / a 1 / bb a

theorem lt_of_neg_of_one_div_lt_one_div {α : Type u_1} [linear_ordered_field α] {a b : α} :
b < 01 / a < 1 / bb < a

theorem one_div_le_one_div {α : Type u_1} [linear_ordered_field α] {a b : α} :
0 < a0 < b(1 / a 1 / b b a)

For the single implications with fewer assumptions, see one_div_le_one_div_of_le and le_of_one_div_le_one_div

theorem one_div_lt_one_div {α : Type u_1} [linear_ordered_field α] {a b : α} :
0 < a0 < b(1 / a < 1 / b b < a)

For the single implications with fewer assumptions, see one_div_lt_one_div_of_lt and lt_of_one_div_lt_one_div

theorem one_div_le_one_div_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} :
a < 0b < 0(1 / a 1 / b b a)

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

theorem one_div_lt_one_div_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} :
a < 0b < 0(1 / a < 1 / b b < a)

For the single implications with fewer assumptions, see one_div_lt_one_div_of_lt and lt_of_one_div_lt_one_div

theorem one_lt_one_div {α : Type u_1} [linear_ordered_field α] {a : α} :
0 < aa < 11 < 1 / a

theorem one_le_one_div {α : Type u_1} [linear_ordered_field α] {a : α} :
0 < aa 11 1 / a

theorem one_div_lt_neg_one {α : Type u_1} [linear_ordered_field α] {a : α} :
a < 0-1 < a1 / a < -1

theorem one_div_le_neg_one {α : Type u_1} [linear_ordered_field α] {a : α} :
a < 0-1 a1 / a -1

Results about halving.

The equalities also hold in fields of characteristic 0.

theorem add_halves {α : Type u_1} [linear_ordered_field α] (a : α) :
a / 2 + a / 2 = a

theorem sub_self_div_two {α : Type u_1} [linear_ordered_field α] (a : α) :
a - a / 2 = a / 2

theorem div_two_sub_self {α : Type u_1} [linear_ordered_field α] (a : α) :
a / 2 - a = -(a / 2)

theorem add_self_div_two {α : Type u_1} [linear_ordered_field α] (a : α) :
(a + a) / 2 = a

theorem half_pos {α : Type u_1} [linear_ordered_field α] {a : α} :
0 < a0 < a / 2

theorem one_half_pos {α : Type u_1} [linear_ordered_field α] :
0 < 1 / 2

theorem div_two_lt_of_pos {α : Type u_1} [linear_ordered_field α] {a : α} :
0 < aa / 2 < a

theorem half_lt_self {α : Type u_1} [linear_ordered_field α] {a : α} :
0 < aa / 2 < a

theorem one_half_lt_one {α : Type u_1} [linear_ordered_field α] :
1 / 2 < 1

theorem add_sub_div_two_lt {α : Type u_1} [linear_ordered_field α] {a b : α} :
a < ba + (b - a) / 2 < b

Miscellaneous lemmas

theorem mul_sub_mul_div_mul_neg_iff {α : Type u_1} [linear_ordered_field α] {a b c d : α} :
c 0d 0((a * d - b * c) / c * d < 0 a / c < b / d)

theorem mul_sub_mul_div_mul_nonpos_iff {α : Type u_1} [linear_ordered_field α] {a b c d : α} :
c 0d 0((a * d - b * c) / c * d 0 a / c b / d)

theorem mul_le_mul_of_mul_div_le {α : Type u_1} [linear_ordered_field α] {a b c d : α} :
a * (b / c) d0 < cb * a d * c

theorem div_mul_le_div_mul_of_div_le_div {α : Type u_1} [linear_ordered_field α] {a b c d e : α} :
a / b c / d0 ea / b * e c / d * e

theorem exists_add_lt_and_pos_of_lt {α : Type u_1} [linear_ordered_field α] {a b : α} :
b < a(∃ (c : α), b + c < a 0 < c)

theorem le_of_forall_sub_le {α : Type u_1} [linear_ordered_field α] {a b : α} :
(∀ (ε : α), ε > 0b - ε a)b a

theorem monotone.div_const {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [preorder β] {f : β → α} (hf : monotone f) {c : α} :
0 cmonotone (λ (x : β), f x / c)

theorem strict_mono.div_const {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [preorder β] {f : β → α} (hf : strict_mono f) {c : α} :
0 < cstrict_mono (λ (x : β), f x / c)

theorem mul_self_inj_of_nonneg {α : Type u_1} [linear_ordered_field α] {a b : α} :
0 a0 b(a * a = b * b a = b)

theorem min_div_div_right {α : Type u_1} [linear_ordered_field α] {c : α} (hc : 0 c) (a b : α) :
min (a / c) (b / c) = min a b / c

theorem max_div_div_right {α : Type u_1} [linear_ordered_field α] {c : α} (hc : 0 c) (a b : α) :
max (a / c) (b / c) = max a b / c

theorem min_div_div_right_of_nonpos {α : Type u_1} [linear_ordered_field α] {c : α} (hc : c 0) (a b : α) :
min (a / c) (b / c) = max a b / c

theorem max_div_div_right_of_nonpos {α : Type u_1} [linear_ordered_field α] {c : α} (hc : c 0) (a b : α) :
max (a / c) (b / c) = min a b / c

theorem abs_div {α : Type u_1} [linear_ordered_field α] (a b : α) :
abs (a / b) = abs a / abs b

theorem abs_one_div {α : Type u_1} [linear_ordered_field α] (a : α) :
abs (1 / a) = 1 / abs a

theorem abs_inv {α : Type u_1} [linear_ordered_field α] (a : α) :