mathlib documentation

algebra.order.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) [self : linear_ordered_field α] :
@[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
def order_iso.mul_left₀ {α : Type u_1} [linear_ordered_field α] (a : α) (ha : 0 < a) :
α ≃o α

equiv.mul_left₀ as an order_iso.

Equations
@[simp]
theorem order_iso.mul_left₀_apply {α : Type u_1} [linear_ordered_field α] (a : α) (ha : 0 < a) (ᾰ : α) :
(order_iso.mul_left₀ a ha) = a *
@[simp]
theorem order_iso.mul_left₀_symm_apply {α : Type u_1} [linear_ordered_field α] (a : α) (ha : 0 < a) (ᾰ : α) :
@[simp]
theorem order_iso.mul_right₀_symm_apply {α : Type u_1} [linear_ordered_field α] (a : α) (ha : 0 < a) (ᾰ : α) :
def order_iso.mul_right₀ {α : Type u_1} [linear_ordered_field α] (a : α) (ha : 0 < a) :
α ≃o α

equiv.mul_right₀ as an order_iso.

Equations
@[simp]
theorem order_iso.mul_right₀_apply {α : Type u_1} [linear_ordered_field α] (a : α) (ha : 0 < a) (ᾰ : α) :
(order_iso.mul_right₀ a ha) = * a

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 : α} (ha : 0 < a) (hb : 0 < b) :
0 < a / b
theorem div_pos_of_neg_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : a < 0) (hb : b < 0) :
0 < a / b
theorem div_neg_of_neg_of_pos {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : a < 0) (hb : 0 < b) :
a / b < 0
theorem div_neg_of_pos_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : 0 < a) (hb : b < 0) :
a / b < 0
theorem div_nonneg {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : 0 a) (hb : 0 b) :
0 a / b
theorem div_nonneg_of_nonpos {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : a 0) (hb : b 0) :
0 a / b
theorem div_nonpos_of_nonpos_of_nonneg {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : a 0) (hb : 0 b) :
a / b 0
theorem div_nonpos_of_nonneg_of_nonpos {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : 0 a) (hb : b 0) :
a / b 0

Relating one division with another term. #

