• add : α → α → α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : ℕ → α → α
• nsmul_zero' : (∀ (x : α), linear_ordered_semifield.nsmul 0 x = 0) . "try_refl_tac"
• nsmul_succ' : (∀ (n : ℕ) (x : α), linear_ordered_semifield.nsmul n.succ x = x + linear_ordered_semifield.nsmul n x) . "try_refl_tac"
• add_comm : ∀ (a b : α), a + b = b + a
• mul : α → α → α
• left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• nat_cast : ℕ → α
• nat_cast_zero : linear_ordered_semifield.nat_cast 0 = 0 . "control_laws_tac"
• nat_cast_succ : (∀ (n : ℕ), linear_ordered_semifield.nat_cast (n + 1) = linear_ordered_semifield.nat_cast n + 1) . "control_laws_tac"
• npow : ℕ → α → α
• npow_zero' : (∀ (x : α), linear_ordered_semifield.npow 0 x = 1) . "try_refl_tac"
• npow_succ' : (∀ (n : ℕ) (x : α), linear_ordered_semifield.npow n.succ x = x * linear_ordered_semifield.npow n x) . "try_refl_tac"
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• 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 : α), c + a ≤ c + b
• le_of_add_le_add_left : ∀ (a b c : α), a + b ≤ a + c → b ≤ c
• exists_pair_ne : ∃ (x y : α), x ≠ y
• zero_le_one : 0 ≤ 1
• mul_lt_mul_of_pos_left : ∀ (a b c : α), a < b → 0 < c → c * a < c * b
• mul_lt_mul_of_pos_right : ∀ (a b c : α), a < b → 0 < c → a * c < b * c
• mul_comm : ∀ (a b : α), a * b = b * a
• 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
• max : α → α → α
• max_def : linear_ordered_semifield.max = max_default . "reflexivity"
• min : α → α → α
• min_def : linear_ordered_semifield.min = min_default . "reflexivity"
• inv : α → α
• div : α → α → α
• div_eq_mul_inv : (∀ (a b : α), a / b = a * b⁻¹) . "try_refl_tac"
• zpow : ℤ → α → α
• zpow_zero' : (∀ (a : α), linear_ordered_semifield.zpow 0 a = 1) . "try_refl_tac"
• zpow_succ' : (∀ (n : ℕ) (a : α), linear_ordered_semifield.zpow (int.of_nat n.succ) a = a * linear_ordered_semifield.zpow (int.of_nat n) a) . "try_refl_tac"
• zpow_neg' : (∀ (n : ℕ) (a : α), linear_ordered_semifield.zpow -[1+ n] a = (linear_ordered_semifield.zpow ↑(n.succ) a)⁻¹) . "try_refl_tac"
• inv_zero : 0⁻¹ = 0
• mul_inv_cancel : ∀ (a : α), a ≠ 0 → a * a⁻¹ = 1

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

Instances of this typeclass

• linear_ordered_field.to_linear_ordered_semifield
• canonically_linear_ordered_semifield.to_linear_ordered_semifield
• nonneg.linear_ordered_semifield

Instances of other typeclasses for linear_ordered_semifield

• linear_ordered_semifield.has_sizeof_inst

• add : α → α → α
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• 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"
• zsmul : ℤ → α → α
• zsmul_zero' : (∀ (a : α), linear_ordered_field.zsmul 0 a = 0) . "try_refl_tac"
• zsmul_succ' : (∀ (n : ℕ) (a : α), linear_ordered_field.zsmul (int.of_nat n.succ) a = a + linear_ordered_field.zsmul (int.of_nat n) a) . "try_refl_tac"
• zsmul_neg' : (∀ (n : ℕ) (a : α), linear_ordered_field.zsmul -[1+ n] a = -linear_ordered_field.zsmul ↑(n.succ) a) . "try_refl_tac"
• add_left_neg : ∀ (a : α), -a + a = 0
• add_comm : ∀ (a b : α), a + b = b + a
• int_cast : ℤ → α
• nat_cast : ℕ → α
• one : α
• nat_cast_zero : linear_ordered_field.nat_cast 0 = 0 . "control_laws_tac"
• nat_cast_succ : (∀ (n : ℕ), linear_ordered_field.nat_cast (n + 1) = linear_ordered_field.nat_cast n + 1) . "control_laws_tac"
• int_cast_of_nat : (∀ (n : ℕ), linear_ordered_field.int_cast ↑n = ↑n) . "control_laws_tac"
• int_cast_neg_succ_of_nat : (∀ (n : ℕ), linear_ordered_field.int_cast (-↑(n + 1)) = -↑(n + 1)) . "control_laws_tac"
• mul : α → α → α
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• 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 : α), a * (b + c) = a * b + a * c
• right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• 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 : α), c + a ≤ c + b
• exists_pair_ne : ∃ (x y : α), x ≠ y
• 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
• max : α → α → α
• max_def : linear_ordered_field.max = max_default . "reflexivity"
• min : α → α → α
• min_def : linear_ordered_field.min = min_default . "reflexivity"
• mul_comm : ∀ (a b : α), a * b = b * a
• inv : α → α
• div : α → α → α
• div_eq_mul_inv : (∀ (a b : α), a / b = a * b⁻¹) . "try_refl_tac"
• zpow : ℤ → α → α
• zpow_zero' : (∀ (a : α), linear_ordered_field.zpow 0 a = 1) . "try_refl_tac"
• zpow_succ' : (∀ (n : ℕ) (a : α), linear_ordered_field.zpow (int.of_nat n.succ) a = a * linear_ordered_field.zpow (int.of_nat n) a) . "try_refl_tac"
• zpow_neg' : (∀ (n : ℕ) (a : α), linear_ordered_field.zpow -[1+ n] a = (linear_ordered_field.zpow ↑(n.succ) a)⁻¹) . "try_refl_tac"
• rat_cast : ℚ → α
• mul_inv_cancel : ∀ {a : α}, a ≠ 0 → a * a⁻¹ = 1
• inv_zero : 0⁻¹ = 0
• rat_cast_mk : (∀ (a : ℤ) (b : ℕ) (h1 : 0 < b) (h2 : a.nat_abs.coprime b), linear_ordered_field.rat_cast {num := a, denom := b, pos := h1, cop := h2} = ↑a * (↑b)⁻¹) . "try_refl_tac"
• qsmul : ℚ → α → α
• qsmul_eq_mul' : (∀ (a : ℚ) (x : α), linear_ordered_field.qsmul a x = linear_ordered_field.rat_cast a * x) . "try_refl_tac"

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

Instances of this typeclass

• subfield_class.to_linear_ordered_field
• normed_linear_ordered_field.to_linear_ordered_field
• conditionally_complete_linear_ordered_field.to_linear_ordered_field
• rat.linear_ordered_field
• subfield.to_linear_ordered_field
• real.linear_ordered_field
• filter.germ.linear_ordered_field
• hyperreal.linear_ordered_field
• counterexample.sorgenfrey_line.linear_ordered_field

Instances of other typeclasses for linear_ordered_field

• linear_ordered_field.has_sizeof_inst