algebra.ordered_field - mathlib docs

source

@[instance]

def linear_ordered_field.to_field (α : Type u_2) [self : linear_ordered_field α] :

field α

source

@[class]

structure linear_ordered_field (α : Type u_2) :

Type 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
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.

Instances

source

@[instance]

def linear_ordered_field.to_linear_ordered_comm_ring (α : Type u_2) [self : linear_ordered_field α] :

linear_ordered_comm_ring α

source

@[simp]

theorem inv_pos {α : Type u_1} [linear_ordered_field α] {a : α} :

0 < a⁻¹ ↔ 0 < a

source

@[simp]

theorem inv_nonneg {α : Type u_1} [linear_ordered_field α] {a : α} :

0 ≤ a⁻¹ ↔ 0 ≤ a

source

@[simp]

theorem inv_lt_zero {α : Type u_1} [linear_ordered_field α] {a : α} :

a⁻¹ < 0 ↔ a < 0

source

@[simp]

theorem inv_nonpos {α : Type u_1} [linear_ordered_field α] {a : α} :

a⁻¹ ≤ 0 ↔ a ≤ 0

source

theorem one_div_pos {α : Type u_1} [linear_ordered_field α] {a : α} :

0 < 1 / a ↔ 0 < a

source

theorem one_div_neg {α : Type u_1} [linear_ordered_field α] {a : α} :

1 / a < 0 ↔ a < 0

source

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

0 ≤ 1 / a ↔ 0 ≤ a

source

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

1 / a ≤ 0 ↔ a ≤ 0

source

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

0 < a / b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

source

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

a / b < 0 ↔ 0 < a ∧ b < 0 ∨ a < 0 ∧ 0 < b

source

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

0 ≤ a / b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

source

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

a / b ≤ 0 ↔ 0 ≤ a ∧ b ≤ 0 ∨ a ≤ 0 ∧ 0 ≤ b

source

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

0 < a / b

source

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

0 < a / b

source

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

a / b < 0

source

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

a / b < 0

source

theorem div_nonneg {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) :

0 ≤ a / b

source

theorem div_nonneg_of_nonpos {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : a ≤ 0) (hb : b ≤ 0) :

0 ≤ a / b

source

theorem div_nonpos_of_nonpos_of_nonneg {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : a ≤ 0) (hb : 0 ≤ b) :

a / b ≤ 0

source

theorem div_nonpos_of_nonneg_of_nonpos {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : 0 ≤ a) (hb : b ≤ 0) :

a / b ≤ 0

source

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

a ≤ b / c ↔ a * c ≤ b

source

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

a ≤ b / c ↔ c * a ≤ b

source

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

a / b ≤ c ↔ a ≤ c * b

source

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

a / b ≤ c ↔ a ≤ b * c

source

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

a < b / c ↔ a * c < b

source

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

a < b / c ↔ c * a < b

source

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

b / c < a ↔ b < a * c

source

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

b / c < a ↔ b < c * a

source

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

b⁻¹ * a ≤ c ↔ a ≤ b * c

source

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

b⁻¹ * a ≤ c ↔ a ≤ c * b

source

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

a * b⁻¹ ≤ c ↔ a ≤ b * c

source

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

a * b⁻¹ ≤ c ↔ a ≤ c * b

source

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

b⁻¹ * a < c ↔ a < b * c

source

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

b⁻¹ * a < c ↔ a < c * b

source

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

a * b⁻¹ < c ↔ a < b * c

source

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

a * b⁻¹ < c ↔ a < c * b

source

theorem inv_pos_le_iff_one_le_mul {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : 0 < a) :

a⁻¹ ≤ b ↔ 1 ≤ b * a

source

theorem inv_pos_le_iff_one_le_mul' {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : 0 < a) :

a⁻¹ ≤ b ↔ 1 ≤ a * b

source

theorem inv_pos_lt_iff_one_lt_mul {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : 0 < a) :

a⁻¹ < b ↔ 1 < b * a

source

theorem inv_pos_lt_iff_one_lt_mul' {α : Type u_1} [linear_ordered_field α] {a b : α} (ha : 0 < a) :

a⁻¹ < b ↔ 1 < a * b

source

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

b / c ≤ a ↔ a * c ≤ b

source

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

b / c ≤ a ↔ c * a ≤ b

source

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

a ≤ b / c ↔ b ≤ a * c

source

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

a ≤ b / c ↔ b ≤ c * a

source

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

b / c < a ↔ a * c < b

source

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

b / c < a ↔ c * a < b

source

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

a < b / c ↔ b < a * c

source

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

a < b / c ↔ b < c * a

source

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)

source

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

a / b ≤ 1

source

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

b⁻¹ ≤ a⁻¹

source

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

a⁻¹ ≤ b⁻¹ ↔ b ≤ a

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

source

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

a⁻¹ ≤ b ↔ b⁻¹ ≤ a

source

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

a ≤ b⁻¹ ↔ b ≤ a⁻¹

source

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

a⁻¹ < b⁻¹ ↔ b < a

source

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

a⁻¹ < b ↔ b⁻¹ < a

source

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

a < b⁻¹ ↔ b < a⁻¹

source

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

a⁻¹ ≤ b⁻¹ ↔ b ≤ a

source

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

a⁻¹ ≤ b ↔ b⁻¹ ≤ a

source

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

a ≤ b⁻¹ ↔ b ≤ a⁻¹

source

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

a⁻¹ < b⁻¹ ↔ b < a

source

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

a⁻¹ < b ↔ b⁻¹ < a

