mul_le_one₀
theorem mul_le_one₀ : ∀ {α : Type u_1} [inst : LinearOrderedCommGroupWithZero α] {a b : α}, a ≤ 1 → b ≤ 1 → a * b ≤ 1
This theorem, `mul_le_one₀`, states that for any type `α` that is a linearly ordered commutative group with zero, if two elements `a` and `b` of `α` are both less than or equal to one, then the product of `a` and `b` is also less than or equal to one.
More concisely: For any commutative group with zero `α` having the property that its elements are linearly ordered and less than or equal to one are closed under multiplication, the product of any two such elements is also less than or equal to one.
|
LinearOrderedCommGroupWithZero.zpow_neg'
theorem LinearOrderedCommGroupWithZero.zpow_neg' :
∀ {α : Type u_2} [self : LinearOrderedCommGroupWithZero α] (n : ℕ) (a : α),
LinearOrderedCommGroupWithZero.zpow (Int.negSucc n) a = (LinearOrderedCommGroupWithZero.zpow (↑n.succ) a)⁻¹
The theorem `LinearOrderedCommGroupWithZero.zpow_neg'` states that for any type `α` which forms a linearly ordered commutative group with zero, for any natural number `n` and any element `a` of type `α`, the inverse of `a` raised to the power of `-n - 1` (expressed as `Int.negSucc n` in the code) is equal to the inverse of `a` raised to the power of `n + 1`. In mathematical terms, it says that $a^{- (n + 1)} = \left(a^{n + 1}\right)^{-1}$ for any `a` in the group and any natural number `n`.
More concisely: For any linearly ordered commutative group with zero `α`, and for all natural numbers `n` and elements `a` in `α`, we have `(a ^ (Int.negSucc n)) ^-1 = a ^ (-n)`.
Or, in more traditional mathematical notation: `(a ^ (-(n + 1))) = (a ^ (n + 1)) ^-1`.
|
zero_lt_iff
theorem zero_lt_iff : ∀ {α : Type u_1} [inst : LinearOrderedCommMonoidWithZero α] {a : α}, 0 < a ↔ a ≠ 0
This theorem, named `zero_lt_iff`, states that for any type `α` that is a linearly ordered commutative monoid with zero, a value `a` of type `α` is greater than zero if and only if `a` is not equal to zero. In other words, for all elements in a linearly ordered commutative monoid with zero, being greater than zero is equivalent to not being zero.
More concisely: In a commutative monoid with a linear order and zero, an element is greater than zero if and only if it is not zero.
|
ne_zero_of_lt
theorem ne_zero_of_lt : ∀ {α : Type u_1} [inst : LinearOrderedCommMonoidWithZero α] {a b : α}, b < a → a ≠ 0
This theorem, `ne_zero_of_lt`, states that for any type `α` that is a linearly ordered commutative monoid with a zero element, if `b` is less than `a` (both `a` and `b` are of type `α`), then `a` is not equal to zero. In mathematical terms, for any elements `a` and `b` of such a structure, if `b < a`, then it must be the case that `a ≠ 0`.
More concisely: If `α` is a linearly ordered commutative monoid with a zero element, then for all `a b` in `α`, if `b < a`, then `a ≠ 0`.
|
zero_le'
theorem zero_le' : ∀ {α : Type u_1} [inst : LinearOrderedCommMonoidWithZero α] {a : α}, 0 ≤ a
This theorem states that for all types `α` that are instances of the `LinearOrderedCommMonoidWithZero` class, zero is less than or equal to any element `a` of type `α`. In other words, in any ordered commutative monoid with zero, zero is the smallest or equal to every element.
More concisely: For all types `α` instancing `LinearOrderedCommMonoidWithZero`, `0 ≤ a` holds for all `a` in `α`.
|
LinearOrderedCommMonoidWithZero.zero_mul
theorem LinearOrderedCommMonoidWithZero.zero_mul :
∀ {α : Type u_2} [self : LinearOrderedCommMonoidWithZero α] (a : α), 0 * a = 0
This theorem states that zero is a left absorbing element for multiplication in the context of a linear ordered commutative monoid with zero. Specifically, for any type `α` that has a structure of a linear ordered commutative monoid with zero, and for any element `a` of type `α`, the product of zero and `a` is always zero.
More concisely: In a commutative monoid with zero, the multiplication of any element with zero is equal to zero.
|
LinearOrderedCommGroupWithZero.zpow_zero'
theorem LinearOrderedCommGroupWithZero.zpow_zero' :
∀ {α : Type u_2} [self : LinearOrderedCommGroupWithZero α] (a : α), LinearOrderedCommGroupWithZero.zpow 0 a = 1
The theorem `LinearOrderedCommGroupWithZero.zpow_zero'` states that for any element `a` from a type `α`, which is a linearly ordered commutative group with zero, the integer power of `a` to the 0th power is 1. In mathematical terms, the theorem states that \(a^0 = 1\) for all `a` in `α`.
More concisely: For any element `a` in a linearly ordered commutative group with zero, `a^0 = 1`.
|
LinearOrderedCommMonoidWithZero.mul_zero
theorem LinearOrderedCommMonoidWithZero.mul_zero :
∀ {α : Type u_2} [self : LinearOrderedCommMonoidWithZero α] (a : α), a * 0 = 0
This theorem states that zero is a right-absorbing element for multiplication in the context of a linear ordered commutative monoid with zero. In other words, for any type `α` that has a structure of a linear ordered commutative monoid with zero (denoted `LinearOrderedCommMonoidWithZero α`), multiplying any element `a` of `α` by zero results in zero, i.e., `a * 0 = 0` for all `a`.
More concisely: In a linear ordered commutative monoid with zero, zero is a right identity for multiplication.
|
le_of_le_mul_right
theorem le_of_le_mul_right :
∀ {α : Type u_1} [inst : LinearOrderedCommGroupWithZero α] {a b c : α}, c ≠ 0 → a * c ≤ b * c → a ≤ b
This theorem states that for any instance `α` of a type `u_1` that forms a linear ordered commutative group with zero, and for any three elements `a`, `b`, and `c` of this type, if `c` is not equal to zero and the product of `a` and `c` is less than or equal to the product of `b` and `c`, then `a` is less than or equal to `b`. Essentially, this theorem allows cancellation in inequalities for commutative groups with a linear order and zero element, under the condition that the element being 'cancelled' is not zero.
More concisely: If `α` is a commutative group with a linear order and zero, and `a`, `b`, and `c` are elements of `α` with `c ≠ 0`, then `a ≤ b` if and only if `a * c ≤ b * c`.
|
LinearOrderedCommGroupWithZero.zpow_succ'
theorem LinearOrderedCommGroupWithZero.zpow_succ' :
∀ {α : Type u_2} [self : LinearOrderedCommGroupWithZero α] (n : ℕ) (a : α),
LinearOrderedCommGroupWithZero.zpow (Int.ofNat n.succ) a =
LinearOrderedCommGroupWithZero.zpow (Int.ofNat n) a * a
The theorem `LinearOrderedCommGroupWithZero.zpow_succ'` states that for any linearly ordered commutative group with a zero element, denoted here by `α`, any natural number `n`, and any element `a` of `α`, we have that raising `a` to the power of `(n + 1)` is the same as multiplying the result of raising `a` to the power of `n` by `a`. In other words, it expresses the property `a ^ (n + 1) = a ^ n * a`. This holds for both positive and negative integers, with `a ^ (-n) = a⁻¹ * ··· * a⁻¹` (`n` times).
More concisely: For any linearly ordered commutative group with a zero element, for all natural numbers $n$ and elements $a$ in the group, we have $a^{n+1} = a^n \cdot a$. This holds for both positive and negative integers, with $a^{-n} = a^{-1} \cdot \dotsb \cdot a^{-1}$ ($n$ times).
|
LinearOrderedCommGroupWithZero.div_eq_mul_inv
theorem LinearOrderedCommGroupWithZero.div_eq_mul_inv :
∀ {α : Type u_2} [self : LinearOrderedCommGroupWithZero α] (a b : α), a / b = a * b⁻¹
This theorem states that for any type `α` that is a linear ordered commutative group with zero, the division operation `a / b` of any two elements `a` and `b` from `α` is equivalent to the multiplication of `a` with the multiplicative inverse of `b` (notated as `b⁻¹`). In mathematical terms, for all `a` and `b` in a linear ordered commutative group with zero, `a / b = a * b⁻¹`.
More concisely: In a linear ordered commutative group with zero, the division operation is equivalent to multiplication with the multiplicative inverse: `a / b = a * b⁻¹` for all `a` and `b` in the group.
|
one_le_mul₀
theorem one_le_mul₀ : ∀ {α : Type u_1} [inst : LinearOrderedCommGroupWithZero α] {a b : α}, 1 ≤ a → 1 ≤ b → 1 ≤ a * b
This theorem, named `one_le_mul₀`, states that for any type `α` that is a linearly ordered commutative group with zero, given any two elements `a` and `b` of `α`, if both `a` and `b` are greater than or equal to 1, then their product `a * b` is also greater than or equal to 1. Essentially, it is a particular case of the inequality property in a ordered commutative group where multiplying two values each at least 1 results in a product that is also at least 1.
More concisely: For any commutative group with zero `α` and `1 ≤ a, b ∈ α`, we have `1 ≤ a * b`.
|
mul_inv_le_of_le_mul
theorem mul_inv_le_of_le_mul :
∀ {α : Type u_1} [inst : LinearOrderedCommGroupWithZero α] {a b c : α}, a ≤ b * c → a * c⁻¹ ≤ b
This theorem states that for any linearly ordered commutative group with zero, specifically for any elements `a`, `b`, and `c` in this group, if `a` is less than or equal to the product of `b` and `c`, then the product of `a` and the inverse of `c` is less than or equal to `b`. This kind of result would often be used in algebraic manipulations in the field of order theory or group theory.
More concisely: If `a` is less than or equal to the product of `b` and `c` in a linearly ordered commutative group with zero, then `a * b^-1` is less than or equal to `c`.
|
inv_le_inv₀
theorem inv_le_inv₀ :
∀ {α : Type u_1} [inst : LinearOrderedCommGroupWithZero α] {a b : α}, a ≠ 0 → b ≠ 0 → (a⁻¹ ≤ b⁻¹ ↔ b ≤ a) := by
sorry
This theorem states that for any type `α` which has the structure of a linearly ordered commutative group with zero, given any two non-zero elements `a` and `b` of this type, the reciprocal of `a` (denoted by `a⁻¹`) is less than or equal to the reciprocal of `b` (denoted by `b⁻¹`) if and only if `b` is less than or equal to `a`. This is a standard result about orderings and reciprocals in the field of algebra.
More concisely: For any linearly ordered commutative group with zero `α`, if `a` and `b` are non-zero elements of `α` with `a ≤ b`, then `a⁻¹ ≥ b⁻¹`.
|
WithZero.zero_le
theorem WithZero.zero_le : ∀ {α : Type u_1} [inst : Preorder α] (a : WithZero α), 0 ≤ a
The theorem `WithZero.zero_le` states that for any type `α` which has a defined `Preorder` (a mathematical structure that captures the intuitive notion of an ordering that is "less than", "equal to", or "greater than"), when we add an extra element `0` to this type to create `WithZero α`, the new element `0` is less than or equal to any other element `a` in `WithZero α`. In other words, `0` is the least element in the `WithZero α` structure for all possible values of `α` that have a `Preorder` structure.
More concisely: For any type `α` with a `Preorder`, the zero element `0` in `WithZero α` is less than or equal to any element `a` in `WithZero α`.
|
not_lt_zero'
theorem not_lt_zero' : ∀ {α : Type u_1} [inst : LinearOrderedCommMonoidWithZero α] {a : α}, ¬a < 0
This theorem states that for any type `α` that is a linear ordered commutative monoid with zero, no element `a` of that type can be less than zero. In other words, in any such structure, zero is the smallest element.
More concisely: In any linear ordered commutative monoid with zero, zero is the smallest element.
|
LinearOrderedCommMonoidWithZero.zero_le_one
theorem LinearOrderedCommMonoidWithZero.zero_le_one :
∀ {α : Type u_2} [self : LinearOrderedCommMonoidWithZero α], 0 ≤ 1
This theorem states that zero is less than or equal to one in any linearly ordered commutative monoid with zero. In particular, for any type `α` that has a structure of a linearly ordered commutative monoid with zero, the element `0` of `α` is always less than or equal to the element `1` of `α`. This is a fundamental property that is expected in a mathematical structure that behaves like the nonnegative real numbers or the nonnegative integers.
More concisely: In any linearly ordered commutative monoid with zero, the zero element is less than or equal to the one element.
|
LinearOrderedCommGroupWithZero.inv_zero
theorem LinearOrderedCommGroupWithZero.inv_zero : ∀ {α : Type u_2} [self : LinearOrderedCommGroupWithZero α], 0⁻¹ = 0
This theorem states that in any linearly ordered commutative group with zero, the inverse of `0` is `0`. Here, the group is of type `α`, and the group operation is defined in such a way that it respects the linear order and the commutative law. This property is a characteristic of groups with zero, where the element `0` is its own inverse.
More concisely: In any commutative group of type `α` with a linear order and zero element `0`, `0` is its own additive inverse.
|
mul_le_mul_right₀
theorem mul_le_mul_right₀ :
∀ {α : Type u_1} [inst : LinearOrderedCommGroupWithZero α] {a b c : α}, c ≠ 0 → (a * c ≤ b * c ↔ a ≤ b)
This theorem states that for any type `α` which is a linearly ordered commutative group with an identity element that is distinguished as zero, given any three elements `a`, `b`, and `c` of this type, if `c` is not zero, then the product of `a` and `c` is less than or equal to the product of `b` and `c` if and only if `a` is less than or equal to `b`. This essentially means that in such a group, multiplication by a non-zero element preserves the order of elements.
More concisely: For any commutative group with identity and total ordering where multiplication by a non-zero element preserves the order, the product of two elements is less than or equal to the product of another element if and only if the first element is less than or equal to the second.
|
LinearOrderedCommGroupWithZero.mul_inv_cancel
theorem LinearOrderedCommGroupWithZero.mul_inv_cancel :
∀ {α : Type u_2} [self : LinearOrderedCommGroupWithZero α] (a : α), a ≠ 0 → a * a⁻¹ = 1
This theorem states that for every non-zero element `a` of a certain type `α`, which is a linear ordered commutative group with zero, multiplying `a` with its inverse (`a⁻¹`) yields the multiplicative identity, which is `1`. This essentially means every non-zero element in such a group is invertible.
More concisely: In a commutative group with zero and identity element `1`, every non-zero element `a` has an additive inverse `-a` such that `a * a⁻¹ = 1`. (Note: The statement is typically expressed in terms of multiplicative inverses, but since Lean uses additive notation for groups, the statement is given in additive inverse notation in Lean.)
|
WithZero.coe_le_coe
theorem WithZero.coe_le_coe : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, ↑a ≤ ↑b ↔ a ≤ b
This theorem states that for any type `α` with a preorder (a mathematical structure where all elements are comparable), the order of two elements `a` and `b` of type `α` remains the same when they are lifted (i.e., ↑ denotes lifting) into the `WithZero` type (which adds a zero element to the type `α` if it doesn't already exist). In other words, `a` is less than or equal to `b` in the original type if and only if `a` is less than or equal to `b` in the `WithZero` type.
More concisely: For any type `α` with a preorder and any elements `a` and `b` of type `α`, `a ≤ b` if and only if `↑a ≤ ↑b` in the `WithZero` type extension of `α`.
|
le_zero_iff
theorem le_zero_iff : ∀ {α : Type u_1} [inst : LinearOrderedCommMonoidWithZero α] {a : α}, a ≤ 0 ↔ a = 0
This theorem, `le_zero_iff`, is a statement about objects of a certain type, specifically a type `α` that forms a linearly ordered commutative monoid with zero. For any element `a` of this type, the theorem asserts that `a` is less than or equal to zero if and only if `a` is equal to zero. This captures the fact that in these algebraic structures, zero is the smallest element, and anything less than or equal to zero must in fact be zero itself.
More concisely: For any element `a` in a commutative monoid with a zero, `a ≤ 0` if and only if `a = 0`.
|
pow_lt_pow₀
theorem pow_lt_pow₀ :
∀ {α : Type u_1} [inst : LinearOrderedCommGroupWithZero α] {a : α} {m n : ℕ}, 1 < a → m < n → a ^ m < a ^ n := by
sorry
This theorem, `pow_lt_pow₀`, states that for any type `α` that is a linearly ordered commutative group with zero, and for any instance of this type `a` and natural numbers `m` and `n`, if `a` is greater than 1 and `m` is less than `n`, then `a` raised to the power `m` is less than `a` raised to the power `n`. Essentially, in a set that respects the rules of a commutative group and has an order, if we have a number greater than 1, increasing the exponent will result in a larger number.
More concisely: For any commutative group with zero `α` and `a:` `α` with `a > 1`, `m:` `ℕ`, and `n:` `ℕ` (`m < n`), `a^m < a^n`.
|