theorem le_div_iff {α : Type u_1} [linear_ordered_field α] {a b c : α} (hc : 0 < c) :
a b / c a * c b
theorem le_div_iff' {α : Type u_1} [linear_ordered_field α] {a b c : α} (hc : 0 < c) :
a b / c c * a b
theorem div_le_iff {α : Type u_1} [linear_ordered_field α] {a b c : α} (hb : 0 < b) :
a / b c a c * b
theorem div_le_iff' {α : Type u_1} [linear_ordered_field α] {a b c : α} (hb : 0 < b) :
a / b c a b * c
theorem lt_div_iff {α : Type u_1} [linear_ordered_field α] {a b c : α} (hc : 0 < c) :
a < b / c a * c < b
theorem lt_div_iff' {α : Type u_1} [linear_ordered_field α] {a b c : α} (hc : 0 < c) :
a < b / c c * a < b
theorem div_lt_iff {α : Type u_1} [linear_ordered_field α] {a b c : α} (hc : 0 < c) :
b / c < a b < a * c
theorem div_lt_iff' {α : Type u_1} [linear_ordered_field α] {a b c : α} (hc : 0 < c) :
b / c < a b < c * a
theorem inv_mul_le_iff {α : Type u_1} [linear_ordered_field α] {a b c : α} (h : 0 < b) :
b⁻¹ * a c a b * c
theorem inv_mul_le_iff' {α : Type u_1} [linear_ordered_field α] {a b c : α} (h : 0 < b) :
b⁻¹ * a c a c * b
theorem mul_inv_le_iff {α : Type u_1} [linear_ordered_field α] {a b c : α} (h : 0 < b) :
a * b⁻¹ c a b * c
theorem mul_inv_le_iff' {α : Type u_1} [linear_ordered_field α] {a b c : α} (h : 0 < b) :
a * b⁻¹ c a c * b
theorem inv_mul_lt_iff {α : Type u_1} [linear_ordered_field α] {a b c : α} (h : 0 < b) :
b⁻¹ * a < c a < b * c
theorem inv_mul_lt_iff' {α : Type u_1} [linear_ordered_field α] {a b c : α} (h : 0 < b) :
b⁻¹ * a < c a < c * b
theorem mul_inv_lt_iff {α : Type u_1} [linear_ordered_field α] {a b c : α} (h : 0 < b) :
a * b⁻¹ < c a < b * c
theorem mul_inv_lt_iff' {α : Type u_1} [linear_ordered_field α] {a b c : α} (h : 0 < b) :
a * b⁻¹ < c a < c * b
theorem inv_pos_le_iff_one_le_mul {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : 0 < a) :
a⁻¹ b 1 b * a
theorem inv_pos_le_iff_one_le_mul' {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : 0 < a) :
a⁻¹ b 1 a * b
theorem inv_pos_lt_iff_one_lt_mul {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : 0 < a) :
a⁻¹ < b 1 < b * a
theorem inv_pos_lt_iff_one_lt_mul' {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : 0 < a) :
a⁻¹ < b 1 < a * b
theorem div_le_iff_of_neg {α : Type u_1} [linear_ordered_field α] {a b c : α} (hc : c < 0) :
b / c a a * c b
theorem div_le_iff_of_neg' {α : Type u_1} [linear_ordered_field α] {a b c : α} (hc : c < 0) :
b / c a c * a b
theorem le_div_iff_of_neg {α : Type u_1} [linear_ordered_field α] {a b c : α} (hc : c < 0) :
a b / c b a * c
theorem le_div_iff_of_neg' {α : Type u_1} [linear_ordered_field α] {a b c : α} (hc : c < 0) :
a b / c b c * a
theorem div_lt_iff_of_neg {α : Type u_1} [linear_ordered_field α] {a b c : α} (hc : c < 0) :
b / c < a a * c < b
theorem div_lt_iff_of_neg' {α : Type u_1} [linear_ordered_field α] {a b c : α} (hc : c < 0) :
b / c < a c * a < b
theorem lt_div_iff_of_neg {α : Type u_1} [linear_ordered_field α] {a b c : α} (hc : c < 0) :
a < b / c b < a * c
theorem lt_div_iff_of_neg' {α : Type u_1} [linear_ordered_field α] {a b c : α} (hc : c < 0) :
a < b / c b < c * a
theorem div_le_of_nonneg_of_le_mul {α : Type u_1} [linear_ordered_field α] {a b c : α} (hb : 0 b) (hc : 0 c) (h : a c * b) :
a / b c

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

theorem div_le_one_of_le {α : Type u_1} [linear_ordered_field α] {a b : α} (h : a b) (hb : 0 b) :
a / b 1

Bi-implications of inequalities using inversions #

theorem inv_le_inv_of_le {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : 0 < a) (h : a b) :
theorem inv_le_inv {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : 0 < a) (hb : 0 < b) :

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 : α} (ha : 0 < a) (hb : 0 < b) :

In a linear ordered field, for positive a and b we have a⁻¹ ≤ b ↔ b⁻¹ ≤ a. See also inv_le_of_inv_le for a one-sided implication with one fewer assumption.

theorem inv_le_of_inv_le {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : 0 < a) (h : a⁻¹ b) :
theorem le_inv {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : 0 < a) (hb : 0 < b) :
theorem inv_lt_inv {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : 0 < a) (hb : 0 < b) :
a⁻¹ < b⁻¹ b < a
theorem inv_lt {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : 0 < a) (hb : 0 < b) :
a⁻¹ < b b⁻¹ < a

In a linear ordered field, for positive a and b we have a⁻¹ < b ↔ b⁻¹ < a. See also inv_lt_of_inv_lt for a one-sided implication with one fewer assumption.

