mul_self_inj_of_nonneg
theorem mul_self_inj_of_nonneg :
∀ {α : Type u_2} [inst : LinearOrderedField α] {a b : α}, 0 ≤ a → 0 ≤ b → (a * a = b * b ↔ a = b)
This theorem, `mul_self_inj_of_nonneg`, states that for any type `α` that has a structure of `LinearOrderedField` (a field in which strict total ordering is defined), given two non-negative (greater than or equal to zero) elements `a` and `b` of `α`, the equality of the squares of `a` and `b` implies the equality of `a` and `b` themselves. That is, if `a * a = b * b` and `a` and `b` are both non-negative, then `a = b`. The reverse is also true: if `a = b`, then `a * a = b * b`. This theorem essentially states that the square function is injective for non-negative numbers.
More concisely: For any non-negative elements `a` and `b` in a LinearOrderedField, if `a * a = b * b`, then `a = b`.
|
div_two_lt_of_pos
theorem div_two_lt_of_pos : ∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a : α}, 0 < a → a / 2 < a
The theorem `div_two_lt_of_pos` is an alias for the reverse direction of the `half_lt_self_iff` theorem in the Lean 4 theorem prover. It states that for any type `α` that forms a linear ordered semifield and for any element `a` of this type, if `a` is greater than zero, then `a` divided by two is less than `a`. In terms of mathematics, if `a` is a positive number, the result of dividing `a` by 2 is always less than `a`.
More concisely: For any positive element `a` in a linear ordered semifield, `a / 2` is strictly less than `a`.
|
le_inv
theorem le_inv : ∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b : α}, 0 < a → 0 < b → (a ≤ b⁻¹ ↔ b ≤ a⁻¹) := by
sorry
This theorem, `le_inv`, states that for any linear ordered semifield `α` and any two elements `a` and `b` of `α` that are greater than 0, `a` is less than or equal to the inverse of `b` if and only if `b` is less than or equal to the inverse of `a`. This is a property intrinsic to the structure of linear ordered semifields.
More concisely: For any linear ordered semifield `α`, and elements `a, b` in `α` with `0 < a, b`, we have `a ≤ b^⁻¹` if and only if `b ≤ a^⁻¹`.
|
div_lt_iff
theorem div_lt_iff : ∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b c : α}, 0 < c → (b / c < a ↔ b < a * c)
This theorem, `div_lt_iff`, applies to any type `α` that is a "linear ordered semifield", i.e., a field defined on a totally ordered set. The theorem states that for any three elements `a`, `b`, and `c` of this field where `c` is greater than zero, the inequality `b / c < a` is equivalent to `b < a * c`. In other words, dividing `b` by `c` and comparing the result to `a` is the same as comparing `b` to the product of `a` and `c`.
More concisely: For any linear ordered semifield type `α` and elements `a`, `b`, and `c` of `α` where `c` is positive, `b / c < a` if and only if `b < a * c`.
|
sub_one_div_inv_le_two
theorem sub_one_div_inv_le_two : ∀ {α : Type u_2} [inst : LinearOrderedField α] {a : α}, 2 ≤ a → (1 - 1 / a)⁻¹ ≤ 2 := by
sorry
This theorem, `sub_one_div_inv_le_two`, states that for any type `α` which is a linear ordered field, and for any element `a` of this type, if `a` is greater than or equal to 2, then the inverse of (1 - 1/a) is less than or equal to 2. In other words, if `a` is a number in any ordered field and is at least 2, then 1 / (1 - 1/a) ≤ 2.
More concisely: For any linear ordered field `α` and element `a` in `α` greater than or equal to 2, 1 / (1 - 1/`a`) ≤ 2.
|
div_le_one
theorem div_le_one : ∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b : α}, 0 < b → (a / b ≤ 1 ↔ a ≤ b) := by
sorry
This theorem, `div_le_one`, states that for any type `α` that is a Linear Ordered Semifield, and for any two elements `a` and `b` of that type, if `b` is greater than 0, then the condition of `a` divided by `b` being less than or equal to 1 is equivalent to `a` being less than or equal to `b`. In mathematical notation, this can be written as: if $0 < b$, then $\frac{a}{b} \leq 1$ if and only if $a \leq b$.
More concisely: For any Linear Ordered Semifield type `α` and elements `a`, `b` of type `α` with `0 < b`, the condition `a / b <= 1` is equivalent to `a <= b`.
|
sub_self_div_two
theorem sub_self_div_two : ∀ {α : Type u_2} [inst : LinearOrderedField α] (a : α), a - a / 2 = a / 2
This theorem states that for any linear ordered field (which is a field with an order relation that is compatible with the field operations), the result of subtracting half of a certain element 'a' from itself is equal to half of that element 'a'. In mathematical terms, we can express this as: for all 'a' in a linear ordered field 'α', 'a - a/2 = a/2'.
More concisely: In a linear ordered field, subtracting half an element from it is equal to half that element: i.e., for all 'a' in the field, 'a - a/2 = a/2'.
|
add_halves
theorem add_halves : ∀ {α : Type u_2} [inst : LinearOrderedSemifield α] (a : α), a / 2 + a / 2 = a
This theorem, named "add_halves", states that for any type `α` which is a Linear Ordered Semifield (a structure which is both a linearly ordered ring and a commutative division algebra), the sum of half of a given element `a` and half of the same element `a` is equal to `a` itself. Formally, for all `a` in `α`, `a / 2 + a / 2 = a`. This is essentially a formal statement of the intuitive mathematical fact that halving a number and then adding the two halves gives you the original number.
More concisely: For all elements `a` in a Linear Ordered Semifield `α`, `a / 2 + a / 2 = a`.
|
div_le_self
theorem div_le_self : ∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b : α}, 0 ≤ a → 1 ≤ b → a / b ≤ a := by
sorry
This theorem, `div_le_self`, states that for any type `α` that is a linearly ordered semifield, and any elements `a` and `b` of that type, if `a` is greater than or equal to 0 and `b` is greater than or equal to 1, then the value of `a` divided by `b` is less than or equal to `a`. In other words, in a ordered field, dividing a non-negative number by another number greater than or equal to one will never result in a larger number than the original one.
More concisely: For any linearly ordered semifield type `α` and elements `a` and `b` of type `α` with `a ≥ 0` and `b ≥ 1`, `a / b ≤ a`.
|
div_le_div_of_le
theorem div_le_div_of_le :
∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b c : α}, 0 ≤ c → a ≤ b → a / c ≤ b / c
This theorem states that for any type `α` that is a linear ordered semifield, given any three elements `a`, `b`, and `c` of `α` such that `c` is non-negative and `a` is less than or equal to `b`, the value of `a` divided by `c` is less than or equal to `b` divided by `c`.
More concisely: For all linear ordered semifields α and elements a, b, and c in α with c > 0 and a <= b, we have a / c <= b / c.
|
div_lt_iff'
theorem div_lt_iff' : ∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b c : α}, 0 < c → (b / c < a ↔ b < c * a)
This theorem, `div_lt_iff'`, states that for any type `α` that is a LinearOrderedSemifield, and any elements `a`, `b`, `c` of type `α`, if `c` is greater than zero, then `b` divided by `c` is less than `a` if and only if `b` is less than `c` times `a`. In other words, it establishes a particular equivalence relation between division and multiplication in a ordered semifield when the divisor/multiplier is greater than zero.
More concisely: For any LinearOrderedSemifield type `α` and elements `a`, `b`, `c` of type `α` with `c` being positive, `b / c < a` if and only if `b` is less than `a * c`.
|
div_lt_div_left
theorem div_lt_div_left :
∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b c : α}, 0 < a → 0 < b → 0 < c → (a / b < a / c ↔ c < b)
The theorem `div_lt_div_left` states that for any linear ordered semifield `α` and any three elements `a`, `b`, `c` of that field, if `a`, `b`, and `c` are all greater than zero, then the inequality `a / b < a / c` holds if and only if `c < b`. In other words, for positive numbers `a`, `b`, and `c`, `a` divided by `b` is less than `a` divided by `c` precisely when `c` is less than `b`.
More concisely: Given a linear ordered semifield `α` and positive elements `a`, `b`, `c` in `α`, the inequality `a / b < a / c` holds if and only if `c < b`.
|
inv_le_inv_of_neg
theorem inv_le_inv_of_neg :
∀ {α : Type u_2} [inst : LinearOrderedField α] {a b : α}, a < 0 → b < 0 → (a⁻¹ ≤ b⁻¹ ↔ b ≤ a)
This theorem states that for any linear ordered field `α` and any two elements `a` and `b` of `α`, if both `a` and `b` are less than zero, then the reciprocal of `a` is less than or equal to the reciprocal of `b` if and only if `b` is less than or equal to `a`. In mathematical notation, this can be written as: if $a < 0$ and $b < 0$, then $\frac{1}{a} \leq \frac{1}{b}$ if and only if $b \leq a$.
More concisely: For any linear ordered field `α` and elements `a, b ∈ α` with `a, b < 0`, $\frac{1}{a} \leq \frac{1}{b}$ if and only if `b ≤ a`.
|
inv_lt_one
theorem inv_lt_one : ∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a : α}, 1 < a → a⁻¹ < 1
This theorem, `inv_lt_one`, states that for any instance of a linearly ordered semifield `α` and any element `a` of `α`, if `1` is less than `a`, then the inverse of `a` (`a⁻¹`) is less than `1`. Essentially, for any number greater than one in a certain ordered field, its reciprocal will be less than one.
More concisely: For any linearly ordered semifield `α` and `a` in `α` with `1 < a`, it holds that `1 < a⁻¹`.
|
one_le_inv
theorem one_le_inv : ∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a : α}, 0 < a → a ≤ 1 → 1 ≤ a⁻¹
This theorem states that for any type `α` that forms a linearly ordered semifield, given any element `a` of `α`, if `a` is greater than `0` and less than or equal to `1`, then the inverse of `a` (denoted as `a⁻¹`) is greater than or equal to `1`. Essentially, it is capturing the intuitive idea in fractional numbers where if a fraction is less than one, its reciprocal is greater than one.
More concisely: For any linearly ordered semifield type `α` and element `a` in `α` with `0 < a <= 1`, the inverse `a⁻¹` satisfies `1 <= a⁻¹`.
|
div_lt_div_of_lt
theorem div_lt_div_of_lt :
∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b c : α}, a < b → 0 < c → a / c < b / c
This theorem, `div_lt_div_of_lt`, states that for any linear ordered semifield `α` and any three elements `a`, `b`, and `c` of `α`, if `a` is less than `b` and `c` is greater than `0`, then `a` divided by `c` is less than `b` divided by `c`. This is essentially an alias for the theorem `div_lt_div_of_pos_right`.
More concisely: If `α` is a linear ordered semifield, `a`, `b` are elements of `α`, and `0 < c`, then `a / c < b / c`.
|
one_div_le_one_div_of_neg
theorem one_div_le_one_div_of_neg :
∀ {α : Type u_2} [inst : LinearOrderedField α] {a b : α}, a < 0 → b < 0 → (1 / a ≤ 1 / b ↔ b ≤ a)
This theorem, `one_div_le_one_div_of_neg`, states that for any type `α` which is a `LinearOrderedField`, given any two elements `a` and `b` from `α`, if both `a` and `b` are negative, then the fraction `1 / a` is less than or equal to `1 / b` if and only if `b` is less than or equal to `a`.
More concisely: For all `LinearOrderedField` types `α` and elements `a` and `b` in `α`, if `a` and `b` are negative then `1 / a ≤ 1 / b` if and only if `a ≤ b`.
|
inv_mul_lt_iff
theorem inv_mul_lt_iff :
∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b c : α}, 0 < b → (b⁻¹ * a < c ↔ a < b * c)
This theorem, `inv_mul_lt_iff`, states that for any type `α` that forms a linear ordered semiring, given any three elements `a`, `b`, and `c` of this type with `b` being positive, the statement "the inverse of `b` multiplied by `a` is less than `c`" is equivalent to the statement "`a` is less than `b` multiplied by `c`".
More concisely: For any linear ordered semiring type `α` and positive elements `a`, `b`, and `c` of `α`, `a < b * c` if and only if `b⁻¹ * a < c`.
|
div_le_div_of_le_left
theorem div_le_div_of_le_left :
∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b c : α}, 0 ≤ a → 0 < c → c ≤ b → a / b ≤ a / c
This theorem, `div_le_div_of_le_left`, states that for any type `α` that forms a linearly ordered semifield (a field that has a total order that is compatible with the field operations), and for any three elements `a`, `b`, and `c` of type `α`, if `a` is greater than or equal to 0, `c` is strictly greater than 0, and `c` is less than or equal to `b`, then the quotient of `a` divided by `b` is less than or equal to the quotient of `a` divided by `c`. This theorem is an alias of `div_le_div_of_nonneg_left`.
More concisely: If `α` is a linearly ordered semifield, `a ≥ 0`, `c > 0`, and `c ≤ b`, then `a / b ≤ a / c`.
|
add_self_div_two
theorem add_self_div_two : ∀ {α : Type u_2} [inst : LinearOrderedSemifield α] (a : α), (a + a) / 2 = a
This theorem states that for any type `α` which is a linearly ordered semifield, dividing the sum of any element `a` from this type and itself by 2 results in the original element `a`. In mathematical terms, it expresses that $(a + a) / 2 = a$ for any element `a` in a linearly ordered semifield.
More concisely: In a linearly ordered semifield, element-wise addition and division by 2 commute, i.e., `(a + a) / 2 = a` for all `a` in the semifield.
|
div_le_div_iff
theorem div_le_div_iff :
∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b c d : α}, 0 < b → 0 < d → (a / b ≤ c / d ↔ a * d ≤ c * b)
This theorem states that for any type `α` that is a linear ordered semifield, given any four elements `a`, `b`, `c`, `d` of `α` and the condition that `b` and `d` are both greater than zero, the inequality `a / b ≤ c / d` is equivalent to `a * d ≤ c * b`. In plain terms, it shows the relationship between division and multiplication in inequalities, essentially stating that dividing `a` by `b` is less than or equal to dividing `c` by `d` if and only if `a` times `d` is less than or equal to `c` times `b`, given that `b` and `d` are both positive.
More concisely: For any linear ordered semifield type `α` and positive elements `a`, `b`, `c`, `d` in `α`, the inequality `a / b <= c / d` is equivalent to `a * d <= c * b`.
|
abs_div
theorem abs_div : ∀ {α : Type u_2} [inst : LinearOrderedField α] (a b : α), |a / b| = |a| / |b|
This theorem states that for any real numbers `a` and `b` of an arbitrary type `α`, which is a LinearOrderedField (a field that is both ordered and linear), the absolute value of the quotient `a / b` is equal to the quotient of the absolute values `|a| / |b|`. In other words, the absolute value operation can be distributed over the division operation.
More concisely: For any real numbers `a` and `b` in a LinearOrderedField `α`, |a / b| = |a| / |b|.
|
one_lt_div
theorem one_lt_div : ∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b : α}, 0 < b → (1 < a / b ↔ b < a) := by
sorry
The theorem `one_lt_div` states that for any type `α` that has a structure of a linear ordered semiring (a mathematical structure that is both a semiring and a linear ordered set), given two elements `a` and `b` of type `α`, if `b` is greater than `0`, then `1` is less than the fraction `a / b` if and only if `b` is less than `a`. In other words, it establishes a relationship between the comparability of `1` and a fraction `a / b`, and the comparability of `b` and `a`, given that `b` is positive.
More concisely: For any linear ordered semiring type `α` and elements `a`, `b` of type `α` with `b` positive, `1` is less than `a / b` if and only if `b` is less than `a`.
|
half_le_self
theorem half_le_self : ∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a : α}, 0 ≤ a → a / 2 ≤ a
This theorem, `half_le_self`, states that for any type `α` that is a `LinearOrderedSemifield` (a structure that combines the properties of an ordered ring and a field), for any non-negative element `a` of this type, half of `a` is always less than or equal to `a`. This theorem essentially captures the intuitive mathematical idea that half of a non-negative number is always less than or equal to the number itself.
More concisely: For any non-negative element `a` in a LinearOrderedSemifield, `0 < a => 0.5 * a <= a`.
|
inv_mul_le_iff
theorem inv_mul_le_iff :
∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b c : α}, 0 < b → (b⁻¹ * a ≤ c ↔ a ≤ b * c)
This theorem states that for any type `α` that is a linear ordered semifield, and for any three elements `a`, `b`, and `c` of this type where `b` is positive, the statement "the product of the inverse of `b` and `a` is less than or equal to `c`" is equivalent to the statement " `a` is less than or equal to the product of `b` and `c`". This theorem is a useful property of inequalities in fields.
More concisely: For any linear ordered semifield type `α` and elements `a`, `b` (with `b` positive), `a ≤ b × c` if and only if `b⁻¹ × a ≤ c`.
|
one_lt_inv
theorem one_lt_inv : ∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a : α}, 0 < a → a < 1 → 1 < a⁻¹
This theorem, `one_lt_inv`, states that for any type `α` which is an instance of a `LinearOrderedSemifield` -- a field of numbers where linear ordering is defined -- if a particular variable `a` of the given type `α` is positive (greater than 0) and also less than 1, then the reciprocal of `a` (denoted by `a⁻¹` in Lean 4) is greater than 1.
More concisely: If `α` is a LinearOrderedSemifield type and `0 < a < 1` in `α`, then `1 < a⁻¹`.
|
div_le_one_of_le
theorem div_le_one_of_le : ∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b : α}, a ≤ b → 0 ≤ b → a / b ≤ 1 := by
sorry
This theorem, `div_le_one_of_le`, states that for any type `α` that forms a linear ordered semifield, given any two elements `a` and `b` of this type, if `a` is less than or equal to `b` and `b` is greater than or equal to zero, then the quotient of `a` divided by `b` is less than or equal to one. In mathematical notation, this would be expressed as: if `a ≤ b` and `0 ≤ b`, then `a / b ≤ 1`.
More concisely: If `α` is a linear ordered semifield and `a` is less than or equal to `b` in `α` with `b` being greater than or equal to zero, then `a / b ≤ 1`.
|
one_div_lt_one_div
theorem one_div_lt_one_div :
∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b : α}, 0 < a → 0 < b → (1 / a < 1 / b ↔ b < a)
This theorem states that for any type `α` that is a linearly ordered semiring (a mathematical structure having operations of addition and multiplication with ordering properties), given two positive values `a` and `b` of type `α`, the statement "1 divided by `a` is less than 1 divided by `b`" is equivalent to the statement "`b` is less than `a`". This theorem is useful when working with reciprocals in the context of ordered fields.
More concisely: For any linearly ordered semiring type `α` and positive elements `a` and `b` of `α`, `1 / a < 1 / b` if and only if `a` is less than `b`.
|
lt_div_iff'
theorem lt_div_iff' : ∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b c : α}, 0 < c → (a < b / c ↔ c * a < b)
This theorem, `lt_div_iff'`, states that for any type `α` that is a linearly ordered semifield, and for any three elements `a`, `b`, and `c` of type `α`, if `c` is greater than zero, then `a` is less than `b` divided by `c` if and only if `c` multiplied by `a` is less than `b`. In other words, it establishes an equivalence between the comparison of `a` with the quotient `b/c` and the comparison of the product `c*a` with `b`, given the condition that `c` is positive.
More concisely: For any linearly ordered semifield type `α` and elements `a`, `b`, and `c` with `c > 0`, `a < b / c` if and only if `c * a < b`.
|
one_div_lt_one_div_of_neg
theorem one_div_lt_one_div_of_neg :
∀ {α : Type u_2} [inst : LinearOrderedField α] {a b : α}, a < 0 → b < 0 → (1 / a < 1 / b ↔ b < a)
This theorem, `one_div_lt_one_div_of_neg`, states that for any type `α` which is a linear ordered field, if we have two elements `a` and `b` of `α` that are both less than zero, then the statement "1/a is less than 1/b" is equivalent to the statement "b is less than a". In other words, in a linear ordered field, the relationship of negative numbers `a` and `b` is reversed when comparing their reciprocals.
More concisely: In a linear ordered field, for all `a` and `b` of type `α` with `a` and `b` being negative, we have `1/a < 1/b` if and only if `b < a`.
|
lt_inv
theorem lt_inv : ∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b : α}, 0 < a → 0 < b → (a < b⁻¹ ↔ b < a⁻¹) := by
sorry
This theorem `lt_inv` states that for any type `α` that has a structure of a `LinearOrderedSemifield` (a field with a linear order), and for any two elements `a` and `b` of this type that are greater than 0, `a` is less than the inverse of `b` if and only if `b` is less than the inverse of `a`. This theorem basically establishes a relationship between the ordering of two positive elements and the ordering of their inverses in a linearly ordered semifield.
More concisely: In a LinearOrderedSemifield type, for positive elements `a` and `b`, `a < (−1 : α) <=> b < (−1 : α)`.
|
lt_div_iff_of_neg
theorem lt_div_iff_of_neg :
∀ {α : Type u_2} [inst : LinearOrderedField α] {a b c : α}, c < 0 → (a < b / c ↔ b < a * c)
This theorem states that for any linearly ordered field `α` and any elements `a`, `b`, and `c` of `α`, if `c` is less than zero, then `a` is less than `b` divided by `c` if and only if `b` is less than `a` multiplied by `c`. This theorem basically provides a condition for when the inequality between `a` and `b/c` is equivalent to the inequality between `b` and `ac`, given that `c` is negative in the field.
More concisely: For any linearly ordered field `α` and elements `a`, `b`, and `c` in `α` with `c` negative, `a < b / c` if and only if `b < a * c`.
|
div_lt_div_right
theorem div_lt_div_right :
∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b c : α}, 0 < c → (a / c < b / c ↔ a < b)
This theorem, `div_lt_div_right`, states that for any type `α` that is a linear ordered semifield, and for any three elements `a`, `b`, and `c` of this type, if `c` is greater than zero, then `a` divided by `c` is less than `b` divided by `c` if and only if `a` is less than `b`. This is essentially saying that dividing both sides of an inequality by a positive number doesn't change the direction of the inequality.
More concisely: For any linear ordered semifield type `α` and elements `a`, `b`, and `c` with `c > 0`, `a / c < b / c` if and only if `a < b`.
|
inv_le_inv_of_le
theorem inv_le_inv_of_le : ∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b : α}, 0 < a → a ≤ b → b⁻¹ ≤ a⁻¹ := by
sorry
This theorem states that in a linear ordered semifield, given two elements `a` and `b`, if `a` is positive and `a` is less than or equal to `b`, then inverse of `b` is less than or equal to the inverse of `a`. In other words, it is a statement about the "reversal" of order when taking inverses in such a structure. The order of elements is inverted when taking the inverse in positive realm of a linear ordered semifield.
More concisely: In a linear ordered semifield, if `a` is positive and `a` < `b`, then `b^(-1)` < `a^(-1)`.
|
div_le_div
theorem div_le_div :
∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b c d : α}, 0 ≤ c → a ≤ c → 0 < d → d ≤ b → a / b ≤ c / d
This theorem states that for any linear ordered semifield `α`, given four elements `a`, `b`, `c`, `d` in `α`, if `c` is non-negative, `a` is less than or equal to `c`, `d` is positive, and `d` is less than or equal to `b`, then the ratio `a/b` is less than or equal to the ratio `c/d`. This theorem is a fundamental result about the properties of division in a linear ordered semifield.
More concisely: In a linear ordered semifield, if $a \leq c$ are elements, $c \geq 0$, and $d > 0$ with $d \leq b$, then $\frac{a}{b} \leq \frac{c}{d}$.
|
div_lt_iff_of_neg
theorem div_lt_iff_of_neg :
∀ {α : Type u_2} [inst : LinearOrderedField α] {a b c : α}, c < 0 → (b / c < a ↔ a * c < b)
This theorem states that for any type `α` that is a linearly ordered field, and for any three elements `a`, `b`, and `c` of this type, if `c` is less than zero, then `b` divided by `c` is less than `a` if and only if `a` multiplied by `c` is less than `b`. This is a statement about the properties of division and multiplication in ordered fields where one of the elements is negative.
More concisely: For any linearly ordered field `α` and elements `a, b, c` of `α` with `c < 0`, we have `b/c < a` if and only if `ac < b`.
|
mul_sub_mul_div_mul_neg
theorem mul_sub_mul_div_mul_neg :
∀ {α : Type u_2} [inst : LinearOrderedField α] {a b c d : α},
c ≠ 0 → d ≠ 0 → a / c < b / d → (a * d - b * c) / (c * d) < 0
This theorem, `mul_sub_mul_div_mul_neg`, states that for any linearly ordered field `α`, and any four elements `a`, `b`, `c`, and `d` of this field such that `c` and `d` are non-zero, if the ratio of `a` to `c` is less than the ratio of `b` to `d`, then the value of `(a * d - b * c) / (c * d)` is less than zero. This theorem is an alias of the reverse direction of `mul_sub_mul_div_mul_neg_iff`.
More concisely: If `α` is a linearly ordered field, `c` and `d` are non-zero elements of `α`, and `a/c < b/d`, then `(a*d - b*c) / (c*d)` is negative.
|
le_div_iff'
theorem le_div_iff' : ∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b c : α}, 0 < c → (a ≤ b / c ↔ c * a ≤ b)
This theorem states that for any type `α` that is a linear ordered semifield and any three elements `a`, `b`, and `c` of this type with `c` being positive, `a` is less than or equal to `b` divided by `c` if and only if `c` times `a` is less than or equal to `b`. Essentially, it is expressing a property of division in the context of ordered fields.
More concisely: For any linear ordered semifield type `α` and positive elements `a`, `b`, and `c` of `α`, `a ≤ b / c` if and only if `c * a ≤ b`.
|
Mathlib.Algebra.Order.Field.Basic._auxLemma.2
theorem Mathlib.Algebra.Order.Field.Basic._auxLemma.2 :
∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b : α), b⁻¹ * a = a / b
This theorem, `Mathlib.Algebra.Order.Field.Basic._auxLemma.2`, states that for any type `α` equipped with the structure of a Division Commutative Monoid (a structure that generalizes fields by allowing zero divisors), for any two elements `a` and `b` of this type, the product of the inverse of `b` and `a` is equal to the division of `a` by `b`. In mathematical terms, it asserts that for all `a, b` in `α`, `b⁻¹ * a = a / b`.
More concisely: For any divisive Monoid `α`, for all `a, b` in `α`, the product of `b`'s multiplicative inverse and `a` equals their quotient: `b⁻¹ * a = a / b`.
|
div_lt_div_of_mul_sub_mul_div_neg
theorem div_lt_div_of_mul_sub_mul_div_neg :
∀ {α : Type u_2} [inst : LinearOrderedField α] {a b c d : α},
c ≠ 0 → d ≠ 0 → (a * d - b * c) / (c * d) < 0 → a / c < b / d
This theorem, `div_lt_div_of_mul_sub_mul_div_neg`, is an alias of the forward direction of `mul_sub_mul_div_mul_neg_iff`. It's defined for any linearly ordered field `α`. It states that for any non-zero elements `c` and `d`, if the expression `(a * d - b * c) / (c * d)` is less than zero, then `a / c` is less than `b / d`. This theorem provides a condition under which the division of two elements of the field is less than the division of two other elements of the field.
More concisely: If `a * d - b * c` is less than zero and `c * d` is non-zero, then `a / c` is strictly less than `b / d` in a linearly ordered field.
|
lt_div_iff
theorem lt_div_iff : ∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b c : α}, 0 < c → (a < b / c ↔ a * c < b)
This theorem, `lt_div_iff`, states that for any type `α` that forms a `LinearOrderedSemifield`, given any three elements `a`, `b`, and `c` of this type where `c` is greater than zero, `a` is less than `b` divided by `c` if and only if `a` multiplied by `c` is less than `b`.
More concisely: For any `LinearOrderedSemifield` type `α` and elements `a`, `b`, and `c` (with `c > 0`), `a` is less than `b / c` if and only if `a * c` is less than `b`.
|
inv_le_inv
theorem inv_le_inv :
∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b : α}, 0 < a → 0 < b → (a⁻¹ ≤ b⁻¹ ↔ b ≤ a)
This theorem, `inv_le_inv`, states that for any linearly ordered semifield `α` and any two elements `a` and `b` of `α` that are greater than zero, the reciprocal of `a` is less than or equal to the reciprocal of `b` if and only if `b` is less than or equal to `a`. This theorem, thus, provides a way to compare the reciprocals of two positive elements from a linearly ordered semifield. The theorem `inv_le_inv_of_le` provides a similar comparison but requires one less assumption.
More concisely: For any linearly ordered semifield with positive elements `α`, `a` and `b` satisfying `a > 0` and `b > 0`, the condition `a >= b` is equivalent to `1/a <= 1/b`.
|
one_div_le_one_div_of_le
theorem one_div_le_one_div_of_le :
∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b : α}, 0 < a → a ≤ b → 1 / b ≤ 1 / a
This theorem states that for any type `α` that is a linear ordered semifield, given two elements `a` and `b` of this type, if `a` is greater than 0 and less than or equal to `b`, then the reciprocal of `b` is less than or equal to the reciprocal of `a`. In mathematical terms, it states: for all `a` and `b` in `α`, if `0 < a ≤ b`, then `1/b ≤ 1/a`.
More concisely: For any linear ordered semifield type `α`, if `0 < a <= b` in `α`, then `1/b <= 1/a`.
|
Mathlib.Algebra.Order.Field.Basic._auxLemma.7
theorem Mathlib.Algebra.Order.Field.Basic._auxLemma.7 :
∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a : α}, (a / 2 < a) = (0 < a)
This theorem, `Mathlib.Algebra.Order.Field.Basic._auxLemma.7`, states that for any type `α`, which is a linear ordered semifield, and for any element `a` of type `α`, the inequality `a / 2 < a` is equivalent to `0 < a`. In other words, it's saying that a number is greater than half of itself if and only if it is greater than zero.
More concisely: For any linear ordered semifield `α`, the inequality `a / 2 < a` holds if and only if `0 < a` for any `a` in `α`.
|
div_le_div_of_nonpos_of_le
theorem div_le_div_of_nonpos_of_le :
∀ {α : Type u_2} [inst : LinearOrderedField α] {a b c : α}, c ≤ 0 → b ≤ a → a / c ≤ b / c
This theorem states that for any linearly ordered field `α`, and for any elements `a`, `b`, and `c` of `α`, if `c` is less than or equal to zero, and `b` is less than or equal to `a`, then the division of `a` by `c` is less than or equal to the division of `b` by `c`. In mathematical terms, if `c ≤ 0` and `b ≤ a`, then `a / c ≤ b / c`.
More concisely: For any linearly ordered field `α` and elements `a`, `b`, `c` in `α` with `c ≤ 0` and `b ≤ a`, we have `a / c ≤ b / c`.
|
div_le_of_nonneg_of_le_mul
theorem div_le_of_nonneg_of_le_mul :
∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b c : α}, 0 ≤ b → 0 ≤ c → a ≤ c * b → a / b ≤ c
This theorem, `div_le_of_nonneg_of_le_mul`, states that for any type `α` that is a linear ordered semifield and given any three elements `a`, `b`, and `c` of this type, if both `b` and `c` are nonnegative (greater than or equal to zero) and if `a` is less than or equal to the product of `c` and `b`, then the division of `a` by `b` is less than or equal to `c`. In simple terms, if you divide `a` by `b` in a context where `b` and `c` are nonnegative and `a` is not more than `b` times `c`, you will get a result that is not more than `c`.
More concisely: If `α` is a linear ordered semifield, `a`, `b`, `c` ∈ `α` with `b`, `c` nonnegative, and `a` ≤ `c` × `b`, then `a / b` ≤ `c`.
|
abs_inv
theorem abs_inv : ∀ {α : Type u_2} [inst : LinearOrderedField α] (a : α), |a⁻¹| = |a|⁻¹
The theorem `abs_inv` states that for every type `α` that is a linear ordered field, the absolute value of the inverse of any element `a` from `α` is equal to the inverse of the absolute value of `a`. In mathematical notation, this is saying that for any real number `a`, |1/a| = 1/|a|.
More concisely: For any linear ordered field `α`, |a^(-1)| = |a|^(-1) for all `a` in `α`.
|
half_lt_self
theorem half_lt_self : ∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a : α}, 0 < a → a / 2 < a
This theorem, `half_lt_self`, states that for any type `α` that is a `LinearOrderedSemifield` (which means it possesses ordering and field-like properties, such as addition and multiplication), for any element `a` of this type, if `a` is greater than zero, then `a` divided by 2 is less than `a`. In other words, for any positive number, halving it will always result in a value less than the original.
More concisely: For any `LinearOrderedSemifield` type `α` and positive element `a`, we have `0 < a` implies `a / 2 < a`.
|
inv_lt
theorem inv_lt : ∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b : α}, 0 < a → 0 < b → (a⁻¹ < b ↔ b⁻¹ < a) := by
sorry
This theorem states that in any linearly ordered semifield, given two positive elements `a` and `b`, the reciprocal of `a` is less than `b` if and only if the reciprocal of `b` is less than `a`. This theorem also refers to `inv_lt_of_inv_lt`, which presents a similar but one-sided implication with one less assumption.
More concisely: In a linearly ordered semifield, the reciprocal of one positive element is less than another if and only if the reciprocal of the other is less than the first.
|
div_le_div_left
theorem div_le_div_left :
∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b c : α}, 0 < a → 0 < b → 0 < c → (a / b ≤ a / c ↔ c ≤ b)
This theorem states that for any type α which forms a linear ordered semifield, given three positive elements a, b, and c, the division of a by b is less than or equal to the division of a by c if and only if c is less than or equal to b. So it essentially encapsulates a property of division in the context of linear ordered semifields.
More concisely: In a linear ordered semifield, for positive elements a, b, and c, a/b <= a/c if and only if b >= c.
|
inv_le_one
theorem inv_le_one : ∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a : α}, 1 ≤ a → a⁻¹ ≤ 1
This theorem, named `inv_le_one`, states that for any type `α` which forms a Linear Ordered Semifield, if a given element `a` of this type `α` is greater than or equal to 1, then the multiplicative inverse of `a` (denoted by `a⁻¹`) is less than or equal to 1. This is a general property in the field of order theory and algebra, particularly applicable to number systems like the real or complex numbers.
More concisely: For any Linear Ordered Semifield type `α` and element `a` of `α` greater than or equal to 1, `a⁻¹ ≤ 1`.
|
one_div_le_one_div
theorem one_div_le_one_div :
∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b : α}, 0 < a → 0 < b → (1 / a ≤ 1 / b ↔ b ≤ a)
This theorem, `one_div_le_one_div`, states that for any type `α` that is a linearly ordered semifield, and for any values `a` and `b` of this type where both `a` and `b` are greater than zero, the statement "1 divided by `a` is less than or equal to 1 divided by `b`" is equivalent to the statement "`b` is less than or equal to `a`". In mathematical terms, given 0 < a and 0 < b, we have 1 / a ≤ 1 / b if and only if b ≤ a.
More concisely: For any linearly ordered semifield type `α` with elements `a` and `b` such that `0 < a` and `0 < b`, we have `1 / a <= 1 / b` if and only if `b <= a`.
|
one_half_pos
theorem one_half_pos : ∀ {α : Type u_2} [inst : LinearOrderedSemifield α], 0 < 1 / 2
This theorem states that for any semi-field that is linearly ordered, the value of one half (1/2) is always greater than zero. The semi-field is represented by any type `α`. A linearly ordered semi-field is a structure that combines properties of an ordered ring (like the integers with their usual ordering) and a field (like the rational numbers, real numbers, or complex numbers), but with the additional restriction that multiplication of non-zero elements never gives zero.
More concisely: In a linearly ordered semi-field, the multiplicative identity (1) has a positive square root, i.e., 1/2 > 0.
|
div_lt_one
theorem div_lt_one : ∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b : α}, 0 < b → (a / b < 1 ↔ a < b) := by
sorry
This theorem states that for any type `α` that forms a linearly ordered semifield, given any two elements `a` and `b` of this type, if `b` is greater than zero, then the fraction `a / b` is less than 1 if and only if `a` is less than `b`. This is a standard result in elementary number theory and algebra.
More concisely: For any linearly ordered semifield type `α`, elements `a` and `b` with `b` positive, have the property that `a / b` is less than 1 if and only if `a` is less than `b`.
|
mul_sub_mul_div_mul_nonpos
theorem mul_sub_mul_div_mul_nonpos :
∀ {α : Type u_2} [inst : LinearOrderedField α] {a b c d : α},
c ≠ 0 → d ≠ 0 → a / c ≤ b / d → (a * d - b * c) / (c * d) ≤ 0
This theorem, `mul_sub_mul_div_mul_nonpos`, is another way (an alias) to express the reverse direction of `mul_sub_mul_div_mul_nonpos_iff` in Lean 4. Given a linearly ordered field `α` and distinct non-zero elements `a`, `b`, `c`, `d` of type `α`, if the ratio `a / c` is less than or equal to the ratio `b / d`, then the expression `(a * d - b * c) / (c * d)` will be less than or equal to zero.
More concisely: If `α` is a linearly ordered field and `a, b, c, d` are distinct non-zero elements of `α` with `a/c <= b/d`, then `(ad - bc) / (cd) <= 0`.
|
div_le_div_of_mul_sub_mul_div_nonpos
theorem div_le_div_of_mul_sub_mul_div_nonpos :
∀ {α : Type u_2} [inst : LinearOrderedField α] {a b c d : α},
c ≠ 0 → d ≠ 0 → (a * d - b * c) / (c * d) ≤ 0 → a / c ≤ b / d
This theorem, `div_le_div_of_mul_sub_mul_div_nonpos`, states that for any type `α` that forms a linear ordered field, given four elements `a`, `b`, `c`, `d` of this field with `c` and `d` being non-zero, if the expression `(a * d - b * c) / (c * d)` is less than or equal to zero, then the inequality `a / c ≤ b / d` holds. In layman's terms, this shows a relationship between two fractions `a / c` and `b / d` under specific conditions involving their respective numerators and denominators.
More concisely: If `α` is a linear ordered field, `c`, `d` are non-zero elements of `α`, and `(a * d - b * c) / (c * d) ≤ 0`, then `a / c ≤ b / d`.
|
inv_le
theorem inv_le : ∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b : α}, 0 < a → 0 < b → (a⁻¹ ≤ b ↔ b⁻¹ ≤ a) := by
sorry
This theorem states that in any linearly ordered semi-field, if `a` and `b` are positive, then the reciprocal of `a` is less than or equal to `b` if and only if the reciprocal of `b` is less than or equal to `a`. This is a sort of 'reciprocal comparison' property of elements in these structures. There is also a related theorem `inv_le_of_inv_le` that provides a one-sided implication with one less assumption.
More concisely: In a linearly ordered semi-field, the reciprocal of one positive element is less than or equal to another if and only if the reciprocal of the other is less than or equal to the first.
|
div_le_div_right
theorem div_le_div_right :
∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b c : α}, 0 < c → (a / c ≤ b / c ↔ a ≤ b)
This theorem, `div_le_div_right`, states that for any type `α` that is a LinearOrderedSemifield (a field with an order relation that is both a total order and compatible with the field operations), and any elements `a`, `b`, and `c` of this type, if `c` is greater than zero, then the statement "the division of `a` by `c` is less than or equal to the division of `b` by `c`" is equivalent to the statement "`a` is less than or equal to `b`".
More concisely: For any LinearOrderedSemifield `α` and elements `a`, `b`, and `c` in `α` with `c` positive, `a ≤ b` if and only if `a / c ≤ b / c`.
|
inv_lt_inv
theorem inv_lt_inv :
∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b : α}, 0 < a → 0 < b → (a⁻¹ < b⁻¹ ↔ b < a)
The theorem `inv_lt_inv` states that for any linear ordered semifield `α` and any two elements `a` and `b` of `α` that are greater than zero, the inverse of `a` is less than the inverse of `b` if and only if `b` is less than `a`. This theorem captures a key property of inverses in ordered semifields: flipping the order of comparison and taking inverses are equivalent operations.
More concisely: For any linear ordered semifield `α` and elements `a, b` in `α` with `0 < a, b`, `a ^-1 < b ^-1` if and only if `b < a`.
|
Mathlib.Algebra.Order.Field.Basic._auxLemma.5
theorem Mathlib.Algebra.Order.Field.Basic._auxLemma.5 :
∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a : α}, (a⁻¹ < 1) = (a ≤ 0 ∨ 1 < a)
This theorem states that for any type `α` that is a Linear Ordered Semifield and any element `a` of type `α`, `a` inverse is less than 1 if and only if `a` is less than or equal to zero or `a` is greater than 1. Essentially, this theorem provides conditions under which the inverse of a number is less than one within the context of a Linear Ordered Semifield.
More concisely: In a Linear Ordered Semifield `α`, for any element `a` of type `α`, `a` has an inverse `b` such that `0 ≤ a ≤ 1` or `a > 1` implies `b < 1`.
|
one_le_div
theorem one_le_div : ∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b : α}, 0 < b → (1 ≤ a / b ↔ b ≤ a) := by
sorry
This theorem, `one_le_div`, states that for any type `α` in the universe `u_2` which is a Linear Ordered Semifield, and for any `a` and `b` of type `α`, when `b` is greater than 0, the condition that `1` is less than or equal to the division of `a` over `b` holds if and only if `b` is less than or equal to `a`. In simpler terms, in a certain kind of ordered field, if `b` is positive, then `1` is less than or equal to `a` divided by `b` exactly when `b` is less than or equal to `a`.
More concisely: In a Linear Ordered Semifield `α`, for all `a` and `b` of type `α` with `b > 0`, `1 ≤ a / b` if and only if `b ≤ a`.
|
div_le_iff
theorem div_le_iff : ∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b c : α}, 0 < b → (a / b ≤ c ↔ a ≤ c * b)
This theorem states that for any type `α` which forms a linear ordered semifield, and for any elements `a`, `b`, and `c` of this type where `b` is greater than zero, the statement "a divided by b is less than or equal to c" is equivalent to the statement "a is less than or equal to c times b". In other words, it relates a comparison involving division to a comparison involving multiplication in a specific mathematical structure.
More concisely: For any linear ordered semifield type `α` and elements `a`, `b` (with `b > 0`) in `α`, `a / b <= c` if and only if `a <= c * b`.
|
div_le_iff_of_neg
theorem div_le_iff_of_neg :
∀ {α : Type u_2} [inst : LinearOrderedField α] {a b c : α}, c < 0 → (b / c ≤ a ↔ a * c ≤ b)
This theorem states that for any type `α` which is a linear ordered field, and for any three elements `a`, `b`, `c` of the type `α`, if `c` is less than zero, then `b` divided by `c` is less than or equal to `a` if and only if `a` times `c` is less than or equal to `b`. It essentially provides a condition for a certain inequality involving division and multiplication to hold in the context of a linear ordered field, under the condition that `c` is negative.
More concisely: For any linear ordered field `α` and elements `a`, `b`, `c` in `α` with `c` negative, `b/c ≤ a` if and only if `a*c ≤ b`.
|
mul_le_of_nonneg_of_le_div
theorem mul_le_of_nonneg_of_le_div :
∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b c : α}, 0 ≤ b → 0 ≤ c → a ≤ b / c → a * c ≤ b
This theorem, `mul_le_of_nonneg_of_le_div`, states that for any linearly ordered semifield `α` and any elements `a`, `b`, and `c` of `α`, if `b` and `c` are non-negative and `a` is less than or equal to `b` divided by `c`, then the product of `a` and `c` is less than or equal to `b`. Note that `c` can be `0`, but `b` must be non-negative.
More concisely: If `a` is less than or equal to `b/c` and `b` is non-negative in a linearly ordered semifield, then `ac` is less than or equal to `b`.
|
half_pos
theorem half_pos : ∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a : α}, 0 < a → 0 < a / 2
This theorem, `half_pos`, states that for any type `α` that is a linear ordered semifield, if a value `a` of type `α` is greater than zero, then half of `a` is also greater than zero. In other words, dividing a positive number by 2 in such a field will still yield a positive number.
More concisely: If `α` is a linear ordered semifield and `0 < a : α`, then `0 < a / 2`.
|
le_div_iff
theorem le_div_iff : ∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b c : α}, 0 < c → (a ≤ b / c ↔ a * c ≤ b)
This theorem states that for any type `α` which forms a Linear Ordered Semifield, given any three elements `a`, `b`, and `c` of this type, where `c` is greater than zero, `a` is less than or equal to `b` divided by `c` if and only if `a` multiplied by `c` is less than or equal to `b`. Here, `/` denotes division and `*` denotes multiplication. So, essentially, it's a property about the relationship between multiplication, division and order in a linear ordered semifield.
More concisely: For any linear ordered semifield type `α` and elements `a`, `b`, and `c` (with `c > 0`), `a <= b / c` if and only if `a * c <= b`.
|
one_half_lt_one
theorem one_half_lt_one : ∀ {α : Type u_2} [inst : LinearOrderedSemifield α], 1 / 2 < 1
This theorem states that for any type `α` which is a Linear Ordered Semifield (a structure that generalizes both fields and ordered rings), the fraction 1/2 is less than 1. This is an example of a basic inequality property that holds in any such mathematical structure.
More concisely: For any Linear Ordered Semifield `α`, we have `1 / 2 < 1`.
|
le_div_iff_of_neg
theorem le_div_iff_of_neg :
∀ {α : Type u_2} [inst : LinearOrderedField α] {a b c : α}, c < 0 → (a ≤ b / c ↔ b ≤ a * c)
This theorem states that for any type `α` that is a linearly ordered field, and for any three elements `a`, `b` and `c` of type `α`, if `c` is less than zero, then `a` is less than or equal to `b` divided by `c` if and only if `b` is less than or equal to `a` multiplied by `c`. In mathematical terms, given a < 0, we have a ≤ b/c if and only if b ≤ ac.
More concisely: For any linearly ordered field `α` and elements `a, b, c` of type `α` with `c < 0`, we have `a ≤ b/c` if and only if `b ≤ a * c`.
|
div_le_iff'
theorem div_le_iff' : ∀ {α : Type u_2} [inst : LinearOrderedSemifield α] {a b c : α}, 0 < b → (a / b ≤ c ↔ a ≤ b * c)
This theorem states that for any type `α`, given a linearly ordered semiring structure on `α`, and any three elements `a`, `b`, `c` of `α`, if `b` is greater than 0, then the inequality `a / b ≤ c` is equivalent to the inequality `a ≤ b * c`. This theorem essentially represents one way of transferring the division by `b` in the first inequality to a multiplication by `b` in the second inequality.
More concisely: For any linearly ordered semiring `α` and elements `a, b, c` of `α` with `b > 0`, the inequalities `a / b <= c` and `a <= b * c` are equivalent.
|