Canonically ordered semifields

@[deprecated "Use `[LinearOrderedSemifield α] [CanonicallyOrderedAdd α]` instead." (since := "2025-01-13")]

structure CanonicallyLinearOrderedSemifield (α : Type u_1) extends CanonicallyOrderedCommSemiring α, LinearOrderedSemifield α : Type u_1

A canonically linear ordered field is a linear ordered field in which a ≤ b iff there exists c with b = a + c.

• 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 : α) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : α) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : α) : a + b = b + a
• 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
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• add_le_add_left (a b : α) : a ≤ b → ∀ (c : α), c + a ≤ c + b
• bot : α
• bot_le (a : α) : ⊥ ≤ a
• exists_add_of_le {a b : α} : a ≤ b → ∃ (c : α), b = a + c
• le_self_add (a b : α) : a ≤ a + b
• 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
• natCast : ℕ → α
• natCast_zero : NatCast.natCast 0 = 0
• natCast_succ (n : ℕ) : NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → α → α
• npow_zero (x : α) : self.npow 0 x = 1
• npow_succ (n : ℕ) (x : α) : self.npow (n + 1) x = self.npow n x * x
• mul_comm (a b : α) : a * b = b * a
• eq_zero_or_eq_zero_of_mul_eq_zero {a b : α} : a * b = 0 → a = 0 ∨ b = 0
• 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
• min : α → α → α
• max : α → α → α
• compare : α → α → Ordering
• le_total (a b : α) : a ≤ b ∨ b ≤ a
• decidableLE : DecidableRel fun (x1 x2 : α) => x1 ≤ x2
• decidableEq : DecidableEq α
• decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2
• min_def (a b : α) : a ⊓ b = if a ≤ b then a else b
• max_def (a b : α) : a ⊔ b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq (a b : α) : compare a b = compareOfLessAndEq a b
• inv : α → α
• div : α → α → α
• div_eq_mul_inv (a b : α) : a / b = a * b⁻¹
• zpow : ℤ → α → α
• zpow_zero' (a : α) : self.zpow 0 a = 1
• zpow_succ' (n : ℕ) (a : α) : self.zpow (↑n.succ) a = self.zpow (↑n) a * a
• zpow_neg' (n : ℕ) (a : α) : self.zpow (Int.negSucc n) a = (self.zpow (↑n.succ) a)⁻¹
• inv_zero : 0⁻¹ = 0
• mul_inv_cancel (a : α) : a ≠ 0 → a * a⁻¹ = 1
• nnratCast : ℚ≥0 → α
• nnratCast_def (q : ℚ≥0) : ↑q = ↑q.num / ↑q.den
• nnqsmul : ℚ≥0 → α → α
• nnqsmul_def (q : ℚ≥0) (a : α) : self.nnqsmul q a = ↑q * a

@[reducible, inline]

abbrev LinearOrderedSemifield.toLinearOrderedCommGroupWithZero {α : Type u_1} [LinearOrderedSemifield α] [CanonicallyOrderedAdd α] : LinearOrderedCommGroupWithZero α

Construct a LinearOrderedCommGroupWithZero from a canonically ordered LinearOrderedSemifield.

Equations

• LinearOrderedSemifield.toLinearOrderedCommGroupWithZero = LinearOrderedCommGroupWithZero.mk ⋯ LinearOrderedSemifield.zpow ⋯ ⋯ ⋯ ⋯ ⋯

theorem tsub_div {α : Type u_1} [LinearOrderedSemifield α] [CanonicallyOrderedAdd α] [Sub α] [OrderedSub α] (a b c : α) : (a - b) / c = a / c - b / c