mul_tsub
theorem mul_tsub :
∀ {α : Type u} [inst : CanonicallyOrderedCommSemiring α] [inst_1 : Sub α] [inst_2 : OrderedSub α]
[inst_3 : IsTotal α fun x x_1 => x ≤ x_1]
[inst_4 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a b c : α),
a * (b - c) = a * b - a * c
This theorem states that for any type `α` that is a canonically ordered commutative semiring with subtraction (denoted by `-`), following an ordered subtraction law, total order (`≤`) and contravariant class with respect to addition (`+`) and total order (`≤`), the distributive property of multiplication over subtraction holds. In other words, for any three elements `a`, `b`, and `c` of the type `α`, the product of `a` and the difference of `b` and `c` (i.e., `a * (b - c)`) is equal to the difference of the product of `a` and `b` and the product of `a` and `c` (i.e., `a * b - a * c`).
More concisely: For any commutative semiring `α` with subtraction and order `≤` satisfying the ordered subtraction and contravariance properties, the distributive property of multiplication over subtraction holds: `a * (b - c) = a * b - a * c` for all `a, b, c` in `α`.
|
CanonicallyOrderedCommSemiring.natCast_succ
theorem CanonicallyOrderedCommSemiring.natCast_succ :
∀ {α : Type u_2} [self : CanonicallyOrderedCommSemiring α] (n : ℕ),
NatCast.natCast (n + 1) = NatCast.natCast n + 1
This theorem states that for any given type `α`, which is a canonically ordered commutative semiring, the canonical map from natural numbers `ℕ` to `α` preserves the successor function. In other words, casting the natural number `n + 1` to `α` is equivalent to casting `n` to `α` and then adding `1` in the semiring `α`.
More concisely: For any commutative semiring `α` with a canonical order, the canonical map from natural numbers to `α` preserves the successor function: `coe : ℕ → α` satisfies `coe (n + 1) = coe n + 1`.
|
CanonicallyOrderedCommSemiring.right_distrib
theorem CanonicallyOrderedCommSemiring.right_distrib :
∀ {α : Type u_2} [self : CanonicallyOrderedCommSemiring α] (a b c : α), (a + b) * c = a * c + b * c
This theorem states that, in a canonically ordered commutative semiring of a certain type (`α`), multiplication distributes over addition from the right. Specifically, given any three elements (`a`, `b`, `c`) in this semiring, the product of the sum of `a` and `b` with `c` is equal to the sum of the product of `a` and `c` with the product of `b` and `c`. In mathematical notation, this is expressed as `(a + b) * c = a * c + b * c`.
More concisely: In a commutative semiring, multiplication distributes over addition from the right: `(a + b) * c = a * c + b * c` for all elements `a`, `b`, and `c`.
|
CanonicallyOrderedCommSemiring.mul_comm
theorem CanonicallyOrderedCommSemiring.mul_comm :
∀ {α : Type u_2} [self : CanonicallyOrderedCommSemiring α] (a b : α), a * b = b * a
This theorem states that for any type `α` that is a canonically ordered commutative semiring, the multiplication operation is commutative. In other words, for any two elements `a` and `b` of type `α`, the result of multiplying `a` by `b` is the same as the result of multiplying `b` by `a`.
More concisely: For any commutative semiring `α` with a canonical order, multiplication is commutative: `a * b = b * a` for all `a, b` in `α`.
|
CanonicallyOrderedCommSemiring.npow_zero
theorem CanonicallyOrderedCommSemiring.npow_zero :
∀ {α : Type u_2} [self : CanonicallyOrderedCommSemiring α] (x : α), CanonicallyOrderedCommSemiring.npow 0 x = 1
This theorem states that for any canonically ordered commutative semiring `α`, and for any element `x` of `α`, raising `x` to the power of `0` results in `1`. In other words, in any canonically ordered commutative semiring, any element to the power of zero equals the multiplicative identity, which is `1`. This is analogous to the rule in basic arithmetic where any number raised to the power of zero is `1`.
More concisely: In any commutative semiring with a canonical ordering, any element raised to the power of 0 equals the multiplicative identity 1.
|
CanonicallyOrderedCommSemiring.mul_one
theorem CanonicallyOrderedCommSemiring.mul_one :
∀ {α : Type u_2} [self : CanonicallyOrderedCommSemiring α] (a : α), a * 1 = a
This theorem states that for any canonically ordered commutative semiring `α`, one (`1`) is a right neutral element for the multiplication operation. In other words, for any element `a` from the semiring, the product of `a` and one (`1`) is equal to `a` itself. This property is a basic characteristic of multiplicative operations in a semiring.
More concisely: For any commutative semiring `α`, the multiplicative identity `1` is a right identity for the multiplication operation, i.e., for all `a` in `α`, `a * 1 = a`.
|
CanonicallyOrderedCommSemiring.mul_zero
theorem CanonicallyOrderedCommSemiring.mul_zero :
∀ {α : Type u_2} [self : CanonicallyOrderedCommSemiring α] (a : α), a * 0 = 0
This theorem states that zero is a right absorbing element for multiplication in a canonically ordered commutative semiring. In mathematical terms, given any element `a` from a canonically ordered commutative semiring `α`, the product of `a` and zero always equals zero. This property is commonly known in mathematics where multiplying any number by zero results in zero.
More concisely: In a commutative semiring with canonical ordering, the product of any element with zero is zero.
|
CanonicallyOrderedCommSemiring.npow_succ
theorem CanonicallyOrderedCommSemiring.npow_succ :
∀ {α : Type u_2} [self : CanonicallyOrderedCommSemiring α] (n : ℕ) (x : α),
CanonicallyOrderedCommSemiring.npow (n + 1) x = CanonicallyOrderedCommSemiring.npow n x * x
This theorem states that for any canonically ordered commutative semiring (a mathematical structure with two binary operations satisfying certain properties) and any element `x` of that semiring, if you raise `x` to the power of `n + 1` (where `n` is a natural number), the result is the same as taking `x` to the power of `n` and then multiplying by `x`. In mathematical notation, for all `n` in the natural numbers and all `x` in the semiring, $(x^{n+1}) = (x^n) * x$.
More concisely: For any commutative semiring and its element `x`, the power `x^(n+1)` equals `x^n` multiplied by `x`, where `n` is a natural number.
|
CanonicallyOrderedCommSemiring.left_distrib
theorem CanonicallyOrderedCommSemiring.left_distrib :
∀ {α : Type u_2} [self : CanonicallyOrderedCommSemiring α] (a b c : α), a * (b + c) = a * b + a * c
This theorem states that for any canonically ordered commutative semiring `α`, multiplication is left distributive over addition. Specifically, for any elements `a`, `b`, `c` of this semiring, the product of `a` and the sum of `b` and `c` equals the sum of the product of `a` and `b` with the product of `a` and `c`. In mathematical terms, it asserts that `a * (b + c) = a * b + a * c` for all `a`, `b`, `c` in `α`.
More concisely: For any commutative semiring `α` with canonical ordering, multiplication distributes over addition, i.e., `a * (b + c) = a * b + a * c` for all `a, b, c` in `α`.
|
CanonicallyOrderedCommSemiring.eq_zero_or_eq_zero_of_mul_eq_zero
theorem CanonicallyOrderedCommSemiring.eq_zero_or_eq_zero_of_mul_eq_zero :
∀ {α : Type u_2} [self : CanonicallyOrderedCommSemiring α] {a b : α}, a * b = 0 → a = 0 ∨ b = 0
This theorem states that in any canonically ordered commutative semiring, if the product of two elements 'a' and 'b' is zero, then either 'a' or 'b' (or both) must be zero. This property is called "no zero divisors". In other words, there are no nonzero elements 'a' and 'b' such that their product equals zero.
More concisely: In a commutative semiring with canonical ordering, the product of two nonzero elements is nonzero.
|
CanonicallyOrderedCommSemiring.mul_assoc
theorem CanonicallyOrderedCommSemiring.mul_assoc :
∀ {α : Type u_2} [self : CanonicallyOrderedCommSemiring α] (a b c : α), a * b * c = a * (b * c)
This theorem states that multiplication is associative for any canonically ordered commutative semiring. In other words, for any three elements `a`, `b`, and `c` of a given type `α` that forms a canonically ordered commutative semiring, the product of `a`, `b`, and `c` remains the same irrespective of how they are grouped. In mathematical notation, this would be `a * b * c = a * (b * c)`.
More concisely: In a commutative semiring with canonical ordering, multiplication is associative: `a * b * c = a * (b * c)` for all `a`, `b`, and `c` in the semiring.
|
CanonicallyOrderedCommSemiring.one_mul
theorem CanonicallyOrderedCommSemiring.one_mul :
∀ {α : Type u_2} [self : CanonicallyOrderedCommSemiring α] (a : α), 1 * a = a
This theorem states that for any canonically ordered commutative semiring `α`, the number `1` is a left neutral element for multiplication. That is, for any element `a` in `α`, multiplying `1` by `a` results in `a` itself. This property is one of the fundamental properties of any semiring structure.
More concisely: In any commutative semiring, the multiplicative identity (1) is a left identity for multiplication, i.e., for all elements `a`, `1 * a = a`.
|
CanonicallyOrderedCommSemiring.natCast_zero
theorem CanonicallyOrderedCommSemiring.natCast_zero :
∀ {α : Type u_2} [self : CanonicallyOrderedCommSemiring α], NatCast.natCast 0 = 0
This theorem states that for any type `α` that has a structure of `CanonicallyOrderedCommSemiring`, the canonical map from natural numbers (`ℕ`) to `α` sends the natural number `0` to the `0` of `α`. This means that under this map, the element `0` from the set of natural numbers is mapped to the element `0` in the semiring `α`.
More concisely: For any `CanonicallyOrderedCommSemiring` type `α`, the canonical map from `ℕ` to `α` maps `0` to `0` in `α`.
|
tsub_mul
theorem tsub_mul :
∀ {α : Type u} [inst : CanonicallyOrderedCommSemiring α] [inst_1 : Sub α] [inst_2 : OrderedSub α]
[inst_3 : IsTotal α fun x x_1 => x ≤ x_1]
[inst_4 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a b c : α),
(a - b) * c = a * c - b * c
This theorem states that, for any type `α` that is a canonically ordered commutative semiring and also supports subtraction operation that is ordered, and for any three elements `a`, `b`, and `c` of this type, the operation of subtracting `b` from `a` and then multiplying the result by `c` is equivalent to first multiplying `a` and `b` by `c` and then subtracting the two results. In mathematical notation, this can be written as `(a - b) * c = a * c - b * c`. This can be thought of as a distributive property of multiplication over subtraction in this algebraic structure.
More concisely: For any commutative semiring `α` with a canonically ordered additive and multiplicative structure and supported subtraction operation, the distribution law holds: `(a - b) * c = a * c - b * c` for all `a, b, c ∈ α`.
|
CanonicallyOrderedCommSemiring.zero_mul
theorem CanonicallyOrderedCommSemiring.zero_mul :
∀ {α : Type u_2} [self : CanonicallyOrderedCommSemiring α] (a : α), 0 * a = 0
This theorem states that zero is a left absorbing element for multiplication in a canonically ordered commutative semiring. In other words, for any element 'a' of a type 'α' that forms a canonically ordered commutative semiring, the result of the operation '0 * a' will always be zero.
More concisely: In a commutative semiring with canonical ordering, multiplication of any element by zero results in zero.
|