LinearOrderedField.mul_inv_cancel
theorem LinearOrderedField.mul_inv_cancel :
∀ {α : Type u_2} [self : LinearOrderedField α] (a : α), a ≠ 0 → a * a⁻¹ = 1
This theorem states that for any non-zero value `a` in a linear ordered field `α`, the multiplicative inverse of `a` (denoted as `a⁻¹`) is a right inverse. This means that multiplying `a` by its inverse results in the multiplicative identity, which is `1`. In mathematical terms, if `a` is not equal to `0`, then `a * a⁻¹ = 1`.
More concisely: For any non-zero element `a` in a linear ordered field, `a * a⁻¹ = 1`.
|
inv_nonpos
theorem inv_nonpos : ∀ {α : Type u_1} [inst : LinearOrderedSemifield α] {a : α}, a⁻¹ ≤ 0 ↔ a ≤ 0
This theorem named `inv_nonpos` states that for any type `α` which is a Linear Ordered Semifield, an element `a` of this type has a nonpositive inverse if and only if `a` itself is nonpositive. In other words, in such a field, an element and its inverse share the same sign, so if `a` is less than or equal to zero, then its inverse `a⁻¹` is also less than or equal to zero.
More concisely: For any Linear Ordered Semifield type `α`, if `a` is an element of `α` with nonpositive inverse, then `a` is also nonpositive.
|
LinearOrderedSemifield.zpow_neg'
theorem LinearOrderedSemifield.zpow_neg' :
∀ {α : Type u_2} [self : LinearOrderedSemifield α] (n : ℕ) (a : α),
LinearOrderedSemifield.zpow (Int.negSucc n) a = (LinearOrderedSemifield.zpow (↑n.succ) a)⁻¹
This theorem states that for any natural number `n` and any element `a` from a type `α` that constitutes a linearly ordered semifield, the power operation where `a` is raised to the power of the negation of `n + 1` (i.e., `a ^ -(n + 1)`) is equal to the inverse of the operation where `a` is raised to the power of `n + 1` (i.e., `(a ^ (n + 1))⁻¹`). In other words, taking an element to the power of a negative integer in a linearly ordered semifield is equivalent to taking the inverse of that element raised to the corresponding positive power.
More concisely: For any linearly ordered semifield element `a` and natural number `n`, `a ^ (-(n + 1)) = (a ^ (n + 1))⁻¹`.
|
inv_lt_zero
theorem inv_lt_zero : ∀ {α : Type u_1} [inst : LinearOrderedSemifield α] {a : α}, a⁻¹ < 0 ↔ a < 0
The theorem `inv_lt_zero` states that for any type `α` which is a LinearOrderedSemifield, a type of field with a linear order, a element `a` from `α` has its inverse less than zero if and only if `a` itself is less than zero. In terms of mathematics, this theorem says: given a linear ordered semifield, the inverse of a number is less than zero if and only if the number itself is less than zero.
More concisely: For any linear ordered semifield type `α`, if `a` is an element of `α` with `a < 0`, then `0 < -a`. Conversely, if `-a < 0`, then `a < 0`.
|
LinearOrderedSemifield.mul_inv_cancel
theorem LinearOrderedSemifield.mul_inv_cancel :
∀ {α : Type u_2} [self : LinearOrderedSemifield α] (a : α), a ≠ 0 → a * a⁻¹ = 1
The theorem `LinearOrderedSemifield.mul_inv_cancel` states that for every nonzero element `a` of a type `α`, where `α` is a linearly ordered semifield, the product of `a` and its reciprocal (`a⁻¹`) is equal to 1. This is equivalent to saying that every nonzero element in a linearly ordered semifield is invertible, with its inverse being its reciprocal.
More concisely: In a linearly ordered semifield, every nonzero element has an inverse equal to its reciprocal, making the product of an element and its inverse equal to 1.
|
inv_nonneg_of_nonneg
theorem inv_nonneg_of_nonneg : ∀ {α : Type u_1} [inst : LinearOrderedSemifield α] {a : α}, 0 ≤ a → 0 ≤ a⁻¹
This theorem, `inv_nonneg_of_nonneg`, states that for any type `α` that is a Linear Ordered Semifield, if a value `a` of type `α` is nonnegative (i.e., `a` is greater than or equal to 0), then the multiplicative inverse of `a` (denoted as `a⁻¹`) is also nonnegative. In other words, if `a` is nonnegative in a Linear Ordered Semifield, then `1/a` is nonnegative as well.
More concisely: In a Linear Ordered Semifield, if `a` is nonnegative, then its multiplicative inverse is also nonnegative.
|
LinearOrderedField.inv_zero
theorem LinearOrderedField.inv_zero : ∀ {α : Type u_2} [self : LinearOrderedField α], 0⁻¹ = 0
This theorem states that the multiplicative inverse of `0`, denoted as `0⁻¹`, is `0` in any linearly ordered field. Here, a linearly ordered field is a field which is also a linear order, meaning it satisfies certain properties like associativity, commutativity, distributivity, and order axioms. We define this property by convention, since division by zero is undefined. Thus, in this context, `0⁻¹` is defined to be `0`.
More concisely: In any linearly ordered field, the multiplicative identity for the additive identity (0) is 0. (Equivalently, the multiplicative inverse of 0 is 0.)
|
zpow_nonneg
theorem zpow_nonneg : ∀ {α : Type u_1} [inst : LinearOrderedSemifield α] {a : α}, 0 ≤ a → ∀ (n : ℤ), 0 ≤ a ^ n := by
sorry
This theorem states that for any type `α` which forms a linear ordered semifield, any non-negative number `a` of type `α`, raised to any integer power `n`, is always non-negative. In mathematical terms, this could be written as: for any non-negative α, 0 ≤ a, and any integer n, we have 0 ≤ a^n.
More concisely: For any non-negative element $a$ in a linear ordered semifield $\alpha$, $a$ raised to any integer power $n$ is also non-negative. In mathematical notation: $0 \leq a \implies 0 \leq a^n$.
|
LinearOrderedSemifield.div_eq_mul_inv
theorem LinearOrderedSemifield.div_eq_mul_inv :
∀ {α : Type u_2} [self : LinearOrderedSemifield α] (a b : α), a / b = a * b⁻¹
This theorem states that for any type `α` that is an instance of a `LinearOrderedSemifield` (a structure combining properties of ordered fields and semirings), the division operation `a / b` for any elements `a` and `b` of `α` is equivalent to the multiplication of `a` and the multiplicative inverse of `b`, written as `b⁻¹`. In other words, in such a structure, dividing by `b` is the same as multiplying by `b`'s reciprocal.
More concisely: For any type `α` that is a LinearOrderedSemifield, the division operation `a / b` equals the multiplication of `a` and the multiplicative inverse of `b`, i.e., `a / b = a * b⁻¹`.
|
LinearOrderedSemifield.inv_zero
theorem LinearOrderedSemifield.inv_zero : ∀ {α : Type u_2} [self : LinearOrderedSemifield α], 0⁻¹ = 0
This theorem states that in any linearly ordered semifield, the multiplicative inverse (or reciprocal) of zero is zero. That is, the number which when multiplied with zero gives the multiplicative identity (typically one), is zero itself.
More concisely: In a linearly ordered semifield, the multiplicative identity is the additive identity (zero).
|
LinearOrderedField.div_eq_mul_inv
theorem LinearOrderedField.div_eq_mul_inv : ∀ {α : Type u_2} [self : LinearOrderedField α] (a b : α), a / b = a * b⁻¹
This theorem, named `LinearOrderedField.div_eq_mul_inv`, states that for any linear ordered field `α`, and any two elements `a` and `b` of `α`, the operation of division `a / b` is equivalent to multiplying `a` by the multiplicative inverse of `b` (i.e., `a * b⁻¹`). Essentially, it defines division in terms of multiplication and inversion in the field.
More concisely: For any linear ordered field `α`, and elements `a` and `b` in `α` with `b ≠ 0`, we have `a / b = a * b⁻¹`.
|
one_div_nonneg
theorem one_div_nonneg : ∀ {α : Type u_1} [inst : LinearOrderedSemifield α] {a : α}, 0 ≤ 1 / a ↔ 0 ≤ a
This theorem states that for any type `α` that forms a linearly ordered semiring (a structure with both addition and multiplication that behaves like the real numbers in some sense), if `a` is an element of `α`, then `1 / a` is non-negative if and only if `a` itself is non-negative. Here, non-negativity means the value is either greater than or equal to zero.
More concisely: For any linearly ordered semiring type `α`, element `a` belongs to `α` is non-negative if and only if its multiplicative inverse `1 / a` is non-negative.
|
inv_nonneg
theorem inv_nonneg : ∀ {α : Type u_1} [inst : LinearOrderedSemifield α] {a : α}, 0 ≤ a⁻¹ ↔ 0 ≤ a
This theorem, named `inv_nonneg`, states that for any type `α` that has a structure of a linear ordered semifield, the inverse `a⁻¹` of an element `a` in `α` is nonnegative (i.e., `0 ≤ a⁻¹`) if and only if `a` itself is nonnegative (i.e., `0 ≤ a`). In mathematical terms, this theorem ensures the preservation of non-negativity through inversion in a linear ordered semifield.
More concisely: For any linear ordered semifield `α`, if `0 ≤ a` then `0 ≤ a⁻¹`.
|
LinearOrderedField.zpow_succ'
theorem LinearOrderedField.zpow_succ' :
∀ {α : Type u_2} [self : LinearOrderedField α] (n : ℕ) (a : α),
LinearOrderedField.zpow (Int.ofNat n.succ) a = LinearOrderedField.zpow (Int.ofNat n) a * a
This theorem states that, for any linear ordered field "α" and any natural number "n", the power of any element "a" of the field raised to "n+1" is equal to "a" raised to the power of "n" multiplied by "a". In simpler terms, it's saying that incrementing the exponent by one effectively multiplies the overall expression by the base "a". This is a generalization of the classic property of exponentiation seen in mathematics: a^(n+1) = a^n * a.
More concisely: For any linear ordered field α and natural number n, a^(n+1) = a^n * a.
|
zpow_pos_of_pos
theorem zpow_pos_of_pos : ∀ {α : Type u_1} [inst : LinearOrderedSemifield α] {a : α}, 0 < a → ∀ (n : ℤ), 0 < a ^ n := by
sorry
This theorem states that for any type `α` that is a linearly ordered semifield, if `a` is a positive element of this type, then raising `a` to any integer power `n` will always result in a positive value. In other words, if `0 < a`, then `0 < a^n` for any integer `n`. This is essentially an extension of the mathematical fact that any positive number raised to any power is always positive.
More concisely: For any linearly ordered semifield type `α` and positive element `a` of `α`, `0 < a` implies `0 < a^n` for all integers `n`.
|
LinearOrderedField.zpow_zero'
theorem LinearOrderedField.zpow_zero' :
∀ {α : Type u_2} [self : LinearOrderedField α] (a : α), LinearOrderedField.zpow 0 a = 1
This theorem states that for any element 'a' in a linearly ordered field 'α', the zeroth power of 'a' is always 1. In mathematical terms, it asserts that `a ^ 0 = 1` for any `a` in a LinearOrderedField `α`.
More concisely: In any linearly ordered field, the zeroth power of any element equals 1.
|
div_pos
theorem div_pos : ∀ {α : Type u_1} [inst : LinearOrderedSemifield α] {a b : α}, 0 < a → 0 < b → 0 < a / b
This theorem, named `div_pos`, states that for any type `α` that is a `LinearOrderedSemifield` (a structure where order and operations like addition, subtraction, multiplication, and division are defined and follow certain rules), if `a` and `b` are two elements of `α` where both `a` and `b` are greater than zero, then the result of `a` divided by `b` is also greater than zero. In other words, the division of two positive numbers in a linearly ordered semifield produces a positive number.
More concisely: If `α` is a LinearOrderedSemifield and `a`, `b` are positive elements of `α`, then `a / b` is also positive.
|
div_nonneg
theorem div_nonneg : ∀ {α : Type u_1} [inst : LinearOrderedSemifield α] {a b : α}, 0 ≤ a → 0 ≤ b → 0 ≤ a / b
This theorem, `div_nonneg`, asserts that for any type `α` that has a structure of `LinearOrderedSemifield`, if `a` and `b` are two elements of `α` such that both `a` and `b` are nonnegative (i.e., greater than or equal to zero), then the division of `a` by `b` is also nonnegative. That is, in the context of a linearly ordered semifield, if you divide a nonnegative number by another nonnegative number, the result will be nonnegative.
More concisely: In a linearly ordered semifield, if both dividend and divisor are nonnegative, then the quotient is nonnegative.
|
one_div_pos
theorem one_div_pos : ∀ {α : Type u_1} [inst : LinearOrderedSemifield α] {a : α}, 0 < 1 / a ↔ 0 < a
This theorem, named `one_div_pos`, states that for all types `α` that have a `LinearOrderedSemifield` structure, and for all elements `a` of type `α`, the reciprocal of `a` (1 / a) is greater than zero if and only if `a` itself is greater than zero. In mathematical terms, for any real or complex number `a`, 1/a > 0 if and only if a > 0.
More concisely: For any type `α` with a `LinearOrderedSemifield` structure and any `a` in `α`, 1 / a > 0 if and only if a > 0.
|
LinearOrderedSemifield.zpow_succ'
theorem LinearOrderedSemifield.zpow_succ' :
∀ {α : Type u_2} [self : LinearOrderedSemifield α] (n : ℕ) (a : α),
LinearOrderedSemifield.zpow (Int.ofNat n.succ) a = LinearOrderedSemifield.zpow (Int.ofNat n) a * a
The theorem `LinearOrderedSemifield.zpow_succ'` states that for any type `α` which forms a linearly ordered semifield, and for any natural number `n` and element `a` from that type `α`, the power of `a` raised to `(n + 1)` is equal to the power of `a` raised to `n`, multiplied by `a`. In mathematical notation, this would be expressed as `a ^ (n + 1) = a ^ n * a`.
More concisely: For any linearly ordered semifield type `α` and natural number `n`, the law of exponent distribution holds: `a ^ (n + 1) = a ^ n * a`, for all `a` in `α`.
|
LinearOrderedSemifield.zpow_zero'
theorem LinearOrderedSemifield.zpow_zero' :
∀ {α : Type u_2} [self : LinearOrderedSemifield α] (a : α), LinearOrderedSemifield.zpow 0 a = 1
This theorem states that for any element `a` from a linear ordered semifield `α`, the zeroth power of `a` equals to one. In other words, in any linear ordered semifield, raising any element to the power of zero results in the multiplicative identity element, which is one.
More concisely: In any linear ordered semifield, for all elements `a`, `a^0 = 1`.
|
inv_pos_of_pos
theorem inv_pos_of_pos : ∀ {α : Type u_1} [inst : LinearOrderedSemifield α] {a : α}, 0 < a → 0 < a⁻¹
This theorem, `inv_pos_of_pos`, states that for any value `a` from a linearly ordered semifield `α`, if `a` is greater than zero, then its multiplicative inverse `a⁻¹` is also greater than zero. In mathematical terms, if `0 < a`, then it follows that `0 < a⁻¹`. This theorem essentially mirrors the reverse direction of the `inv_pos` theorem.
More concisely: If `α` is a linearly ordered semifield and `0 < a` in `α`, then `0 < a⁻¹`.
|
LinearOrderedField.zpow_neg'
theorem LinearOrderedField.zpow_neg' :
∀ {α : Type u_2} [self : LinearOrderedField α] (n : ℕ) (a : α),
LinearOrderedField.zpow (Int.negSucc n) a = (LinearOrderedField.zpow (↑n.succ) a)⁻¹
This theorem states that for any linear ordered field `α` and any natural number `n` and element `a` of `α`, the definition of the power operation in the negative case `a ^ -(n + 1)` is equal to the inverse of the power operation in the positive case `(a ^ (n + 1))⁻¹`. In other words, raising `a` to the power of the negative of `(n + 1)` is the same as taking the reciprocal of `a` raised to the power of `(n + 1)`.
More concisely: For any linear ordered field `α` and natural number `n`, `a ^ (-(n + 1)) = (a ^ (n + 1))⁻¹`.
|
inv_pos
theorem inv_pos : ∀ {α : Type u_1} [inst : LinearOrderedSemifield α] {a : α}, 0 < a⁻¹ ↔ 0 < a
This theorem states that for any type `α` that forms a `LinearOrderedSemifield`, the reciprocal of a given element `a` of `α` is greater than zero if and only if `a` is greater than zero. In mathematical terms, for any real number `a`, `0 < 1/a` is true if and only if `0 < a` is true.
More concisely: For any type `α` that is a LinearOrderedSemifield, `0 < a` implies `0 < 1/a`.
|