theorem inv_lt_of_inv_lt {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : 0 < a) (h : a⁻¹ < b) :
b⁻¹ < a
theorem lt_inv {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : 0 < a) (hb : 0 < b) :
a < b⁻¹ b < a⁻¹
theorem inv_le_inv_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : a < 0) (hb : b < 0) :
theorem inv_le_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : a < 0) (hb : b < 0) :
theorem le_inv_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : a < 0) (hb : b < 0) :
theorem inv_lt_inv_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : a < 0) (hb : b < 0) :
a⁻¹ < b⁻¹ b < a
theorem inv_lt_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : a < 0) (hb : b < 0) :
a⁻¹ < b b⁻¹ < a
theorem lt_inv_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : a < 0) (hb : b < 0) :
a < b⁻¹ b < a⁻¹
theorem inv_lt_one {α : Type u_1} [linear_ordered_field α] {a : α} (ha : 1 < a) :
a⁻¹ < 1
theorem one_lt_inv {α : Type u_1} [linear_ordered_field α] {a : α} (h₁ : 0 < a) (h₂ : a < 1) :
1 < a⁻¹
theorem inv_le_one {α : Type u_1} [linear_ordered_field α] {a : α} (ha : 1 a) :
theorem one_le_inv {α : Type u_1} [linear_ordered_field α] {a : α} (h₁ : 0 < a) (h₂ : a 1) :
theorem inv_lt_one_iff_of_pos {α : Type u_1} [linear_ordered_field α] {a : α} (h₀ : 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 : α} (hc : 0 c) (h : a b) :
a / c b / c
theorem div_le_div_of_le_left {α : Type u_1} [linear_ordered_field α] {a b c : α} (ha : 0 a) (hc : 0 < c) (h : c b) :
a / b a / c
theorem div_le_div_of_le_of_nonneg {α : Type u_1} [linear_ordered_field α] {a b c : α} (hab : a b) (hc : 0 c) :
a / c b / c
theorem div_le_div_of_nonpos_of_le {α : Type u_1} [linear_ordered_field α] {a b c : α} (hc : c 0) (h : b a) :
a / c b / c
theorem div_lt_div_of_lt {α : Type u_1} [linear_ordered_field α] {a b c : α} (hc : 0 < c) (h : a < b) :
a / c < b / c
theorem div_lt_div_of_neg_of_lt {α : Type u_1} [linear_ordered_field α] {a b c : α} (hc : c < 0) (h : b < a) :
a / c < b / c
theorem div_le_div_right {α : Type u_1} [linear_ordered_field α] {a b c : α} (hc : 0 < c) :
a / c b / c a b
theorem div_le_div_right_of_neg {α : Type u_1} [linear_ordered_field α] {a b c : α} (hc : c < 0) :
a / c b / c b a
theorem div_lt_div_right {α : Type u_1} [linear_ordered_field α] {a b c : α} (hc : 0 < c) :
a / c < b / c a < b
theorem div_lt_div_right_of_neg {α : Type u_1} [linear_ordered_field α] {a b c : α} (hc : c < 0) :
a / c < b / c b < a
theorem div_lt_div_left {α : Type u_1} [linear_ordered_field α] {a b c : α} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
a / b < a / c c < b
theorem div_le_div_left {α : Type u_1} [linear_ordered_field α] {a b c : α} (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
a / b a / c c b
theorem div_lt_div_iff {α : Type u_1} [linear_ordered_field α] {a b c d : α} (b0 : 0 < b) (d0 : 0 < d) :
a / b < c / d a * d < c * b
theorem div_le_div_iff {α : Type u_1} [linear_ordered_field α] {a b c d : α} (b0 : 0 < b) (d0 : 0 < d) :
a / b c / d a * d c * b
theorem div_le_div {α : Type u_1} [linear_ordered_field α] {a b c d : α} (hc : 0 c) (hac : a c) (hd : 0 < d) (hbd : d b) :
a / b c / d
theorem div_lt_div {α : Type u_1} [linear_ordered_field α] {a b c d : α} (hac : a < c) (hbd : d b) (c0 : 0 c) (d0 : 0 < d) :
a / b < c / d
theorem div_lt_div' {α : Type u_1} [linear_ordered_field α] {a b c d : α} (hac : a c) (hbd : d < b) (c0 : 0 < c) (d0 : 0 < d) :
a / b < c / d
theorem div_lt_div_of_lt_left {α : Type u_1} [linear_ordered_field α] {a b c : α} (hb : 0 < b) (h : b < a) (hc : 0 < c) :
c / a < c / b

Relating one division and involving 1 #

theorem one_le_div {α : Type u_1} [linear_ordered_field α] {a b : α} (hb : 0 < b) :
1 a / b b a
theorem div_le_one {α : Type u_1} [linear_ordered_field α] {a b : α} (hb : 0 < b) :
a / b 1 a b
theorem one_lt_div {α : Type u_1} [linear_ordered_field α] {a b : α} (hb : 0 < b) :
1 < a / b b < a
theorem div_lt_one {α : Type u_1} [linear_ordered_field α] {a b : α} (hb : 0 < b) :
a / b < 1 a < b
theorem one_le_div_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} (hb : b < 0) :
1 a / b a b
theorem div_le_one_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} (hb : b < 0) :
a / b 1 b a
theorem one_lt_div_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} (hb : b < 0) :
1 < a / b a < b
theorem div_lt_one_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} (hb : b < 0) :
a / b < 1 b < a
theorem one_div_le {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : 0 < a) (hb : 0 < b) :
1 / a b 1 / b a
theorem one_div_lt {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : 0 < a) (hb : 0 < b) :
1 / a < b 1 / b < a
theorem le_one_div {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : 0 < a) (hb : 0 < b) :
a 1 / b b 1 / a
theorem lt_one_div {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : 0 < a) (hb : 0 < b) :
a < 1 / b b < 1 / a
theorem one_div_le_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : a < 0) (hb : b < 0) :
1 / a b 1 / b a
theorem one_div_lt_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : a < 0) (hb : b < 0) :
1 / a < b 1 / b < a
theorem le_one_div_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : a < 0) (hb : b < 0) :
a 1 / b b 1 / a
theorem lt_one_div_of_neg {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : a < 0) (hb : b < 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 : α} (ha : 0 < a) (h : a b) :
1 / b 1 / a
theorem one_div_lt_one_div_of_lt {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : 0 < a) (h : a < b) :
1 / b < 1 / a
theorem one_div_le_one_div_of_neg_of_le {α : Type u_1} [linear_ordered_field α] {a b : α} (hb : b < 0) (h : a b) :
1 / b 1 / a
theorem one_div_lt_one_div_of_neg_of_lt {α : Type u_1} [linear_ordered_field α] {a b : α} (hb : b < 0) (h : a < b) :
1 / b < 1 / a
theorem le_of_one_div_le_one_div {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : 0 < a) (h : 1 / a 1 / b) :
b a
theorem lt_of_one_div_lt_one_div {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : 0 < a) (h : 1 / a < 1 / b) :
b < a
theorem le_of_neg_of_one_div_le_one_div {α : Type u_1} [linear_ordered_field α] {a b : α} (hb : b < 0) (h : 1 / a 1 / b) :
b a
theorem lt_of_neg_of_one_div_lt_one_div {α : Type u_1} [linear_ordered_field α] {a b : α} (hb : b < 0) (h : 1 / a < 1 / b) :
b < a
theorem one_div_le_one_div {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : 0 < a) (hb : 0 < 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 : α} (ha : 0 < a) (hb : 0 < 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 : α} (ha : a < 0) (hb : b < 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 : α} (ha : a < 0) (hb : b < 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 : α} (h1 : 0 < a) (h2 : a < 1) :
1 < 1 / a
theorem one_le_one_div {α : Type u_1} [linear_ordered_field α] {a : α} (h1 : 0 < a) (h2 : a 1) :
1 1 / a
theorem one_div_lt_neg_one {α : Type u_1} [linear_ordered_field α] {a : α} (h1 : a < 0) (h2 : -1 < a) :
1 / a < -1
theorem one_div_le_neg_one {α : Type u_1} [linear_ordered_field α] {a : α} (h1 : a < 0) (h2 : -1 a) :
1 / 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 : α} (h : 0 < a) :
0 < 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 : α} (h : 0 < a) :
a / 2 < a
theorem half_lt_self {α : Type u_1} [linear_ordered_field α] {a : α} :
0 < aa / 2 < a
theorem half_le_self {α : Type u_1} [linear_ordered_field α] {a : α} (ha_nonneg : 0 a) :
a / 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 : α} (h : a < b) :
a + (b - a) / 2 < b
theorem left_lt_add_div_two {α : Type u_1} [linear_ordered_field α] {a b : α} :
a < (a + b) / 2 a < b
theorem add_div_two_lt_right {α : Type u_1} [linear_ordered_field α] {a b : α} :
(a + b) / 2 < b a < b
theorem sub_one_div_inv_le_two {α : Type u_1} [linear_ordered_field α] {a : α} (a2 : 2 a) :
(1 - 1 / a)⁻¹ 2

