LeanAide GPT-4 documentation

Module: Mathlib.Algebra.Order.Ring.Defs

two_mul_le_add_sq

theorem two_mul_le_add_sq : ∀ {α : Type u} [inst : LinearOrderedCommSemiring α] [inst_1 : ExistsAddOfLE α] (a b : α), 2 * a * b ≤ a ^ 2 + b ^ 2

The theorem `two_mul_le_add_sq` states the binary arithmetic mean-geometric mean inequality (also known as AM-GM inequality) for linearly ordered commutative semirings. Specifically, for any two elements `a` and `b` from a linearly ordered commutative semiring `α` (which also supports the existence of an additive operation for any two elements that satisfy the less than or equal to relation), the product of `a` and `b` multiplied by 2 is always less than or equal to the sum of the squares of `a` and `b`. In mathematical terms, this can be written as $2ab \leq a^2 + b^2$.

More concisely: For any elements $a$ and $b$ in a linearly ordered commutative semiring with additive operation, $2ab \leq a^2 + b^2$.

mul_lt_mul_of_neg_right

theorem mul_lt_mul_of_neg_right : ∀ {α : Type u} [inst : StrictOrderedSemiring α] {a b c : α} [inst_1 : ExistsAddOfLE α], b < a → c < 0 → a * c < b * c

This theorem states that for any strictly ordered semiring `α` and three elements `a`, `b`, and `c` in `α` (where addition can be defined from less than or equal to), if `b` is less than `a` and `c` is less than zero, then the product of `a` and `c` is less than the product of `b` and `c`. In essence, it is a statement about the effect of multiplication by a negative number on the order of elements in a strictly ordered semiring.

More concisely: In a strictly ordered semiring, if `a` is greater than `b` and `c` is negative, then `a * c` is less than `b * c`.

two_mul_le_add_pow_two

theorem two_mul_le_add_pow_two : ∀ {α : Type u} [inst : LinearOrderedCommSemiring α] [inst_1 : ExistsAddOfLE α] (a b : α), 2 * a * b ≤ a ^ 2 + b ^ 2

This theorem, named `two_mul_le_add_pow_two`, states the binary arithmetic mean-geometric mean inequality (also known as the AM-GM inequality) for linearly ordered commutative semirings. Specifically, for any two elements `a` and `b` from a given linearly ordered commutative semiring `α`, the inequality `2 * a * b ≤ a ^ 2 + b ^ 2` holds true. This theorem is an alias of `two_mul_le_add_sq`.

More concisely: For any two elements in a linearly ordered commutative semiring, their product is less than or equal to the sum of their squares. (Binary Arithmetic Mean-Geometric Mean Inequality)

mul_lt_of_one_lt_right

theorem mul_lt_of_one_lt_right : ∀ {α : Type u} [inst : StrictOrderedSemiring α] {a b : α} [inst_1 : ExistsAddOfLE α], a < 0 → 1 < b → a * b < a

This theorem, `mul_lt_of_one_lt_right`, states that for any strictly ordered semiring (a mathematical structure which is an ordered ring and a semiring, where the multiplication operation is compatible with the ordering), given two elements `a` and `b` and the existence of addition for any less than or equal to operation, if `a` is less than 0 and `b` is greater than 1, then the product of `a` and `b` is less than `a`.

More concisely: For any strictly ordered semiring, if `a` is negative and `b` is strictly greater than 1, then `a * b` is strictly less than `a`.

antitone_mul_left

theorem antitone_mul_left : ∀ {α : Type u} [inst : OrderedSemiring α] [inst_1 : ExistsAddOfLE α] [inst_2 : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α}, a ≤ 0 → Antitone fun x => a * x

The theorem `antitone_mul_left` states that for all types `α` that are ordered semirings (a structure that combines properties of rings and ordered groups), and for which there exists an additive operation compatible with a partial order, and for which the relation of being less than or equal to is contravariant with respect to addition, then for any element `a` of type `α` that is less than or equal to zero, the function that multiplies `a` by an input value `x` is an antitone function. In simpler terms, if `a` is less than or equal to zero in an ordered semiring, then multiplying by `a` reverses the order of elements: if `x ≤ y`, then `a*y ≤ a*x`.

More concisely: If `α` is an ordered semiring with an additive order compatible with multiplication such that `a ≤ 0` implies `a * x ≤ a * y` for all `x, y` in `α`, then `a * x ≤ a * y` implies `x ≤ y`.

le_iff_exists_nonneg_add

theorem le_iff_exists_nonneg_add : ∀ {α : Type u} [inst : OrderedSemiring α] [inst_1 : ExistsAddOfLE α] [inst_2 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a b : α), a ≤ b ↔ ∃ c ≥ 0, b = a + c

This theorem, `le_iff_exists_nonneg_add`, states that for all types `α` that are ordered semirings and support the existence of an additive operation satisfying the less than or equal to (`≤`) relation, and have a contravariant order-preserving addition operation, given any two elements `a` and `b` of type `α`, `a` is less than or equal to `b` if and only if there exists a non-negative `c` such that `b` is equal to the sum of `a` and `c`.

More concisely: For all ordered semirings `α` with a contravariant order-preserving addition and for all `a, b` in `α`, `a ≤ b` if and only if there exists a non-negative `c` such that `b = a + c`.

one_lt_mul

theorem one_lt_mul : ∀ {α : Type u} [inst : OrderedSemiring α] {a b : α}, 1 ≤ a → 1 < b → 1 < a * b

This is an alias of the theorem `one_lt_mul_of_le_of_lt`. The theorem `one_lt_mul` states that for any ordered semiring `α`, and any elements `a` and `b` of `α`, if `a` is greater than or equal to 1 and `b` is strictly greater than 1, then the product `a * b` is strictly greater than 1.

More concisely: In an ordered semiring, if 1 < a and 1 < b, then a * b > 1.

mul_add_mul_le_mul_add_mul

theorem mul_add_mul_le_mul_add_mul : ∀ {α : Type u} [inst : StrictOrderedSemiring α] {a b c d : α} [inst_1 : ExistsAddOfLE α], a ≤ b → c ≤ d → a * d + b * c ≤ a * c + b * d

This theorem is known as the binary **rearrangement inequality**. It's a statement in the field of ordered semirings. It says that for any strict ordered semiring `α`, given any four elements `a, b, c, d` in `α` such that `a` is less than or equal to `b` and `c` is less than or equal to `d`, the sum of the product of `a` and `d` and the product of `b` and `c` is less than or equal to the sum of the product of `a` and `c` and the product of `b` and `d`. In mathematical notation, if $a \leq b$ and $c \leq d$, then $a \cdot d + b \cdot c \leq a \cdot c + b \cdot d$.

More concisely: For any strict ordered semiring `α`, if `a ≤ b` and `c ≤ d` in `α`, then `a * d + b * c ≤ a * c + b * d`.

StrictOrderedSemiring.zero_le_one

theorem StrictOrderedSemiring.zero_le_one : ∀ {α : Type u} [self : StrictOrderedSemiring α], 0 ≤ 1

This theorem states that in any strict ordered semiring (which is a mathematical structure that extends a ring with a strict order relation that is compatible with the ring operations), the element `0` is less than or equal to the element `1`. This is a property that holds universally for all such semirings.

More concisely: In any strict ordered semiring, the additive identity (0) is less than or equal to the multiplicative identity (1).

Mathlib.Algebra.Order.Ring.Defs._auxLemma.3

theorem Mathlib.Algebra.Order.Ring.Defs._auxLemma.3 : ∀ {α : Type u} [inst : StrictOrderedSemiring α] {a : α}, 0 < a → ∀ (n : ℕ), (0 < a ^ n) = True

This theorem, from the `Mathlib.Algebra.Order.Ring.Defs._auxLemma.3`, states that for any strictly ordered semiring `α` and any element `a` from `α`, if `a` is greater than zero, then for any natural number `n`, `a` raised to the power of `n` is also greater than zero. In simpler terms, any positive number raised to any natural number power in a strictly ordered semiring will always yield a positive result.

More concisely: In a strictly ordered semiring, if 0 < a then a^n > 0 for all natural numbers n.

mul_max_of_nonneg

theorem mul_max_of_nonneg : ∀ {α : Type u} [inst : LinearOrderedSemiring α] {a : α} (b c : α), 0 ≤ a → a * max b c = max (a * b) (a * c) := by sorry

This theorem, named `mul_max_of_nonneg`, states that for any type `α` that has a structure of `LinearOrderedSemiring`, and for any nonnegative element `a` of this type, the product of `a` and the maximum of two elements `b` and `c` is equal to the maximum of the product of `a` and `b` and the product of `a` and `c`. In other words, if `a` is nonnegative, multiplication by `a` preserves the maximum operation. This is expressed in the language of the Lean 4 theorem prover.

More concisely: For any non-negative element `a` in a LinearOrderedSemiring `α`, and elements `b`, `c` in `α`, we have `a * (max b c) = max (a * b) (a * c)`.

mul_self_le_mul_self_iff

