Module docstring
{"# Canonically ordered semifields "}
CanonicallyLinearOrderedSemifield
structure
(α : Type*) extends CanonicallyOrderedCommSemiring α,
LinearOrderedSemifield α
Full source
/-- A canonically linear ordered field is a linear ordered field in which `a ≤ b` iff there exists
`c` with `b = a + c`. -/
@[deprecated "Use `[LinearOrderedSemifield α] [CanonicallyOrderedAdd α]` instead."
(since := "2025-01-13")]
structure CanonicallyLinearOrderedSemifield (α : Type*) extends CanonicallyOrderedCommSemiring α,
LinearOrderedSemifield αInformal description
A canonically linear ordered semifield is a structure that combines the properties of a canonically ordered commutative semiring and a linear ordered semifield. Specifically, it is a linear ordered field where the order relation `a ≤ b` is equivalent to the existence of an element `c` such that `b = a + c`.
CanonicallyOrderedAdd.toLinearOrderedCommGroupWithZero
abbrev
: LinearOrderedCommGroupWithZero α
Full source
/-- Construct a `LinearOrderedCommGroupWithZero` from a canonically linear ordered semifield. -/
abbrev CanonicallyOrderedAdd.toLinearOrderedCommGroupWithZero :
LinearOrderedCommGroupWithZero α where
__ := ‹Semifield α›
__ := ‹LinearOrder α›
bot := 0
bot_le := zero_le
zero_le_one := zero_le_one
mul_le_mul_left := fun _ _ h _ ↦ mul_le_mul_of_nonneg_left h <| zero_le _Informal description
Given a canonically linear ordered semifield $\alpha$, there exists a corresponding structure of a linear ordered commutative group with zero on $\alpha$.
tsub_div
theorem
(a b c : α) : (a - b) / c = a / c - b / c
Full source
theorem tsub_div (a b c : α) : (a - b) / c = a / c - b / c := by simp_rw [div_eq_mul_inv, tsub_mul]Informal description
For any elements $a$, $b$, and $c$ in a canonically ordered semifield $\alpha$, the equality $(a - b) / c = a / c - b / c$ holds.