An inequality involving 2.

Miscellaneous lemmas #

def function.injective.linear_ordered_field {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [has_zero β] [has_one β] [has_add β] [has_mul β] [has_neg β] [has_sub β] [has_inv β] [has_div β] (f : β → α) (hf : function.injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ (x y : β), f (x + y) = f x + f y) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) (neg : ∀ (x : β), f (-x) = -f x) (sub : ∀ (x y : β), f (x - y) = f x - f y) (inv : ∀ (x : β), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : β), f (x / y) = f x / f y) :

Pullback a linear_ordered_field under an injective map. See note [reducible non-instances].

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

Alias of mul_sub_mul_div_mul_neg_iff.

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

Alias of mul_sub_mul_div_mul_neg_iff.

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

Alias of mul_sub_mul_div_mul_nonpos_iff.

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

Alias of mul_sub_mul_div_mul_nonpos_iff.

theorem mul_le_mul_of_mul_div_le {α : Type u_1} [linear_ordered_field α] {a b c d : α} (h : a * (b / c) d) (hc : 0 < c) :
b * a d * c
theorem div_mul_le_div_mul_of_div_le_div {α : Type u_1} [linear_ordered_field α] {a b c d e : α} (h : a / b c / d) (he : 0 e) :
a / b * e c / d * e
theorem exists_add_lt_and_pos_of_lt {α : Type u_1} [linear_ordered_field α] {a b : α} (h : b < a) :
∃ (c : α), b + c < a 0 < c
theorem exists_pos_mul_lt {α : Type u_1} [linear_ordered_field α] {a : α} (h : 0 < a) (b : α) :
∃ (c : α), 0 < c b * c < a
theorem le_of_forall_sub_le {α : Type u_1} [linear_ordered_field α] {a b : α} (h : ∀ (ε : α), ε > 0b - ε a) :
b a
theorem monotone.div_const {α : Type u_1} [linear_ordered_field α] {β : Type u_2} [preorder β] {f : β → α} (hf : monotone f) {c : α} (hc : 0 c) :
monotone (λ (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 : α} (hc : 0 < c) :
strict_mono (λ (x : β), f x / c)
@[protected, instance]
theorem mul_self_inj_of_nonneg {α : Type u_1} [linear_ordered_field α] {a b : α} (a0 : 0 a) (b0 : 0 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 : α) :
|a / b| = |a| / |b|
theorem abs_one_div {α : Type u_1} [linear_ordered_field α] (a : α) :
|1 / a| = 1 / |a|
theorem abs_inv {α : Type u_1} [linear_ordered_field α] (a : α) :
theorem one_div_strict_anti_on {α : Type u_1} [linear_ordered_field α] :
strict_anti_on (λ (x : α), 1 / x) (set.Ioi 0)
theorem one_div_pow_le_one_div_pow_of_le {α : Type u_1} [linear_ordered_field α] {a : α} (a1 : 1 a) {m n : } (mn : m n) :
1 / a ^ n 1 / a ^ m
theorem one_div_pow_lt_one_div_pow_of_lt {α : Type u_1} [linear_ordered_field α] {a : α} (a1 : 1 < a) {m n : } (mn : m < n) :
1 / a ^ n < 1 / a ^ m
theorem one_div_pow_mono {α : Type u_1} [linear_ordered_field α] {a : α} (a1 : 1 a) :
theorem one_div_pow_strict_mono {α : Type u_1} [linear_ordered_field α] {a : α} (a1 : 1 < a) :