source

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

a < b⁻¹ ↔ b < a⁻¹

source

theorem inv_lt_one {α : Type u_1} [linear_ordered_field α] {a : α} (ha : 1 < a) :

a⁻¹ < 1

source

theorem one_lt_inv {α : Type u_1} [linear_ordered_field α] {a : α} (h₁ : 0 < a) (h₂ : a < 1) :

1 < a⁻¹

source

theorem inv_le_one {α : Type u_1} [linear_ordered_field α] {a : α} (ha : 1 ≤ a) :

a⁻¹ ≤ 1

source

theorem one_le_inv {α : Type u_1} [linear_ordered_field α] {a : α} (h₁ : 0 < a) (h₂ : a ≤ 1) :

1 ≤ a⁻¹

source

theorem inv_lt_one_iff_of_pos {α : Type u_1} [linear_ordered_field α] {a : α} (h₀ : 0 < a) :

a⁻¹ < 1 ↔ 1 < a

source

theorem inv_lt_one_iff {α : Type u_1} [linear_ordered_field α] {a : α} :

a⁻¹ < 1 ↔ a ≤ 0 ∨ 1 < a

source

theorem one_lt_inv_iff {α : Type u_1} [linear_ordered_field α] {a : α} :

1 < a⁻¹ ↔ 0 < a ∧ a < 1

source

theorem inv_le_one_iff {α : Type u_1} [linear_ordered_field α] {a : α} :

a⁻¹ ≤ 1 ↔ a ≤ 0 ∨ 1 ≤ a

source

theorem one_le_inv_iff {α : Type u_1} [linear_ordered_field α] {a : α} :

1 ≤ a⁻¹ ↔ 0 < a ∧ a ≤ 1

source

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

source

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

source

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

source

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

source

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

source

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

source

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

a / c ≤ b / c ↔ a ≤ b

source

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

source

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

a / c < b / c ↔ a < b

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

1 ≤ a / b ↔ b ≤ a

source

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

a / b ≤ 1 ↔ a ≤ b

source

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

1 < a / b ↔ b < a

source

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

a / b < 1 ↔ a < b

source

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

1 ≤ a / b ↔ a ≤ b

source

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

a / b ≤ 1 ↔ b ≤ a

source

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

1 < a / b ↔ a < b

source

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

a / b < 1 ↔ b < a

source

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

1 / a ≤ b ↔ 1 / b ≤ a

source

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

1 / a < b ↔ 1 / b < a

source

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

a ≤ 1 / b ↔ b ≤ 1 / a

source

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

a < 1 / b ↔ b < 1 / a

source

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

source

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

source

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

source

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

source

theorem one_lt_div_iff {α : Type u_1} [linear_ordered_field α] {a b : α} :

1 < a / b ↔ 0 < b ∧ b < a ∨ b < 0 ∧ a < b

source

theorem one_le_div_iff {α : Type u_1} [linear_ordered_field α] {a b : α} :

1 ≤ a / b ↔ 0 < b ∧ b ≤ a ∨ b < 0 ∧ a ≤ b

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

theorem one_lt_one_div {α : Type u_1} [linear_ordered_field α] {a : α} (h1 : 0 < a) (h2 : a < 1) :

1 < 1 / a

source

theorem one_le_one_div {α : Type u_1} [linear_ordered_field α] {a : α} (h1 : 0 < a) (h2 : a ≤ 1) :

1 ≤ 1 / a

source

theorem one_div_lt_neg_one {α : Type u_1} [linear_ordered_field α] {a : α} (h1 : a < 0) (h2 : -1 < a) :

1 / a < -1

source

theorem one_div_le_neg_one {α : Type u_1} [linear_ordered_field α] {a : α} (h1 : a < 0) (h2 : -1 ≤ a) :

1 / a ≤ -1

source

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

a / 2 + a / 2 = a

source

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

a - a / 2 = a / 2

source

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

a / 2 - a = -(a / 2)

source

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

(a + a) / 2 = a

source

theorem half_pos {α : Type u_1} [linear_ordered_field α] {a : α} (h : 0 < a) :

0 < a / 2

source

theorem one_half_pos {α : Type u_1} [linear_ordered_field α] :

0 < 1 / 2

source

theorem div_two_lt_of_pos {α : Type u_1} [linear_ordered_field α] {a : α} (h : 0 < a) :

a / 2 < a

source

theorem half_lt_self {α : Type u_1} [linear_ordered_field α] {a : α} :

0 < a → a / 2 < a

source

theorem half_le_self {α : Type u_1} [linear_ordered_field α] {a : α} (ha_nonneg : 0 ≤ a) :

a / 2 ≤ a

source

theorem one_half_lt_one {α : Type u_1} [linear_ordered_field α] :

1 / 2 < 1

source

theorem add_sub_div_two_lt {α : Type u_1} [linear_ordered_field α] {a b : α} (h : a < b) :

a + (b - a) / 2 < b

source

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 β] [nontrivial β] (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) :

linear_ordered_field β

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 := _}

source

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

source

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.

source

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 < 0 → a / c < b / d

Alias of mul_sub_mul_div_mul_neg_iff.

source

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

source

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.

source

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 ≤ 0 → a / c ≤ b / d

Alias of mul_sub_mul_div_mul_nonpos_iff.

source

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

source

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

source

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

source

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

b ≤ a

source

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)

source

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)

source

@[protected, instance]

def linear_ordered_field.to_densely_ordered {α : Type u_1} [linear_ordered_field α] :

densely_ordered α

source