theorem mul_self_le_mul_self_iff : ∀ {α : Type u} [inst : LinearOrderedSemiring α] {a b : α}, 0 ≤ a → 0 ≤ b → (a ≤ b ↔ a * a ≤ b * b)

This theorem, `mul_self_le_mul_self_iff`, states that for any type `α` that is a linearly ordered semiring and for any two elements `a` and `b` of this type, if `a` and `b` are both non-negative, then `a` is less than or equal to `b` if and only if `a` squared (or `a * a`) is less than or equal to `b` squared (or `b * b`).

More concisely: For any linearly ordered semiring type `α` and elements `a, b` of type `α` that are non-negative, `a ≤ b` if and only if `a * a ≤ b * b`.

mul_nonneg_iff_pos_imp_nonneg

theorem mul_nonneg_iff_pos_imp_nonneg : ∀ {α : Type u} [inst : LinearOrderedSemiring α] {a b : α} [inst_1 : ExistsAddOfLE α], 0 ≤ a * b ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a)

This theorem states that for any type `α` which is a `LinearOrderedSemiring` and for any elements `a` and `b` of this type, the product `a * b` is non-negative if and only if the following two conditions are met: if `a` is positive then `b` is non-negative, and if `b` is positive then `a` is non-negative. Here, `LinearOrderedSemiring` is a mathematical structure with addition, multiplication, and an ordering that is compatible with these operations. The theorem requires the existence of an additive operation that can be applied when one element is less than or equal to another.

More concisely: For any `LinearOrderedSemiring` type `α` and elements `a, b` of `α`, the product `a * b` is non-negative if and only if `a` is non-negative when `b` is, and `b` is non-negative when `a` is.

StrictOrderedSemiring.mul_lt_mul_of_pos_right

theorem StrictOrderedSemiring.mul_lt_mul_of_pos_right : ∀ {α : Type u} [self : StrictOrderedSemiring α] (a b c : α), a < b → 0 < c → a * c < b * c

This theorem states that in any strictly ordered semiring `α`, if `a` is less than `b` and `c` is a positive element, then the result of multiplying `a` by `c` is less than the result of multiplying `b` by `c`. That is, right multiplication by a positive element preserves the order of the elements in a strictly ordered semiring.

More concisely: In a strictly ordered semiring, if $a < b$ and $c$ is positive, then $a \cdot c < b \cdot c$.

strictMono_mul_right_of_pos

theorem strictMono_mul_right_of_pos : ∀ {α : Type u} [inst : StrictOrderedSemiring α] {a : α}, 0 < a → StrictMono fun x => x * a

The theorem `strictMono_mul_right_of_pos` states that for any strictly ordered semiring `α` and any element `a` in `α`, if `a` is greater than 0, then the function that multiplies `x` by `a` is strictly monotone. In other words, for any two elements `b` and `c` in `α`, if `b` is less than `c`, then `b * a` is less than `c * a`.

More concisely: For any strictly ordered semiring `α` and element `a` in `α` with `0 < a`, the multiplication function `×` is strictly increasing: `(x₁ < x₂) → (x₁ * a < x₂ * a)`.

mul_lt_one_of_nonneg_of_lt_one_left

theorem mul_lt_one_of_nonneg_of_lt_one_left : ∀ {α : Type u} [inst : OrderedSemiring α] {a b : α}, 0 ≤ a → a < 1 → b ≤ 1 → a * b < 1

This theorem states that for any ordered semiring `α`, and any two elements `a` and `b` of `α`, if `a` is nonnegative and less than 1, and `b` is less than or equal to 1, then the product of `a` and `b` is less than 1. Intuitively, this reflects the idea that multiplying two values, both less than or equal to 1, gives a result that is also less than 1.

More concisely: For any ordered semiring `α`, if `a, b ∈ α` satisfy `0 ≤ a < 1` and `0 ≤ b ≤ 1`, then `a * b < 1`.

mul_le_mul_of_nonpos_right

theorem mul_le_mul_of_nonpos_right : ∀ {α : Type u} [inst : OrderedSemiring α] {a b c : α} [inst_1 : ExistsAddOfLE α] [inst_2 : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], b ≤ a → c ≤ 0 → a * c ≤ b * c

The theorem `mul_le_mul_of_nonpos_right` is a statement about ordered semirings. It says that for any type `α` which is an ordered semiring and for any elements `a`, `b`, and `c` of this type, if `b` is less than or equal to `a` and `c` is less than or equal to zero, then the product of `a` and `c` is less than or equal to the product of `b` and `c`. This can also be understood as: in an ordered semiring, if we multiply by a non-positive number, the order of multiplication is reversed.

More concisely: In an ordered semiring, if one multiplier is non-positive and the other is less than or equal to the first, then their product is less than or equal to the product of the smaller multiplier and the non-positive multiplier.

mul_lt_mul_of_neg_left

theorem mul_lt_mul_of_neg_left : ∀ {α : Type u} [inst : StrictOrderedSemiring α] {a b c : α} [inst_1 : ExistsAddOfLE α], b < a → c < 0 → c * a < c * b

This theorem, `mul_lt_mul_of_neg_left`, is applicable within the context of a `StrictOrderedSemiring` type (a type of algebraic structure that combines the properties of a ring and an ordered set, but without requiring the existence of additive inverses). It states that for any three elements `a`, `b`, and `c` of this type, if `b` is less than `a` and `c` is less than zero, then the product of `c` and `a` is less than the product of `c` and `b`. In simpler terms, it expresses the property that multiplying by a negative number reverses the order of inequality.

More concisely: For any `StrictOrderedSemiring` `a, b, c`, if `b < a` and `c < 0`, then `c * a < c * b`.

nonneg_of_mul_nonneg_right

theorem nonneg_of_mul_nonneg_right : ∀ {α : Type u} [inst : LinearOrderedSemiring α] {a b : α}, 0 ≤ a * b → 0 < a → 0 ≤ b

This theorem states that for any type `α` that is a linear ordered semiring, for any elements `a` and `b` of that type, if the product of `a` and `b` is nonnegative and `a` is positive then `b` must be nonnegative. In mathematical terms, `0 ≤ a * b` and `0 < a` implies `0 ≤ b` in the context of a linear ordered semiring.

More concisely: In a linear ordered semiring, if product of two positive elements is non-negative, then the second element is non-negative.

sq_nonneg

theorem sq_nonneg : ∀ {α : Type u} [inst : LinearOrderedSemiring α] [inst_1 : ExistsAddOfLE α] (a : α), 0 ≤ a ^ 2 := by sorry

This theorem, `sq_nonneg`, states that for any type `α` that is a linear ordered semiring (a mathematical structure that combines properties of order and operations addition and multiplication) and for which there exists an addition operation that respects the order (`ExistsAddOfLE α`), the square of any element `a` from that type is always nonnegative, i.e., greater than or equal to zero. In mathematical notation, this can be expressed as ∀a ∈ α, 0 ≤ a^2.

More concisely: For any linear ordered semiring `α` with respect to an order-preserving addition, every element `a` in `α` satisfies `0 ≤ a^2`.

OrderedRing.add_le_add_left

