CanonicallyLinearOrderedSemifield.mul_inv_cancel
theorem CanonicallyLinearOrderedSemifield.mul_inv_cancel :
∀ {α : Type u_2} [self : CanonicallyLinearOrderedSemifield α] (a : α), a ≠ 0 → a * a⁻¹ = 1
The theorem states that for any non-zero element 'a' in a canonically linear ordered semi-field (a structure defined by the type variable `α`), the product of 'a' and its inverse is equal to 1. This is a fundamental property of fields, asserting that every non-zero element is invertible, i.e., it has a multiplicative inverse.
More concisely: For any non-zero element 'a' in a canonically linear ordered semi-field, 'a' multiplied by its multiplicative inverse equals 1.
|
CanonicallyLinearOrderedSemifield.le_total
theorem CanonicallyLinearOrderedSemifield.le_total :
∀ {α : Type u_2} [self : CanonicallyLinearOrderedSemifield α] (a b : α), a ≤ b ∨ b ≤ a
The theorem `CanonicallyLinearOrderedSemifield.le_total` states that for any type `α` that is a canonically linear ordered semifield, and for any two elements `a` and `b` of type `α`, either `a` is less than or equal to `b`, or `b` is less than or equal to `a`. In other words, in a canonically linear ordered semifield, any two elements are comparable, underlining the totalness of the linear order.
More concisely: In a canonically linear ordered semifield, every two elements are comparable.
|
CanonicallyLinearOrderedSemifield.min_def
theorem CanonicallyLinearOrderedSemifield.min_def :
∀ {α : Type u_2} [self : CanonicallyLinearOrderedSemifield α] (a b : α), min a b = if a ≤ b then a else b := by
sorry
This theorem states that for any canonically linearly ordered semifield `α` and any two elements `a` and `b` of this semifield, the minimum of `a` and `b` is defined as `a` if `a` is less than or equal to `b`, otherwise it is `b`. This means that the `min` function behaves exactly as you would expect when using the `≤` operator to compare two elements of `α`.
More concisely: For any canonically linearly ordered semifield `α`, the minimum of two elements `a` and `b` is `a` if `a` is less than or equal to `b`, and `b` otherwise. (i.e., `min a b = a ∧ a ≤ b ∨ b < a`).
|
CanonicallyLinearOrderedSemifield.zero_le_one
theorem CanonicallyLinearOrderedSemifield.zero_le_one :
∀ {α : Type u_2} [self : CanonicallyLinearOrderedSemifield α], 0 ≤ 1
This theorem states that in any canonically linear ordered semifield, the value zero is less than or equal to one. Here, a "canonically linear ordered semifield" refers to a mathematical structure (a set with two operations, addition and multiplication) that is an ordered semiring (meaning it respects the properties of addition and multiplication in an ordered context) and it has a canonical linear order (a well-defined notion of "less than" that covers every pair of elements in the set).
More concisely: In any canonically linear ordered semifield, 0 is less than or equal to 1.
|
CanonicallyLinearOrderedSemifield.mul_lt_mul_of_pos_right
theorem CanonicallyLinearOrderedSemifield.mul_lt_mul_of_pos_right :
∀ {α : Type u_2} [self : CanonicallyLinearOrderedSemifield α] (a b c : α), a < b → 0 < c → a * c < b * c
This theorem states that for any type `α` that is a "Canonically Linear Ordered Semifield" (a particular kind of mathematical structure), right multiplication by a positive element is strictly monotone. More concretely, if you have three elements `a`, `b`, and `c` from this structure such that `a` is less than `b` and `c` is positive (greater than zero), then the result of multiplying `a` by `c` is less than the result of multiplying `b` by `c`. In terms of mathematical notation, if `a < b` and `0 < c`, then `a * c < b * c`.
More concisely: For any Canonically Linear Ordered Semifield `α` and positive elements `a < b` in `α`, we have `a * c < b * c` for all `0 < c` in `α`.
|
CanonicallyLinearOrderedSemifield.mul_lt_mul_of_pos_left
theorem CanonicallyLinearOrderedSemifield.mul_lt_mul_of_pos_left :
∀ {α : Type u_2} [self : CanonicallyLinearOrderedSemifield α] (a b c : α), a < b → 0 < c → c * a < c * b
This theorem states that for any canonically ordered semifield, if you have three elements a, b, and c, such that a is less than b and c is positive, then the result of multiplying c with a is less than the result of multiplying c with b. In other words, left multiplication by a positive element in such a semifield is strictly monotone.
More concisely: In a canonically ordered semifield, for any positive elements a and b, we have a * c < b * c.
|
CanonicallyLinearOrderedSemifield.max_def
theorem CanonicallyLinearOrderedSemifield.max_def :
∀ {α : Type u_2} [self : CanonicallyLinearOrderedSemifield α] (a b : α), max a b = if a ≤ b then b else a := by
sorry
This theorem states that for any two elements `a` and `b` from a given canonically linearly ordered semifield, the maximum of `a` and `b` is defined to be `b` if `a` is less than or equal to `b`, otherwise it is `a`. In other words, it establishes an equivalence between the `max` function and the function you get from `maxOfLe`. This sets a standard behavior for obtaining the maximum of two elements in such a semifield.
More concisely: For any two elements `a` and `b` in a canonically linearly ordered semifield, `max a b = if a ≤ b then b else a`.
|
CanonicallyLinearOrderedSemifield.inv_zero
theorem CanonicallyLinearOrderedSemifield.inv_zero :
∀ {α : Type u_2} [self : CanonicallyLinearOrderedSemifield α], 0⁻¹ = 0
This theorem states that the multiplicative inverse (also known as reciprocal) of zero in any canonically linearly ordered semifield is zero. In other words, for any type `α` that is a canonically linearly ordered semifield, the value of `0⁻¹` (the inverse of zero) is always `0`. This is a common property in many algebraic structures where zero is its own inverse.
More concisely: In any canonically linearly ordered semifield, the multiplicative identity is equal to the additive zero. (Equivalently, the multiplicative inverse of zero is zero.)
|
CanonicallyLinearOrderedSemifield.div_eq_mul_inv
theorem CanonicallyLinearOrderedSemifield.div_eq_mul_inv :
∀ {α : Type u_2} [self : CanonicallyLinearOrderedSemifield α] (a b : α), a / b = a * b⁻¹
This theorem states that for any canonically linearly ordered semifield `α`, the operation of division of any two elements `a` and `b` in `α` is defined as the multiplication of `a` with the multiplicative inverse of `b` (expressed as `b⁻¹`). In mathematical notation, this concept is represented as `a / b = a * b⁻¹`.
More concisely: For any canonically linearly ordered semifield `α`, the division operation is equivalently defined as multiplication by the multiplicative inverse. That is, for all `a, b ∈ α`, `a / b = a * b⁻¹`.
|
CanonicallyLinearOrderedSemifield.zpow_succ'
theorem CanonicallyLinearOrderedSemifield.zpow_succ' :
∀ {α : Type u_2} [self : CanonicallyLinearOrderedSemifield α] (n : ℕ) (a : α),
CanonicallyLinearOrderedSemifield.zpow (Int.ofNat n.succ) a =
CanonicallyLinearOrderedSemifield.zpow (Int.ofNat n) a * a
This theorem states that for any canonically linear ordered semi-field `α` and any natural number `n`, if `a` is an element of `α`, then raising `a` to the power of `n + 1` is equivalent to raising `a` to the power `n` and then multiplying the result by `a`. In mathematical notation, this would be expressed as `a^(n+1) = a^n * a`. This property is a fundamental identity of exponentiation.
More concisely: For any canonically linear ordered semi-field `α` and natural number `n`, the operation of raising an element `a` in `α` to the power `n+1` is equivalent to raising `a` to the power `n` and then multiplying the result by `a`: `a^(n+1) = a^n * a`.
|
CanonicallyLinearOrderedSemifield.zpow_zero'
theorem CanonicallyLinearOrderedSemifield.zpow_zero' :
∀ {α : Type u_2} [self : CanonicallyLinearOrderedSemifield α] (a : α),
CanonicallyLinearOrderedSemifield.zpow 0 a = 1
This theorem states that for any element `a` of a type `α`, which is an instance of a canonically linearly ordered semifield, raising `a` to the power of zero using the `zpow` operation results in the identity element `1`. This corresponds to the mathematical statement that any number to the power of zero equals one, i.e., \(a^0 = 1\), where `a` is any member of the canonically linearly ordered semifield `α`.
More concisely: For any element `a` in a canonically linearly ordered semifield, `a^0` equals the identity element `1`.
|
CanonicallyLinearOrderedSemifield.compare_eq_compareOfLessAndEq
theorem CanonicallyLinearOrderedSemifield.compare_eq_compareOfLessAndEq :
∀ {α : Type u_2} [self : CanonicallyLinearOrderedSemifield α] (a b : α), compare a b = compareOfLessAndEq a b := by
sorry
This theorem asserts that, for any type `α` that is canonically linearly ordered and is also a semifield, the built-in `compare` operation for comparing two elements `a` and `b` of type `α` is equivalent to the `compareOfLessAndEq` function defined earlier. The `compareOfLessAndEq` function uses decidable less-than (`<`) and equality (`=`) to establish an ordering between `x` and `y`. In particular, `x < y` maps to `Ordering.lt` (meaning `x` is less than `y`), `x = y` maps to `Ordering.eq` (meaning `x` is equal to `y`), and otherwise, it results in `Ordering.gt` (signifying that `x` is greater than `y`). This theorem thus ensures the consistency between the natural comparison and the comparison determined by the `compareOfLessAndEq` function.
More concisely: For any canonically linearly ordered semifield type `α`, the built-in `compare` operation is equivalent to the `compareOfLessAndEq` function using decidable less-than and equality relations.
|
CanonicallyLinearOrderedSemifield.zpow_neg'
theorem CanonicallyLinearOrderedSemifield.zpow_neg' :
∀ {α : Type u_2} [self : CanonicallyLinearOrderedSemifield α] (n : ℕ) (a : α),
CanonicallyLinearOrderedSemifield.zpow (Int.negSucc n) a =
(CanonicallyLinearOrderedSemifield.zpow (↑n.succ) a)⁻¹
This theorem states that for any element `a` of a type `α` that is a canonically linearly ordered semifield, and for any natural number `n`, the power operation `a ^ -(n + 1)` is equal to the inverse of `a ^ (n + 1)`. In simpler words, raising `a` to the power of `-(n + 1)` is the same as taking the reciprocal of `a` raised to the power `(n + 1)`.
More concisely: For any element `a` in a canonically linearly ordered semifield `α`, the negative power `a ^ (-(n + 1))` equals the multiplicative inverse of `a ^ (n + 1)` for any natural number `n`.
|