theorem OrderedRing.add_le_add_left : ∀ {α : Type u} [self : OrderedRing α] (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b

This theorem states that in an ordered ring, where addition is commutative, the operation of addition is monotone. That is, for any elements `a` and `b` in the ring, if `a` is less than or equal to `b`, then adding any element `c` to `a` will result in a sum that is less than or equal to the sum of `c` and `b`. This principle is true for all elements in the given ordered ring.

More concisely: In an ordered commutative ring, the operation of addition is monotonic, that is, for all elements `a` and `b` with `a ≤ b`, it holds that `a + c ≤ b + c` for all `c`.

mul_add_mul_lt_mul_add_mul

theorem mul_add_mul_lt_mul_add_mul : ∀ {α : Type u} [inst : StrictOrderedSemiring α] {a b c d : α} [inst_1 : ExistsAddOfLE α], a < b → c < d → a * d + b * c < a * c + b * d

This theorem is known as the binary strict rearrangement inequality. It states that for any strict ordered semiring `α` and any four elements `a`, `b`, `c`, and `d` from `α`, if `a` is less than `b` and `c` is less than `d`, then the sum of `a` multiplied by `d` and `b` multiplied by `c` is less than the sum of `a` multiplied by `c` and `b` multiplied by `d`. This inequality provides an ordering rule for products in the context of an ordered semiring.

More concisely: In a strict ordered semiring, for elements a < b and c < d, we have a * d + b * c < a * c + b * d.

pow_pos

theorem pow_pos : ∀ {α : Type u} [inst : StrictOrderedSemiring α] {a : α}, 0 < a → ∀ (n : ℕ), 0 < a ^ n

This theorem states that for all types `α` that are strict ordered semi-rings, if `a` is an element of `α` and is greater than 0, then any natural number power of `a` (expressed as `a ^ n` where `n` is a natural number) is also greater than 0. In LaTeX, this would be expressed as: For all $a \in \alpha$, where $\alpha$ is a strict ordered semi-ring, if $a > 0$, then for all $n \in \mathbb{N}$, $a^n > 0$.

More concisely: In a strict ordered semi-ring $\alpha$, if $00$ for all natural numbers $n$.

StrictOrderedSemiring.mul_lt_mul_of_pos_left

theorem StrictOrderedSemiring.mul_lt_mul_of_pos_left : ∀ {α : Type u} [self : StrictOrderedSemiring α] (a b c : α), a < b → 0 < c → c * a < c * b

This theorem states that in a `StrictOrderedSemiring` (which is a semiring with a strict total order that is compatible with the operations), for any three elements `a`, `b` and `c`, if `a` is less than `b` and `c` is positive, then the product of `c` and `a` is less than the product of `c` and `b`. In other words, left multiplication by a positive element preserves the order. The type `α` is presumed to be a `StrictOrderedSemiring`.

More concisely: In a strict ordered semiring, if `a` is less than `b` and `c` is positive, then `c * a` is less than `c * b`.

LinearOrderedSemiring.compare_eq_compareOfLessAndEq

theorem LinearOrderedSemiring.compare_eq_compareOfLessAndEq : ∀ {α : Type u} [self : LinearOrderedSemiring α] (a b : α), compare a b = compareOfLessAndEq a b

This theorem states that for any type `α` that forms a linear ordered semiring, and for any two elements `a` and `b` of this type, the comparison operation `compare a b` is equivalent to the operation `compareOfLessAndEq a b`. Here, `compareOfLessAndEq a b` differentiates three possible orderings: `a` is less than `b` (Ordering.lt), `a` is equal to `b` (Ordering.eq), and `a` is greater than `b` (Ordering.gt), based on decidable properties of less than `<` and equals `=` operations.

More concisely: For any linear ordered semiring type `α`, the comparison operation `compare a b` is equivalent to the order relation `Ordering.lt a b.or (Ordering.eq a b)` in Lean.

zero_lt_mul_right

theorem zero_lt_mul_right : ∀ {α : Type u_1} {a b : α} [inst : MulZeroClass α] [inst_1 : Preorder α] [inst_2 : MulPosStrictMono α] [inst_3 : MulPosReflectLT α], 0 < b → (0 < a * b ↔ 0 < a)

This theorem, referred to as `zero_lt_mul_right`, states that for any type `α` that has multiplication and zero, and that is both strictly monotonically increasing and strictly reverse monotonically decreasing when multiplied by a positive number on the right, and for any two elements `a` and `b` of this type, if `b` is greater than zero, then `a` is greater than zero if and only if (`iff`) the product of `a` and `b` is greater than zero. In other words, `0 < a * b` is true if and only if `0 < a` is true under the given conditions. The theorem asserts that the positivity of `a` is preserved when it is multiplied by a positive number `b`.

More concisely: For any type with multiplication and zero that is strictly monotonically increasing and strictly reverse monotonically decreasing when multiplied by a positive number on the right, the product of two positive elements is positive.

mul_lt_mul''

theorem mul_lt_mul'' : ∀ {α : Type u} [inst : StrictOrderedSemiring α] {a b c d : α}, a < c → b < d → 0 ≤ a → 0 ≤ b → a * b < c * d := by sorry

This theorem states that for any strictly ordered semiring `α`, given four elements `a`, `b`, `c`, and `d` from `α` where `a` is less than `c` and `b` is less than `d`, and both `a` and `b` are non-negative, then the product of `a` and `b` is less than the product of `c` and `d`.

More concisely: For any strictly ordered semiring `α`, if `a`, `b`, `c`, and `d` are elements of `α` with `a < c`, `b < d`, and `a`, `b` non-negative, then `a * b < c * d`.

LinearOrderedCommSemiring.max_def

theorem LinearOrderedCommSemiring.max_def : ∀ {α : Type u_2} [self : LinearOrderedCommSemiring α] (a b : α), max a b = if a ≤ b then b else a

This theorem states that for any type `α` that is a Linear Ordered Commutative Semiring, the maximum of two elements `a` and `b` is defined as `b` if `a` is less than or equal to `b`, else it's `a`. In other words, the definition of the maximum function in this context is equivalent to the one you get from 'maxOfLe' condition.

More concisely: For any Linear Ordered Commutative Semiring type `α`, the maximum of `a` and `b` is `a` if `a` ≤ `b`, otherwise it is `b`.

mul_self_pos

theorem mul_self_pos : ∀ {α : Type u} [inst : LinearOrderedSemiring α] [inst_1 : ExistsAddOfLE α] {a : α}, 0 < a * a ↔ a ≠ 0

This theorem states that for any type `α` that is a linear ordered semiring and supports the existence of an addition operation for less than or equal to comparisons, the square of any instance `a` from this type is greater than zero if and only if `a` is not equal to zero. In mathematical terms, for any `a` in a linear ordered semiring, 0 < a² if and only if `a` ≠ 0.

More concisely: In a linear ordered semiring, the square of any non-zero element is positive.

mul_nonneg_iff_of_pos_left

theorem mul_nonneg_iff_of_pos_left : ∀ {α : Type u} [inst : LinearOrderedSemiring α] {b c : α}, 0 < c → (0 ≤ c * b ↔ 0 ≤ b)

This theorem states that for any type `α` which is a `LinearOrderedSemiring`, and for any instances `b` and `c` of this type, if `c` is greater than 0, then `c * b` is non-negative if and only if `b` is non-negative. Essentially, this is stating that in a linear ordered semiring, positive numbers preserve the non-negativity when they multiply other numbers.

More concisely: In a LinearOrderedSemiring, for all `α`, `c` (with `c > 0`), `c * b` is non-negative if and only if `b` is non-negative.

sub_one_lt

theorem sub_one_lt : ∀ {α : Type u} [inst : LinearOrderedRing α] (a : α), a - 1 < a

This theorem states that for any type `α` that has an instance of `LinearOrderedRing`, subtracting one from any element `a` of that type will always result in a value that is less than `a`. In terms of traditional mathematical notation, this is equivalent to the statement ∀a ∈ α, a - 1 < a.

More concisely: For all `α` with `LinearOrderedRing`, for all `a` in `α`, `a` > `a` - 1. (This is the negative of the original statement, as Lean uses the convention that `x < y` is the same as `-y < x` in its order theory.)

StrictOrderedRing.mul_pos

theorem StrictOrderedRing.mul_pos : ∀ {α : Type u} [self : StrictOrderedRing α] (a b : α), 0 < a → 0 < b → 0 < a * b

This theorem states that in any strict ordered ring (a mathematical structure where addition, subtraction, multiplication are defined and an order relation is present), the product of two positive elements is positive. Given any two positive elements `a` and `b` in such a ring, if `a` is greater than zero and `b` is greater than zero, then their product `a * b` is also greater than zero.

More concisely: In a strict ordered ring, the product of two positive elements is positive.

Mathlib.Algebra.Order.Ring.Defs._auxLemma.27

theorem Mathlib.Algebra.Order.Ring.Defs._auxLemma.27 : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α}, (0 ≤ -a) = (a ≤ 0)

This theorem, labelled as `Mathlib.Algebra.Order.Ring.Defs._auxLemma.27` in Lean 4, states that for any type `α` that has an addition group structure and an order relation, and the addition operation is covariant with respect to this order, then for any element 'a' of this type, the inequality '0 is less than or equal to negative a' is equivalent to the inequality 'a is less than or equal to 0'. In other words, an element is non-positive if and only if its negation is non-negative.

More concisely: For any type endowed with an additive structure and a compatible order relation, the element 'a' is non-positive if and only if -'a' is non-negative.

mul_lt_of_one_lt_left

theorem mul_lt_of_one_lt_left : ∀ {α : Type u} [inst : StrictOrderedSemiring α] {a b : α} [inst_1 : ExistsAddOfLE α], b < 0 → 1 < a → a * b < b

This theorem, `mul_lt_of_one_lt_left`, states that for any strict ordered semiring `α` and any two elements `a` and `b` of `α` where an addition operation is defined for elements that are less than or equal to each other, if `b` is less than zero and `a` is greater than one, then the product of `a` and `b` is less than `b`. Essentially, it's a variant of the `lt_mul_of_one_lt_left` theorem, but specifically for the case when `b` is negative instead of positive.

More concisely: If `α` is a strict ordered semiring with additions defined for elements that are less than or equal to each other, and `a > 1` and `b < 0` in `α`, then `a * b < b`.

nonneg_le_nonneg_of_sq_le_sq

theorem nonneg_le_nonneg_of_sq_le_sq : ∀ {α : Type u} [inst : LinearOrderedSemiring α] {a b : α}, 0 ≤ b → a * a ≤ b * b → a ≤ b

This theorem, `nonneg_le_nonneg_of_sq_le_sq`, states that for any type `α` that is a linear ordered semiring, given two elements `a` and `b` from `α` where `b` is non-negative (i.e., `0 ≤ b`), if the square of `a` is less than or equal to the square of `b` (i.e., `a * a ≤ b * b`), then `a` is less than or equal to `b`. In mathematical terms, $\forall a, b \in \alpha, 0 \leq b \land a^2 \leq b^2 \rightarrow a \leq b$.

More concisely: If `α` is a linear ordered semiring, `b` is non-negative in `α`, and `a^2 ≤ b^2` holds, then `a ≤ b`.

LinearOrderedRing.le_total

theorem LinearOrderedRing.le_total : ∀ {α : Type u} [self : LinearOrderedRing α] (a b : α), a ≤ b ∨ b ≤ a

This theorem states that for any type `α` which has a structure of a `LinearOrderedRing`, 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 linearly ordered ring, any two elements are comparable, ensuring the property of total order.

More concisely: In a linearly ordered ring, every two elements are comparable.

mul_le_mul_of_nonpos_left

theorem mul_le_mul_of_nonpos_left : ∀ {α : Type u} [inst : OrderedSemiring α] {a b c : α} [inst_1 : ExistsAddOfLE α] [inst_2 : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], b ≤ a → c ≤ 0 → c * a ≤ c * b

The theorem `mul_le_mul_of_nonpos_left` states that for any ordered semiring `α`, if `b` is less than or equal to `a` and `c` is less than or equal to `0`, then the product `c * a` is less than or equal to the product `c * b`. It is important to have the property `ExistsAddOfLE α`, which ensures the existence of addition operation satisfying certain properties. Also, the contravariant property is required which states that if `x + y` is less than `x + z` for all `y` and `z`, then `y` is less than `z` in `α`.

More concisely: For any ordered semiring `α` with `ExistsAddOfLE` and the contravariant property, if `c ≤ 0`, `b ≤ a`, then `c * a ≤ c * b`.

LinearOrderedRing.min_def

theorem LinearOrderedRing.min_def : ∀ {α : Type u} [self : LinearOrderedRing α] (a b : α), min a b = if a ≤ b then a else b

This theorem states that for any linear ordered ring, the minimum function for any two elements (a and b) is equivalent to using a conditional statement that checks if a is less than or equal to b. If a is less than or equal to b, then the minimum is a; otherwise, the minimum is b. In mathematical terms, for all α being an instance of a linear ordered ring, min(a, b) is the same as the result of the conditional 'if a ≤ b then a else b'.

More concisely: For any linear ordered ring, the minimum of two elements a and b is equivalent to the conditional expression if a <= b then a else b.

LinearOrderedRing.max_def

theorem LinearOrderedRing.max_def : ∀ {α : Type u} [self : LinearOrderedRing α] (a b : α), max a b = if a ≤ b then b else a

This theorem states that for any two elements `a` and `b` from a linearly ordered ring `α`, the maximum of `a` and `b` can be defined using the conditional `if-then-else` construct. Specifically, it says that the maximum of `a` and `b` is `b` if `a` is less than or equal to `b`, else it is `a`. This provides an alternative definition of the maximum function in the context of a linearly ordered ring.

More concisely: For any two elements `a` and `b` in a linearly ordered ring, the maximum `max a b` is defined as `if a <= b then b else a`.

OrderedCommRing.mul_comm

theorem OrderedCommRing.mul_comm : ∀ {α : Type u} [self : OrderedCommRing α] (a b : α), a * b = b * a

This theorem states that for any ordered commutative ring, given any two elements 'a' and 'b' in that ring, the result of multiplying 'a' by 'b' is the same as the result of multiplying 'b' by 'a'. This property is known as the commutativity of multiplication. In more formal mathematical terms, `∀ a b ∈ α, a * b = b * a`, where α is a commutative multiplicative magma (which in this case, is an ordered commutative ring).

More concisely: In any commutative ring, multiplication is commutative: for all elements a and b, a * b = b * a.

mul_nonneg_of_nonpos_of_nonpos

theorem mul_nonneg_of_nonpos_of_nonpos : ∀ {α : Type u} [inst : OrderedSemiring α] {a b : α} [inst_1 : ExistsAddOfLE α] [inst_2 : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a ≤ 0 → b ≤ 0 → 0 ≤ a * b

The theorem `mul_nonneg_of_nonpos_of_nonpos` asserts that for any ordered semiring `α`, if elements `a` and `b` of `α` are nonpositive (i.e., `a` and `b` are both less than or equal to zero), then the product of `a` and `b` is nonnegative (i.e., greater than or equal to zero). This is a generalization of the familiar fact from basic algebra that the product of two negative numbers is a nonnegative number. The proof relies on the existence of addition for elements less than or equal to each other and a contravariant class of binary functions on `α` that swaps the order of addition and verifies the inequality.

More concisely: If `α` is an ordered semiring and `a` and `b` are its elements that are less than or equal to zero, then the product `a * b` is greater than or equal to zero.

antitone_mul_right

theorem antitone_mul_right : ∀ {α : Type u} [inst : OrderedSemiring α] [inst_1 : ExistsAddOfLE α] [inst_2 : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α}, a ≤ 0 → Antitone fun x => x * a

The theorem `antitone_mul_right` states that for any ordered semiring `α`, assuming an additive identity for any element less than or equal to another, and having a contravariant class with respect to the swapped addition operation and the standard less than or equal operation, for any `a` in `α`, if `a` is less than or equal to zero then multiplication by `a` is an antitone function. In other words, if `a` is less than or equal to zero in an ordered semiring, then for any two elements `x` and `y` in `α`, if `x` is less than or equal to `y` then `y * a` is less than or equal to `x * a`.

More concisely: If `α` is an ordered semiring with `a ≤ 0`, then for all `x, y ∈ α`, `x ≤ y` implies `y * a ≤ x * a`.

le_mul_of_le_one_left

theorem le_mul_of_le_one_left : ∀ {α : Type u} [inst : OrderedSemiring α] {a b : α} [inst_1 : ExistsAddOfLE α] [inst_2 : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], b ≤ 0 → a ≤ 1 → b ≤ a * b

This theorem, `le_mul_of_le_one_left`, states that for any ordered semi-ring `α`, given elements `a` and `b` of `α`, such that `b` is less than or equal to zero and `a` is less than or equal to one, then `b` is also less than or equal to the product of `a` and `b`. This is essentially a variant of the `mul_le_of_le_one_left` theorem where `b` is non-positive instead of non-negative. The `ContravariantClass` instance is used here to ensure the order relationship under addition operation is preserved.

More concisely: For any ordered semi-ring `α`, if `0 ≤ b` and `0 ≤ a ≤ 1`, then `a * b ≤ b`.

monotone_mul_right_of_nonneg

theorem monotone_mul_right_of_nonneg : ∀ {α : Type u} [inst : OrderedSemiring α] {a : α}, 0 ≤ a → Monotone fun x => x * a

This theorem, `monotone_mul_right_of_nonneg`, states that for any type `α` endowed with an ordered semiring structure and any nonnegative element `a` of type `α`, the function that multiplies `x` by `a` is monotone. In other words, if `0 ≤ a`, then for any `x` and `y` of type `α` where `x ≤ y`, it follows that `x * a ≤ y * a`.

More concisely: For any ordered semiring `α` and non-negative element `a` in `α`, the multiplication function `x => x * a` is monotone.

mul_lt_one_of_nonneg_of_lt_one_right

theorem mul_lt_one_of_nonneg_of_lt_one_right : ∀ {α : Type u} [inst : OrderedSemiring α] {a b : α}, a ≤ 1 → 0 ≤ b → b < 1 → a * b < 1

This theorem states that for any ordered semiring `α`, given two elements `a` and `b` from `α`, if `a` is less than or equal to 1, `b` is non-negative (greater than or equal to 0), and `b` is less than 1, then the product of `a` and `b` is less than 1. This theorem essentially captures the property that in an ordered semiring, the product of a number less than or equal to 1 and a positive number less than 1 is itself less than 1.

More concisely: In an ordered semiring, if `0 ≤ a ≤ 1` and `0 ≤ b < 1`, then `a * b < 1`.

mul_add_mul_lt_mul_add_mul'

theorem mul_add_mul_lt_mul_add_mul' : ∀ {α : Type u} [inst : StrictOrderedSemiring α] {a b c d : α} [inst_1 : ExistsAddOfLE α], b < a → d < c → a * d + b * c < a * c + b * d

This theorem is the binary version of the rearrangement inequality. Given a strict ordered semiring (a number system that supports addition, multiplication, and a strict total order), and elements `a`, `b`, `c`, `d` from that semiring, it states that if `b` is less than `a`, and `d` is less than `c`, then the sum of `a` multiplied by `d` and `b` multiplied by `c` is less than the sum of `a` multiplied by `c` and `b` multiplied by `d`.

More concisely: In a strict ordered semiring, if $a \geq b$ and $c \geq d$, then $ac + bd \leq ad + bc$.

zero_lt_mul_left

theorem zero_lt_mul_left : ∀ {α : Type u_1} {a b : α} [inst : MulZeroClass α] [inst_1 : Preorder α] [inst_2 : PosMulStrictMono α] [inst_3 : PosMulReflectLT α], 0 < a → (0 < a * b ↔ 0 < b)

This theorem, `zero_lt_mul_left`, states that for any type `α` that has a multiplication operation, a zero element, and an ordering operation satisfying the properties of a `MulZeroClass`, a `Preorder`, `PosMulStrictMono` and `PosMulReflectLT`, if a certain element `a` is positive (greater than zero), then the product of `a` and another element `b` is positive if and only if `b` itself is positive. This property, also known as the "Alias of `mul_pos_iff_of_pos_left`", represents the mathematical concept that the product of two positive numbers in an ordered semiring is positive.

More concisely: For any type `α` with a multiplication, zero, ordering, and the given properties, if `a` is positive and `b` is non-negative, then `a * b` is positive.

StrictOrderedRing.zero_le_one

theorem StrictOrderedRing.zero_le_one : ∀ {α : Type u} [self : StrictOrderedRing α], 0 ≤ 1

This theorem states that in any strict ordered ring, the number 0 is less than or equal to the number 1. A strict ordered ring is a ring with a specified total order that is compatible with the ring operations, where the multiplicative identity (1) is strictly greater than the additive identity (0).

More concisely: In a strict ordered ring, 0 ≤ 1.

LinearOrderedSemiring.le_total

theorem LinearOrderedSemiring.le_total : ∀ {α : Type u} [self : LinearOrderedSemiring α] (a b : α), a ≤ b ∨ b ≤ a := by sorry

This theorem states that for any linear ordered semiring (a structure that combines the properties of a semiring and a linear order) the order relation is total. In simpler terms, given any two elements `a` and `b` in this structure, either `a` is less than or equal to `b` or `b` is less than or equal to `a`. This property is one of the defining characteristics of a total order.

More concisely: In a linear ordered semiring, the relation is a total order.

le_mul_of_le_one_right

theorem le_mul_of_le_one_right : ∀ {α : Type u} [inst : OrderedSemiring α] {a b : α} [inst_1 : ExistsAddOfLE α] [inst_2 : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a ≤ 0 → b ≤ 1 → a ≤ a * b

This theorem, `le_mul_of_le_one_right`, is a variant of `mul_le_of_le_one_right` but for non-positive values of `a` rather than non-negative. It applies to any ordered semiring `α`. Given two elements `a` and `b` of this semiring, it states that if `a` is less than or equal to 0 and `b` is less than or equal to 1, then `a` is less than or equal to the product of `a` and `b`. It also requires two additional properties. First, that there exists an `add` operation for elements of type `α` that are less than or equal to each other. Second, that the semiring `α` is a contravariant class with respect to the swapped addition operation and the less than or equal relation.

More concisely: If `α` is an ordered semiring with the property that `a ≤ b` implies `a + c ≤ b + c` for all `a`, `b`, and `c`, and `a ≤ 0` and `0 ≤ b`, then `a ≤ a * b`.

mul_pos_iff

theorem mul_pos_iff : ∀ {α : Type u} [inst : LinearOrderedSemiring α] {a b : α} [inst_1 : ExistsAddOfLE α], 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

This theorem, `mul_pos_iff`, states a property for any linearly ordered semiring. Specifically, for any two elements `a` and `b` from the semiring, the product `a * b` is positive if and only if either both `a` and `b` are positive or both `a` and `b` are negative. This is a basic property of multiplication in ordered rings.

More concisely: In a linearly ordered semiring, the product of two elements is positive if and only if both elements are positive or both are negative.

pow_nonneg

theorem pow_nonneg : ∀ {α : Type u} [inst : OrderedSemiring α] {a : α}, 0 ≤ a → ∀ (n : ℕ), 0 ≤ a ^ n

This theorem states that for any ordered semiring `α`, any non-negative element `a` of `α`, and any natural number `n`, the `n`th power of `a` is also non-negative. In other words, it generalizes the familiar fact from arithmetic that the product of any number of non-negative numbers is itself non-negative. It is valid in any context where a semiring structure is assumed, which includes many structures in abstract algebra and number theory.

More concisely: For any ordered semiring `α` and non-negative element `a` in `α`, the `n`th power `a^n` is also non-negative.

LinearOrderedSemiring.min_def

theorem LinearOrderedSemiring.min_def : ∀ {α : Type u} [self : LinearOrderedSemiring α] (a b : α), min a b = if a ≤ b then a else b

This theorem states that for any type `α` that is a linear ordered semiring, and for any two elements `a` and `b` of `α`, the minimum of `a` and `b` is equivalent to choosing `a` if `a` is less than or equal to `b`, else choosing `b`. In other words, the minimum function in a linear ordered semiring 'α' is defined as being equivalent to the function `minOfLe` which selects the smaller of two elements based on the condition of one being less than or equal to the other.

More concisely: For any linear ordered semiring `α`, the minimum `a ⊓ b` of two elements `a` and `b` is equivalent to `if a ≤ b then a else b`.

monotone_mul_left_of_nonneg

theorem monotone_mul_left_of_nonneg : ∀ {α : Type u} [inst : OrderedSemiring α] {a : α}, 0 ≤ a → Monotone fun x => a * x

The theorem `monotone_mul_left_of_nonneg` states that for any type `α` that has an ordered semiring structure, for any element `a` of type `α` which is nonnegative (i.e., `0 ≤ a`), the function which multiplies `a` to the left is monotone. In other words, if `a` is a nonnegative number in an ordered semiring, then for any two elements `b` and `c` of the semiring, if `b ≤ c` then `a * b ≤ a * c`.

More concisely: For any non-negative element `a` in an ordered semiring `α`, the multiplication-by-`a` function is monotone, that is, `a * b ≤ a * c` for all `b ≤ c` in `α`.

lt_mul_of_lt_one_right

theorem lt_mul_of_lt_one_right : ∀ {α : Type u} [inst : StrictOrderedSemiring α] {a b : α} [inst_1 : ExistsAddOfLE α], a < 0 → b < 1 → a < a * b

This theorem, named `lt_mul_of_lt_one_right`, states that for any strictly ordered semiring `α` and any two elements `a` and `b` of `α`, if `a` is less than zero and `b` is less than one, then `a` is less than the product of `a` and `b`. In mathematical terms, this can be written as: for all `a`, `b` in `α`, if `a < 0` and `b < 1`, then `a < a * b`.

More concisely: If `α` is a strictly ordered semiring, and `a` and `b` are elements of `α` with `a < 0` and `b < 1`, then `a < a * b`.

zero_le_mul_left

theorem zero_le_mul_left : ∀ {α : Type u} [inst : LinearOrderedSemiring α] {b c : α}, 0 < c → (0 ≤ c * b ↔ 0 ≤ b) := by sorry

This theorem, `zero_le_mul_left`, states that for any type `α` which is an instance of `LinearOrderedSemiring`, given any two elements `b` and `c` of this type, if `c` is strictly greater than zero, then `c` times `b` is non-negative if and only if `b` itself is non-negative. In other words, multiplying a non-negative number by a positive number doesn't change the sign. This theorem is an alias of `mul_nonneg_iff_of_pos_left`.

More concisely: For any type `α` being a LinearOrderedSemiring, `b` and `c` elements of `α` with `c` positive, `b ≥ 0` if and only if `c * b ≥ 0`.

mul_self_nonneg

theorem mul_self_nonneg : ∀ {α : Type u} [inst : LinearOrderedSemiring α] [inst_1 : ExistsAddOfLE α] (a : α), 0 ≤ a * a

This theorem states that for any type `α` that has a structure of a linearly ordered semiring (a mathematical structure that combines the properties of an ordered ring and a semiring), and in which addition operation is defined for elements that satisfy less than or equal to relation, the square of any element `a` (represented as `a * a`) is always non-negative (greater than or equal to 0).

More concisely: For any linearly ordered semiring type `α` with non-negative addition, the square of any element `a` in `α` is non-negative (i.e., `a * a ≥ 0`).

bit0_lt_bit0

theorem bit0_lt_bit0 : ∀ {α : Type u} [inst : LinearOrderedSemiring α] {a b : α}, bit0 a < bit0 b ↔ a < b

This theorem, called `bit0_lt_bit0`, states that for any type `α` that forms a linear ordered semiring, given any two elements `a` and `b` of type `α`, the bit doubling function `bit0` applied to `a` is less than `bit0` applied to `b` if and only if `a` is less than `b`. The `bit0` function is defined as `bit0 a = a + a`, meaning that it doubles its input. Therefore, this theorem essentially asserts that the relation of less than (`<`) is preserved under the operation of doubling elements in an ordered semiring.

More concisely: For any linear ordered semiring type `α`, the relation `a < b` holds if and only if `bit0 a < bit0 b`, where `bit0 a = a + a`.

LinearOrderedCommSemiring.le_total

theorem LinearOrderedCommSemiring.le_total : ∀ {α : Type u_2} [self : LinearOrderedCommSemiring α] (a b : α), a ≤ b ∨ b ≤ a

This theorem states that for any type `α` that is a linearly ordered commutative semiring, for any two elements `a` and `b` of that type, either `a` is less than or equal to `b`, or `b` is less than or equal to `a`. This property is what makes the order "total" or "linear" - every pair of elements is comparable.

More concisely: For any linearly ordered commutative semiring type `α`, every pair of its elements `a` and `b` satisfies `a ≤ b` or `b ≤ a`.

mul_pos_of_neg_of_neg

theorem mul_pos_of_neg_of_neg : ∀ {α : Type u} [inst : StrictOrderedSemiring α] [inst_1 : ExistsAddOfLE α] {a b : α}, a < 0 → b < 0 → 0 < a * b

This theorem states that for any type `α` that is a strictly ordered semiring (a mathematical structure with two operations, addition and multiplication, satisfying certain properties such as associativity, commutativity, and distributivity) and supports the existence of an addition operation for any two elements where one is less than or equal to the other, if `a` and `b` are two elements of `α` such that both `a` and `b` are less than zero, then the product of `a` and `b` is greater than zero. In other words, it asserts that the product of two negative numbers is positive in any strictly ordered semiring where addition of elements obeying a certain inequality is defined.

More concisely: In a strictly ordered semiring, the product of two negative elements is positive.

LinearOrderedCommSemiring.min_def

theorem LinearOrderedCommSemiring.min_def : ∀ {α : Type u_2} [self : LinearOrderedCommSemiring α] (a b : α), min a b = if a ≤ b then a else b

This theorem states that for any type `α` that is a `LinearOrderedCommSemiring` (a semiring, i.e., a set equipped with two binary operations satisfying certain axioms, that is also linearly ordered), the minimum function `min` for any two elements `a` and `b` of type `α` behaves in the same way as a function defined as returning `a` when `a` is less than or equal to `b` and `b` otherwise.

More concisely: For any linearly ordered semiring `α`, the function `min` on `α` equals the function `if hle a b then a else b`, where `hle` is the relation of `α` being less than or equal to.

strictMono_mul_left_of_pos

theorem strictMono_mul_left_of_pos : ∀ {α : Type u} [inst : StrictOrderedSemiring α] {a : α}, 0 < a → StrictMono fun x => a * x

The theorem `strictMono_mul_left_of_pos` states that for any strictly ordered semiring `α` and any element `a` of `α`, if `a` is greater than zero, then the function that maps `x` to `a * x` is strictly monotone. In other words, if `a` is a positive element of a strictly ordered semiring, then multiplication by `a` preserves the order of elements: if `x` is less than `y`, then `a * x` is less than `a * y`.

More concisely: For any strictly ordered semiring `α` and positive element `a` in `α`, the function `x ↔ a * x` is strictly increasing.

mul_nonneg_of_three

theorem mul_nonneg_of_three : ∀ {α : Type u} [inst : LinearOrderedSemiring α] [inst_1 : ExistsAddOfLE α] (a b c : α), 0 ≤ a * b ∨ 0 ≤ b * c ∨ 0 ≤ c * a

This theorem states that in any linearly ordered semiring, given any three elements `a`, `b`, and `c`, at least one pair of them must have a product that is non-negative (greater than or equal to zero). In other words, either `a * b`, `b * c`, or `c * a` must be non-negative.

More concisely: In a linearly ordered semiring, the product of at least two elements is non-negative for some pair.

mul_add_mul_le_mul_add_mul'

theorem mul_add_mul_le_mul_add_mul' : ∀ {α : Type u} [inst : StrictOrderedSemiring α] {a b c d : α} [inst_1 : ExistsAddOfLE α], b ≤ a → d ≤ c → a * d + b * c ≤ a * c + b * d

This is a theorem about the **binary rearrangement inequality** in the context of a strictly ordered semiring. Given any four elements `a`, `b`, `c`, and `d` from a type `α` which is a strictly ordered semiring, if `b` is less than or equal to `a` and `d` is less than or equal to `c`, then the inequality `a * d + b * c ≤ a * c + b * d` holds true. The inequality basically suggests the rearrangement of terms in such a way that the sum of the products of the greater and lesser values does not exceed the sum of the products of the corresponding elements.

More concisely: In a strictly ordered semiring, for all `a`, `b`, `c`, `d`: `a ≥ b` and `c ≥ d` imply `a * d + b * c ≤ a * c + b * d`.

OrderedRing.mul_nonneg

theorem OrderedRing.mul_nonneg : ∀ {α : Type u} [self : OrderedRing α] (a b : α), 0 ≤ a → 0 ≤ b → 0 ≤ a * b

This theorem states that in any ordered ring (a mathematical structure that combines the properties of a ring and a partial order in a compatible way), the product of two non-negative elements is always non-negative. Here, the non-negativity of elements `a` and `b` is defined in terms of the partial order: an element is non-negative if it is greater than or equal to zero. Therefore, given two elements `a` and `b` of the ordered ring `α`, if both `a` and `b` are non-negative (i.e., `0 ≤ a` and `0 ≤ b`), then their product `a * b` is also non-negative (i.e., `0 ≤ a * b`).

More concisely: In any ordered ring, the product of two non-negative elements is non-negative.

mul_le_of_one_le_right

theorem mul_le_of_one_le_right : ∀ {α : Type u} [inst : OrderedSemiring α] {a b : α} [inst_1 : ExistsAddOfLE α] [inst_2 : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a ≤ 0 → 1 ≤ b → a * b ≤ a

This theorem states that for a given type `α` that forms an ordered semiring and supports the existence of addition for elements that satisfy the less than or equal to relation, if `a` and `b` are elements of `α` and if the type `α` also satisfies the condition that swapping arguments in addition function yields a function for which if one argument is more, the result is less (`ContravariantClass`), then if `a` is less than or equal to zero and `b` is greater than or equal to one, the product of `a` and `b` is less than or equal to `a`. In mathematical terms, `mul_le_of_one_le_right` is stating that for any ordered semiring, if `a` ≤ 0 and 1 ≤ `b`, then `a*b` ≤ `a`.

More concisely: For any ordered semiring, if `a` is less than or equal to zero and `b` is greater than or equal to one, then `a * b` is less than or equal to `a`.

mul_nonneg_iff

theorem mul_nonneg_iff : ∀ {α : Type u} [inst : LinearOrderedSemiring α] {a b : α} [inst_1 : ExistsAddOfLE α], 0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

This theorem states that for any type `α` that is a linearly ordered semiring, and any `a` and `b` of type `α`, the product `a * b` is non-negative if and only if either both `a` and `b` are non-negative or both `a` and `b` are non-positive. Here, non-negative and non-positive are represented by `0 ≤ a` and `0 ≤ b`, and `a ≤ 0` and `b ≤ 0`, respectively. The existence of an addition operation for the semiring `α` that respects order (denoted by `[inst_1 : ExistsAddOfLE α]`) is assumed.

More concisely: For any linearly ordered semiring `α` with addition respecting order, the product of two elements `a` and `b` is non-negative (`0 ≤ a * b`) if and only if both `a` and `b` are non-negative (`0 ≤ a` and `0 ≤ b`) or both are non-positive (`a ≤ 0` and `b ≤ 0`).

mul_le_of_one_le_left

theorem mul_le_of_one_le_left : ∀ {α : Type u} [inst : OrderedSemiring α] {a b : α} [inst_1 : ExistsAddOfLE α] [inst_2 : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], b ≤ 0 → 1 ≤ a → a * b ≤ b

The given theorem, `mul_le_of_one_le_left`, states that for any ordered semiring `α` and any elements `a` and `b` of `α`, where `b` is less than or equal to zero and `a` is greater than or equal to 1, then the product of `a` and `b` is less than or equal to `b`. Here an ordered semiring is a structure which combines the order and operation of both an ordered ring and a semiring. The conditions of `b` being less than or equal to zero and `a` being greater than or equal to 1, ensure that the multiplication operation increases the value when multiplying with a number greater than 1 and decreases it when multiplying with a number less than or equal to 0. The function `Function.swap` is used here to denote the contravariant nature of the operations, i.e., reversing the order of operations.

More concisely: For any ordered semiring `α`, if `a` is in `α` is greater than or equal to 1 and `b` is in `α` is less than or equal to zero, then `a * b` is less than or equal to `b`.

StrictOrderedRing.add_le_add_left

theorem StrictOrderedRing.add_le_add_left : ∀ {α : Type u} [self : StrictOrderedRing α] (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b

This theorem states that addition operation is monotone in a strictly ordered ring. More specifically, for any given type `α` that forms a strictly ordered ring, if a value `a` is less than or equal to another value `b`, then for any value `c`, the sum of `c` and `a` is less than or equal to the sum of `c` and `b`. This property is fundamental in the mathematical structure known as an ordered commutative group.

More concisely: In a strictly ordered ring, if `a` ≤ `b` and `c` is any value, then `c + a` ≤ `c + b`.

mul_self_add_mul_self_eq_zero

theorem mul_self_add_mul_self_eq_zero : ∀ {α : Type u} [inst : LinearOrderedSemiring α] {a b : α} [inst_1 : ExistsAddOfLE α], a * a + b * b = 0 ↔ a = 0 ∧ b = 0

This theorem asserts that for any given type `α` that is a LinearOrderedSemiring (a structure combining order and algebraic properties), and for any two elements `a` and `b` of this type such that addition is possible for any two elements that satisfy a less than or equal to relation, the sum of the squares of `a` and `b` equals zero if and only if both `a` and `b` are zero. Hence, if `a * a + b * b = 0`, then `a = 0` and `b = 0`, and if `a = 0` and `b = 0`, then `a * a + b * b = 0`. It formalizes the mathematical fact that the sum of two squares in a linear ordered semiring can only be zero if both squares are zero themselves.

More concisely: In a LinearOrderedSemiring, the sum of the squares of two elements is zero if and only if both elements are zero.

one_le_mul_of_one_le_of_one_le

theorem one_le_mul_of_one_le_of_one_le : ∀ {α : Type u} [inst : OrderedSemiring α] {a b : α}, 1 ≤ a → 1 ≤ b → 1 ≤ a * b

This theorem states that for any ordered semiring (a type of algebraic structure that includes operations of addition and multiplication and obeys certain axioms), if both 'a' and 'b' are elements of this semiring such that they are both greater than or equal to 1, then their product 'a * b' is also greater than or equal to 1.

More concisely: In any ordered semiring, if both a and b are elements greater than or equal to 1, then their product a * b is also greater than or equal to 1.

OrderedSemiring.zero_le_one

theorem OrderedSemiring.zero_le_one : ∀ {α : Type u} [self : OrderedSemiring α], 0 ≤ 1

This theorem states that zero is less than or equal to one in any ordered semiring. An ordered semiring is a certain kind of algebraic structure that includes both an ordering (such as less than, equal to, or greater than) and operations like addition and multiplication. Therefore, irrespective of the specific ordered semiring being considered, zero will always be less than or equal to one.

More concisely: In every ordered semiring, zero is less than or equal to one.

LinearOrderedSemiring.max_def

theorem LinearOrderedSemiring.max_def : ∀ {α : Type u} [self : LinearOrderedSemiring α] (a b : α), max a b = if a ≤ b then b else a

This theorem states that for any type `α` that forms a linearly ordered semiring (a structure that combines the properties of an ordered ring and a semiring), the maximum value between any two elements `a` and `b` of `α` can be determined using a conditional statement. If `a` is less than or equal to `b`, the maximum is `b`, else it is `a`. Essentially, this theorem formalizes the intuitive way we determine the maximum from two numbers in the context of a linearly ordered semiring.

More concisely: For any linearly ordered semiring type `α`, the maximum of two elements `a` and `b` is given by the conditional expression `if a <= b then b else a`.

pow_le_pow_of_le_one

theorem pow_le_pow_of_le_one : ∀ {α : Type u} [inst : OrderedSemiring α] {a : α}, 0 ≤ a → a ≤ 1 → ∀ {m n : ℕ}, m ≤ n → a ^ n ≤ a ^ m

This theorem states that for any type `α` that is an ordered semiring, and for any element `a` of this type that is between 0 and 1 inclusive, if you raise `a` to the power of `n` and `m` (where `n` and `m` are natural numbers and `m` is less than or equal to `n`), then `a` raised to the `n`th power will be less than or equal to `a` raised to the `m`th power. This theorem captures the property of numbers between 0 and 1 where increasing the exponent results in a smaller number.

More concisely: For any ordered semiring type `α` and element `a` between 0 and 1, `a^n <= a^(m)` when `n >= m`.

LinearOrderedCommSemiring.compare_eq_compareOfLessAndEq

theorem LinearOrderedCommSemiring.compare_eq_compareOfLessAndEq : ∀ {α : Type u_2} [self : LinearOrderedCommSemiring α] (a b : α), compare a b = compareOfLessAndEq a b

The theorem `LinearOrderedCommSemiring.compare_eq_compareOfLessAndEq` states that for any linear ordered commutative semiring `α` and any two elements `a` and `b` from `α`, the comparison of `a` and `b` using the built-in `compare` function is equivalent to the comparison of `a` and `b` using the `compareOfLessAndEq` function, where the latter function returns `Ordering.lt` if `a < b`, `Ordering.eq` if `a = b`, and `Ordering.gt` otherwise. This comparison is conducted in the context of a decidable order (`<`) and equality (`=`).

More concisely: For any linear ordered commutative semiring and its elements, the comparison functions `compare` and `compareOfLessAndEq` agree in their results.

mul_lt_mul'

theorem mul_lt_mul' : ∀ {α : Type u} [inst : StrictOrderedSemiring α] {a b c d : α}, a ≤ c → b < d → 0 ≤ b → 0 < c → a * b < c * d := by sorry

This theorem states that for any strictly ordered semiring `α`, given four elements `a`, `b`, `c`, and `d` of `α`, if `a` is less than or equal to `c`, `b` is less than `d`, `b` is non-negative and `c` is positive, then the product of `a` and `b` is less than the product of `c` and `d`. In mathematical notation, this would be written as: if $a \leq c$, $b < d$, $b \geq 0$ and $c > 0$, then $a \cdot b < c \cdot d$.

More concisely: If `a` is a non-negative element less than a positive element `c` in a strictly ordered semiring, then `a` multiplied by another non-negative element `b` is strictly less than `c` multiplied by another element `d`. In mathematical notation: `0 ≤ a ≤ c`, `b > 0` implies `a * b < c * d`.

LinearOrderedCommRing.mul_comm

theorem LinearOrderedCommRing.mul_comm : ∀ {α : Type u} [self : LinearOrderedCommRing α] (a b : α), a * b = b * a := by sorry

This theorem states that in a linearly ordered commutative ring, the multiplication operation is commutative. Specifically, for any two elements 'a' and 'b' in the ring, the result of multiplying 'a' by 'b' is the same as the result of multiplying 'b' by 'a'. This is a fundamental property of commutative multiplication, and this theorem proves that it holds true in the context of a linearly ordered commutative ring.

More concisely: In a commutative ring with a linear order, multiplication is commutative.

Mathlib.Algebra.Order.Ring.Defs._auxLemma.1

theorem Mathlib.Algebra.Order.Ring.Defs._auxLemma.1 : ∀ {α : Type u} [inst : OrderedSemiring α] {a : α}, 0 ≤ a → ∀ (n : ℕ), (0 ≤ a ^ n) = True

This theorem states that for any type `α` that forms an ordered semiring and for any element `a` of this type, if `a` is greater than or equal to zero, then for any natural number `n`, `a` raised to the power `n` is also greater than or equal to zero. In other words, the nonnegative power of a nonnegative number in an ordered semiring is always nonnegative.

More concisely: For any ordered semiring type `α` and its non-negative element `a`, if `a` is non-negative, then `a^n` is non-negative for all natural numbers `n`.

lt_mul_of_lt_one_left

theorem lt_mul_of_lt_one_left : ∀ {α : Type u} [inst : StrictOrderedSemiring α] {a b : α} [inst_1 : ExistsAddOfLE α], b < 0 → a < 1 → b < a * b

This theorem, `lt_mul_of_lt_one_left`, states that for any strictly ordered semiring `α`, and any two elements `a` and `b` of `α`, if `b` is less than zero and `a` is less than one, then `b` is less than the product of `a` and `b`. In mathematical terms, if `b < 0` and `a < 1`, then `b < a * b`. The existence of an addition operation for any two elements in `α` which are less than or equal to each other is also required.

More concisely: If `α` is a strictly ordered semiring with an addition operation, and `a` and `b` are elements of `α` with `b < 0` and `a < 1`, then `b < a * b`.

OrderedSemiring.mul_le_mul_of_nonneg_left

theorem OrderedSemiring.mul_le_mul_of_nonneg_left : ∀ {α : Type u} [self : OrderedSemiring α] (a b c : α), a ≤ b → 0 ≤ c → c * a ≤ c * b

This theorem states that in any ordered semiring, when you have an inequality `a ≤ b` and another non-negative element `c` such that `0 ≤ c`, then the product of `c` and `a` is less than or equal to the product of `c` and `b`, that is `c * a ≤ c * b`. This is essentially a rule that allows us to multiply inequalities by non-negative elements on the left side in the context of ordered semirings.

More concisely: In any ordered semiring, if `0 ≤ c` and `a ≤ b`, then `c * a ≤ c * b`.

StrictOrderedCommRing.mul_comm

theorem StrictOrderedCommRing.mul_comm : ∀ {α : Type u_2} [self : StrictOrderedCommRing α] (a b : α), a * b = b * a

This theorem states that multiplication is a commutative operation in a specific type of algebraic structure called a "strict ordered commutative ring". In simpler terms, for any two elements `a` and `b` in an ordered commutative ring, the product of `a` and `b` is the same as the product of `b` and `a`. This means that the order in which the elements are multiplied does not change the result.

More concisely: In an ordered commutative ring, multiplication is commutative, that is, `a * b = b * a` for all elements `a` and `b`.

StrictOrderedCommSemiring.mul_comm

theorem StrictOrderedCommSemiring.mul_comm : ∀ {α : Type u} [self : StrictOrderedCommSemiring α] (a b : α), a * b = b * a

This theorem states that in a strict ordered commutative semiring, multiplication is commutative. Concretely, for any two elements `a` and `b` of the semiring, the product of `a` and `b` is equal to the product of `b` and `a`. That is, the order in which the elements are multiplied does not affect the outcome.

More concisely: In a strict ordered commutative semiring, multiplication is commutative, that is, `a * b = b * a` for all `a` and `b` in the semiring.

OrderedSemiring.mul_le_mul_of_nonneg_right

theorem OrderedSemiring.mul_le_mul_of_nonneg_right : ∀ {α : Type u} [self : OrderedSemiring α] (a b c : α), a ≤ b → 0 ≤ c → a * c ≤ b * c

This theorem states that in an ordered semiring, if we have an inequality such that `a` is less than or equal to `b`, and if we also have a non-negative element `c` (meaning `c` is greater than or equal to 0), then the result of multiplying `a` by `c` is less than or equal to the result of multiplying `b` by `c`. This preserves the original inequality when scaling by a non-negative factor.

More concisely: In an ordered semiring, if $a \leq b$ and $c \geq 0$, then $a \cdot c \leq b \cdot c$.

LinearOrderedRing.compare_eq_compareOfLessAndEq

theorem LinearOrderedRing.compare_eq_compareOfLessAndEq : ∀ {α : Type u} [self : LinearOrderedRing α] (a b : α), compare a b = compareOfLessAndEq a b

The theorem `LinearOrderedRing.compare_eq_compareOfLessAndEq` states that for any type `α` which has a linear ordered ring structure, the comparison of any two elements `a` and `b` using the `compare` function is equivalent to the comparison using the `compareOfLessAndEq` function. This is true given that the less-than `<` relation and equality `=` operation are decidable on `α`. In simpler terms, it says that two different methods of comparing elements in a linear ordered ring will give the same result.

More concisely: For any linear ordered ring type `α` with decidable `<` and `=` operations, the comparison functions `compare` and `compareOfLessAndEq` agree on all elements of `α`.

neg_one_lt_zero

theorem neg_one_lt_zero : ∀ {α : Type u} [inst : LinearOrderedRing α], -1 < 0

This theorem states that for any type `α` that is a linear ordered ring, the negative one (`-1`) is less than zero (`0`). In terms of mathematics, for any linear ordered ring (which is a ring that also has a linear order compatible with the ring operations), the value `-1` is always less than `0`.

More concisely: In a linear ordered ring, $-1 < 0$.

OrderedCommSemiring.mul_comm

theorem OrderedCommSemiring.mul_comm : ∀ {α : Type u} [self : OrderedCommSemiring α] (a b : α), a * b = b * a := by sorry

The theorem `OrderedCommSemiring.mul_comm` states that multiplication is commutative in an ordered commutative semiring. In other words, for any ordered commutative semiring `α` and any two elements `a` and `b` in `α`, the result of multiplying `a` by `b` is the same as the result of multiplying `b` by `a`. In mathematical terms, this is equivalent to saying that for all `a` and `b` in `α`, `a * b = b * a`.

More concisely: In an ordered commutative semiring, multiplication is commutative: `a * b = b * a` for all `a` and `b` in the semiring.

mul_le_one

theorem mul_le_one : ∀ {α : Type u} [inst : OrderedSemiring α] {a b : α}, a ≤ 1 → 0 ≤ b → b ≤ 1 → a * b ≤ 1

This theorem states that for any type `α` that has the structure of an ordered semiring, if `a` and `b` are elements of `α` such that `a` is less than or equal to 1, `b` is non-negative (equal to or greater than 0), and `b` is less than or equal to 1, then the product of `a` and `b` is less than or equal to 1. In simpler terms, in a certain numerical context (an ordered semiring), if you multiply a number not exceeding 1 with a number between 0 and 1, the result will not exceed 1.

More concisely: In an ordered semiring, the product of any element less than or equal to 1 and any non-negative element less than or equal to 1 is less than or equal to 1.

mul_lt_mul

theorem mul_lt_mul : ∀ {α : Type u} [inst : StrictOrderedSemiring α] {a b c d : α}, a < c → b ≤ d → 0 < b → 0 ≤ c → a * b < c * d := by sorry

This theorem states that for any type `α` that is a strictly ordered semiring (a mathematical structure with two operations, namely addition and multiplication, where the set is strictly ordered and the operations obey certain properties), given four elements `a`, `b`, `c`, `d` of this type, if `a` is less than `c`, `b` is less than or equal to `d`, `b` is greater than zero, and `c` is greater than or equal to zero, then the product of `a` and `b` is less than the product of `c` and `d`. This is a statement about the interplay of order and multiplication in strictly ordered semirings.

More concisely: In a strictly ordered semiring, if a ≤ c and b > 0 with d ≥ 0, then a * b < c * d.

pow_two_nonneg

theorem pow_two_nonneg : ∀ {α : Type u} [inst : LinearOrderedSemiring α] [inst_1 : ExistsAddOfLE α] (a : α), 0 ≤ a ^ 2

This theorem, `pow_two_nonneg`, states that for any element `a` of a type `α` that is a linear ordered semiring and supports the existence of an additive identity element greater than or equal to another element, the square of `a` (`a` raised to the power 2) is always nonnegative, or in other words, greater than or equal to zero.

More concisely: For any element `a` in a linear ordered semiring with an additive identity `0` such that `0 ≤ a`, the square of `a` is nonnegative, i.e., `a² ≥ 0`.

OrderedRing.zero_le_one

theorem OrderedRing.zero_le_one : ∀ {α : Type u} [self : OrderedRing α], 0 ≤ 1

This theorem states that in any ordered ring, zero is less than or equal to one. An ordered ring is a ring that also has a total order compatible with the ring operations. Hence, for any type `α` that is an ordered ring, `0 ≤ 1` holds true.

More concisely: In every ordered ring, the additive identity (zero) is less than or equal to one.

Mathlib.Algebra.Order.Ring.Defs._auxLemma.26

theorem Mathlib.Algebra.Order.Ring.Defs._auxLemma.26 : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α}, (0 < -a) = (a < 0)

This theorem, referred to as `_auxLemma.26` under the `Mathlib.Algebra.Order.Ring.Defs` namespace, states that for any type `α` satisfying the properties of an additive group and an ordered set (with the order compatible with the group operation), the assertion that zero is less than the negation of an element `a` from this type is equivalent to the assertion that `a` is less than zero. In mathematical terms, this theorem says that for all `a` in a certain type of ordered group, `0 < -a` if and only if `a < 0`.

More concisely: In an ordered additive group, the elements `0` and `-a` are order-equivalent if and only if `a` and `0` are.

strictAnti_mul_right

theorem strictAnti_mul_right : ∀ {α : Type u} [inst : StrictOrderedSemiring α] [inst_1 : ExistsAddOfLE α] {a : α}, a < 0 → StrictAnti fun x => x * a

The theorem `strictAnti_mul_right` states that for any type `α` that has a structure of a strict ordered semiring and a proof of existence of addition for less than or equal numbers, and for any element `a` of `α` that is less than zero, the function that multiplies `x` by `a` is strictly antitone. In other words, for all `x` and `y` from `α` such that `x` is less than `y`, `y * a` is in fact less than `x * a`. This represents the idea that multiplication by a negative number reverses the order of numbers.

More concisely: For any strict ordered semiring type `α` with proven existence of addition for less than or equal numbers, and for any negative element `a` of `α`, the function `x => x * a` is strictly antitone, i.e., for all `x` and `y` in `α` with `x < y`, `y * a < x * a`.

zero_le_mul_right

theorem zero_le_mul_right : ∀ {α : Type u} [inst : LinearOrderedSemiring α] {b c : α}, 0 < c → (0 ≤ b * c ↔ 0 ≤ b) := by sorry

This theorem, `zero_le_mul_right`, states that for any type `α` that is a linearly ordered semiring, and any two elements `b` and `c` of `α`, if `c` is greater than zero (`0 < c`), then `b * c` is greater than or equal to zero (`0 ≤ b * c`) if and only if `b` is greater than or equal to zero (`0 ≤ b`). In other words, the non-negativity of the product of `b` and `c` is guaranteed if `c` is positive and `b` is non-negative. This is an alias of the theorem `mul_nonneg_iff_of_pos_right`.

More concisely: For any linearly ordered semiring type `α` and elements `b` and `c` of `α` with `0 < c`, `0 ≤ b * c` if and only if `0 ≤ b`.

strictAnti_mul_left

theorem strictAnti_mul_left : ∀ {α : Type u} [inst : StrictOrderedSemiring α] [inst_1 : ExistsAddOfLE α] {a : α}, a < 0 → StrictAnti fun x => a * x

The theorem `strictAnti_mul_left` states that for any type `α` which has a strictly ordered semiring structure and supports the existence of addition for less than or equal elements, if `a` is a negative element of this type `α`, then the function that multiplies `a` by a variable `x` is strictly antitone. In other words, given any two elements `b` and `c` of type `α` where `b < c`, multiplying `a` by `c` will yield a value less than the result of multiplying `a` by `b`.

More concisely: For any strictly ordered semiring type `α` with additive order and negative element `a`, the function `x => a * x` is strictly decreasing on the positive part of `α`.