Semiring.natCast_zero
theorem Semiring.natCast_zero : ∀ {α : Type u} [self : Semiring α], NatCast.natCast 0 = 0
This theorem states that for all types `α`, given that `α` has a semiring structure, the canonical map from the set of natural numbers `ℕ` to `α` sends the natural number `0` to the `0` of the semiring `α`. In more mathematical terms, for any semiring `R`, the map `NatCast.natCast : ℕ → R` sends `0` to `0` in `R`.
More concisely: For any semiring `R`, the natural number zero map `NatCast.natCast : ℕ → R` sends zero in `ℕ` to zero in `R`.
|
NonAssocSemiring.mul_one
theorem NonAssocSemiring.mul_one : ∀ {α : Type u} [self : NonAssocSemiring α] (a : α), a * 1 = a
This theorem states that one is a right neutral element for multiplication in a non-associative semiring. In other words, for any element 'a' of type 'α' in a non-associative semiring, the product of 'a' and one is equal to 'a'.
More concisely: In a non-associative semiring, for all elements 'a' of type 'α', the multiplication of 'a' with the multiplicative identity (denoted as '1') results in 'a'. That is, 'a * 1 = a'.
|
Semiring.natCast_succ
theorem Semiring.natCast_succ :
∀ {α : Type u} [self : Semiring α] (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
The theorem `Semiring.natCast_succ` states that for all types `α` equipped with a semiring structure, the canonical mapping from natural numbers (ℕ) to `α` is a homomorphism. In other words, for every natural number `n`, the mapping of the successor of `n` (i.e., `n+1`) is equal to the mapping of `n` plus `1` in the semiring `α`. This essentially means that the addition operation on natural numbers is preserved under this mapping to the semiring `α`.
More concisely: The canonical map from natural numbers to a semiring α is a homomorphism, preserving the successor operation. In other words, for all semirings α and natural numbers n, we have (canonicalMap α (n+1)) = (canonicalMap α n) + 1.
|
CommSemiring.mul_comm
theorem CommSemiring.mul_comm : ∀ {R : Type u} [self : CommSemiring R] (a b : R), a * b = b * a
The theorem `CommSemiring.mul_comm` states that for any type `R` that has a `CommSemiring` structure, multiplication operation is commutative. In other words, for any two elements `a` and `b` of type `R`, the result of `a * b` is the same as the result of `b * a`. This concept follows from the fact that the operation of multiplication in a commutative semiring (or a commutative multiplicative magma) is commutative, as given by the name of the structure.
More concisely: For any commutative semiring `R`, the multiplication operation is commutative, i.e., `a * b = b * a` for all `a, b` in `R`.
|
neg_eq_neg_one_mul
theorem neg_eq_neg_one_mul : ∀ {α : Type u} [inst : MulOneClass α] [inst_1 : HasDistribNeg α] (a : α), -a = -1 * a := by
sorry
This theorem states that for any type `α` that is a multiplication-one class (i.e., it supports multiplication and has an identity element for multiplication), and has a negation operation following the distributive law, the negative of an element `a` (`-a`) is equal to `-1` multiplied by `a` (`-1 * a`). This essentially encapsulates the mathematical property of negative numbers in a general algebraic structure.
More concisely: For any multiplication-one class type `α` with negation operation following distributive law, negative of an element `a` equals `-1 * a`.
|
LeftDistribClass.left_distrib
theorem LeftDistribClass.left_distrib :
∀ {R : Type u_1} [inst : Mul R] [inst_1 : Add R] [self : LeftDistribClass R] (a b c : R),
a * (b + c) = a * b + a * c
This theorem states that multiplication is left distributive over addition for any type `R` that has both multiplication (`Mul R`) and addition (`Add R`) operations defined. Specifically, for any three elements `a`, `b`, and `c` of type `R`, the product of `a` and the sum of `b` and `c` (i.e., `a * (b + c)`) is equal to the sum of the product of `a` and `b` and the product of `a` and `c` (i.e., `a * b + a * c`). In mathematical terms, this property can be written as: `a * (b + c) = a * b + a * c`.
More concisely: For all types `R` with defined multiplication and addition operations, and all elements `a`, `b`, and `c` of type `R`, `a * (b + c)` equals `a * b + a * c`.
|
two_mul
theorem two_mul : ∀ {α : Type u} [inst : NonAssocSemiring α] (n : α), 2 * n = n + n
This theorem states that for all types 'α' that have the structure of a 'NonAssocSemiring' (which is a mathematical structure like a ring but without the requirement that multiplication is associative), the multiplication of any element 'n' of this type by 2 is equivalent to adding 'n' to itself. In other words, for all 'n' in such a semiring, `2 * n = n + n`.
More concisely: For any non-associative semiring 'α', the multiplication of an element 'n' by 2 is equivalent to adding 'n' to itself: 2 * n = n + n.
|
mul_add
theorem mul_add :
∀ {R : Type x} [inst : Mul R] [inst_1 : Add R] [inst_2 : LeftDistribClass R] (a b c : R),
a * (b + c) = a * b + a * c
This theorem, called `mul_add`, is an alias of `left_distrib`. It states that for any type `R` that has multiplication and addition operations, and for which the left distribution law holds, the product of `a` with the sum of `b` and `c` (`a * (b + c)`) is equal to the sum of the product of `a` and `b` and the product of `a` and `c` (`a * b + a * c`). This corresponds to the left distributive property in algebra, often given as $a \cdot (b + c) = a \cdot b + a \cdot c$.
More concisely: For any type `R` with multiplication and addition operations satisfying the left distribution law, `a * (b + c)` equals `a * b + a * c`.
|
mul_neg
theorem mul_neg : ∀ {α : Type u} [inst : Mul α] [inst_1 : HasDistribNeg α] (a b : α), a * -b = -(a * b)
This theorem, `mul_neg`, states that for all types `α` that support multiplication (indicated by `Mul α`) and distributed negation (indicated by `HasDistribNeg α`), for any two elements `a` and `b` of this type, the product of `a` and `-b` is equal to the negation of the product of `a` and `b`. In mathematical notation, this corresponds to the statement `a * (-b) = -(a * b)`.
More concisely: For all types `α` with multiplication and distributive negation, `a * (-b) = -(a * b)`.
|
NonUnitalSemiring.mul_assoc
theorem NonUnitalSemiring.mul_assoc :
∀ {α : Type u} [self : NonUnitalSemiring α] (a b c : α), a * b * c = a * (b * c)
This theorem states that multiplication is associative in a non-unital semiring. Specifically, for any three elements `a`, `b`, and `c` of a non-unital semiring `α`, the product of `a`, `b`, and `c` is the same whether we first multiply `a` and `b` and then multiply the result with `c` (`a * b * c`), or we first multiply `b` and `c` and then multiply `a` with the result (`a * (b * c)`). This property holds for all non-unital semirings.
More concisely: In a non-unital semiring, the order of multiplication of elements does not affect the result: `(a * b) * c = a * (b * c)` for all `a, b, c` in the semiring.
|
add_one_mul
theorem add_one_mul :
∀ {α : Type u} [inst : Add α] [inst_1 : MulOneClass α] [inst_2 : RightDistribClass α] (a b : α),
(a + 1) * b = a * b + b
This theorem, `add_one_mul`, states that for any type `α` that has addition, multiplication with one, and right distributivity properties, for any two elements `a` and `b` of that type, the expression `(a + 1) * b` is equal to `a * b + b`. In mathematical terms, this is equivalent to stating the distributive property of multiplication over addition: `(a + 1) * b = a * b + b`.
More concisely: For any type `α` with additions, multiplications with one, and right distributivity properties, `(a + 1) * b = a * b + b` for all `a, b` in `α`.
|
mul_sub_left_distrib
theorem mul_sub_left_distrib :
∀ {α : Type u} [inst : NonUnitalNonAssocRing α] (a b c : α), a * (b - c) = a * b - a * c
This theorem, named `mul_sub_left_distrib`, states that for all types `α` that have a structure of a non-unital, non-associative ring (denoted by `NonUnitalNonAssocRing α`), the standard property of left distributivity of multiplication over subtraction holds. In more formal mathematical terms, for any three elements `a`, `b` and `c` of type `α`, the product of `a` and the difference of `b` and `c` is equal to the difference of the product of `a` and `b` and the product of `a` and `c`. This can be represented in LaTeX math as: \(a \cdot (b - c) = a \cdot b - a \cdot c\).
More concisely: For any non-unital, non-associative ring type `α`, the left distributivity of multiplication over subtraction holds: `a * (b - c) = a * b - a * c`.
|
NonAssocRing.intCast_negSucc
theorem NonAssocRing.intCast_negSucc :
∀ {α : Type u_1} [self : NonAssocRing α] (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
The theorem `NonAssocRing.intCast_negSucc` asserts that for any non-associative ring `α` and any natural number `n`, the canonical homomorphism from the integers to `α` applied to the negation of the successor of `n` is equal to the negation of the canonical homomorphism from the natural numbers to `α` applied to `n + 1`. In other words, it states that in the context of a non-associative ring, the process of casting a negative integer (expressed as the negation of a successor of a natural number) to a ring element is the same as first casting a natural number to the ring and then taking the additive inverse.
More concisely: In a non-associative ring, the mapping of the negation of the successor of a natural number to a ring element is equal to the additive inverse of the mapping of the natural number itself.
|
sub_mul
theorem sub_mul : ∀ {α : Type u} [inst : NonUnitalNonAssocRing α] (a b c : α), (a - b) * c = a * c - b * c
This theorem, named `sub_mul`, asserts that for any non-unital, non-associative ring α, and any elements a, b, and c of α, the operation of subtracting b from a and then multiplying by c is the same as subtracting the product of b and c from the product of a and c. In mathematical notation, this would be written as $(a - b) * c = a * c - b * c$. This theorem is an alias of the `mul_sub_right_distrib` theorem.
More concisely: For any non-unital, non-associative ring α and elements a, b, and c in α, the distributive property holds: a * (c - b) = a * c - a * b.
|
mul_one_add
theorem mul_one_add :
∀ {α : Type u} [inst : Add α] [inst_1 : MulOneClass α] [inst_2 : LeftDistribClass α] (a b : α),
a * (1 + b) = a + a * b
This theorem, `mul_one_add`, states that for all types `α`, that have addition, multiplication with a multiplicative identity, and left-distributive properties, the result of a number `a` multiplied by the sum of `1` and another number `b` is equal to `a` added to the product of `a` and `b`. In mathematical terms, it's establishing that `a * (1 + b) = a + a * b` for all `a` and `b` in type α, which is a generalization of the distributive law of multiplication over addition.
More concisely: For all types `α` with additions, multiplications, and left-distributive properties, `a * (1 + b) = a + a * b` for all `a, b` in `α`.
|
NonAssocSemiring.natCast_zero
theorem NonAssocSemiring.natCast_zero : ∀ {α : Type u} [self : NonAssocSemiring α], NatCast.natCast 0 = 0
This theorem states that for any type `α` that has a structure of a non-associative semiring, the canonical map from natural numbers to `α`, denoted as `NatCast.natCast`, sends the number `0` from the set of natural numbers (`ℕ`) to the `0` in `α`. In other words, when you apply this canonical map to `0`, you get the zero element of the semiring `α`.
More concisely: For any non-associative semiring type `α`, the canonical map `NatCast.natCast` from natural numbers maps `0` to the additive identity of `α`.
|
Semiring.mul_one
theorem Semiring.mul_one : ∀ {α : Type u} [self : Semiring α] (a : α), a * 1 = a
This theorem states that one is a right neutral element for the multiplication operation in a semiring. In other words, for any element 'a' of a given type 'α' that forms a semiring, the product of 'a' and 1 is always 'a'. This property is one of the defining characteristics of a semiring.
More concisely: In a semiring, for all elements 'a' of type 'α', 'a' * 1 = 'a'.
|
neg_one_mul
theorem neg_one_mul : ∀ {α : Type u} [inst : MulOneClass α] [inst_1 : HasDistribNeg α] (a : α), -1 * a = -a
This theorem, `neg_one_mul`, states that for any element 'a' of a ring (denoted by the type α), the product of the additive inverse of one and 'a' equals the additive inverse of 'a'. In other words, multiplying any element of the ring by negative one produces the negative of that element. This is often a property in many algebraic structures including rings and fields.
More concisely: For any ring element 'a', negative one times 'a' equals the additive inverse of 'a'.
|
mul_ite
theorem mul_ite :
∀ {α : Type u_1} [inst : Mul α] (P : Prop) [inst_1 : Decidable P] (a b c : α),
(a * if P then b else c) = if P then a * b else a * c
This theorem, `mul_ite`, states that for any type `α` that supports multiplication, any proposition `P`, and any three elements `a`, `b`, and `c` of type `α`, the product of `a` and the result of an "if-then-else" condition based on `P` selecting between `b` and `c` is equal to the result of an "if-then-else" condition based on `P` selecting between the product of `a` and `b` and the product of `a` and `c`. In simpler terms, it states that multiplication distributes over the "if-then-else" conditional - the expression "a times (if P then b else c)" is the same as the expression "if P then (a times b) else (a times c)".
More concisely: For any type `α` with multiplication and proposition `P`, the multiplication of `a` with the conditional `(if P then b else c)` equals the conditional `(if P then (a * b) else (a * c))`.
|
Semiring.npow_succ
theorem Semiring.npow_succ :
∀ {α : Type u} [self : Semiring α] (n : ℕ) (x : α), Semiring.npow (n + 1) x = Semiring.npow n x * x
The theorem `Semiring.npow_succ` states that for any type `α` that forms a semiring, any natural number `n`, and any element `x` of `α`, the function `Semiring.npow` that raises an element to the power of a natural number behaves as expected when raising to the power `(n + 1 : ℕ)`. Specifically, `Semiring.npow (n + 1) x` equals `Semiring.npow n x * x`, which mirrors the intuitive notion of powers in mathematics: raising an element to the `(n+1)`-th power is equivalent to raising it to the `n`-th power and then multiplying by the element itself.
More concisely: For any semiring `α`, `Semiring.npow (n + 1) x = Semiring.npow n x * x`, where `n` is a natural number and `x` is an element of `α`.
|
NonUnitalCommRing.mul_comm
theorem NonUnitalCommRing.mul_comm : ∀ {α : Type u} [self : NonUnitalCommRing α] (a b : α), a * b = b * a
This theorem states that in a non-unital commutative ring, the operation of multiplication is commutative. In other words, for any two elements `a` and `b` of the ring, the product of `a` and `b` is equal to the product of `b` and `a`. The ring is "non-unital", meaning it does not necessarily have a multiplicative identity element.
More concisely: In a commutative non-unital ring, the multiplication is commutative, i.e., for all elements `a` and `b`, `a * b` equals `b * a`.
|
NonAssocRing.intCast_ofNat
theorem NonAssocRing.intCast_ofNat : ∀ {α : Type u_1} [self : NonAssocRing α] (n : ℕ), IntCast.intCast ↑n = ↑n := by
sorry
This theorem states that for any type `α` which has a `NonAssocRing` structure, the canonical homomorphism from integers `ℤ` to `α`, agrees with the homomorphism from natural numbers `ℕ` to `α` when applied on natural numbers. In other words, when you cast a natural number `n` to an integer and then further cast it to some ring `α`, you get the same result as casting `n` directly to `α`.
More concisely: For any type `α` with a `NonAssocRing` structure, the canonical homomorphism from `ℤ` to `α` coincides with the restriction of this homomorphism to `ℕ`.
|
Ring.intCast_negSucc
theorem Ring.intCast_negSucc : ∀ {R : Type u} [self : Ring R] (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1) := by
sorry
This theorem states that for any ring `R` and any natural number `n`, the canonical homomorphism from integers to `R` applied to the negative successor of `n` is equal to the negation of the canonical homomorphism from natural numbers to `R` applied to `n + 1`. In other words, the mapping of a negative integer to the ring `R` is just the negation of the mapping of its corresponding positive natural number (plus one) to the ring `R`.
More concisely: For any ring `R` and natural number `n`, the canonical homomorphism from integers to `R` maps `-(n + 1)` to `-(canonical_hom_nat_to_R (n + 1))`.
|
CommRing.mul_comm
theorem CommRing.mul_comm : ∀ {α : Type u} [self : CommRing α] (a b : α), a * b = b * a
This theorem states that for any commutative ring `α`, the multiplication operation is commutative. In other words, for any two elements `a` and `b` of the ring, the product of `a` and `b` is the same as the product of `b` and `a`. This is a basic property of commutative rings, reflecting that the order in which elements are multiplied does not change the result.
More concisely: For any commutative ring `α`, the multiplication is commutative, that is, `a * b = b * a` for all `a, b` in `α`.
|
HasDistribNeg.mul_neg
theorem HasDistribNeg.mul_neg : ∀ {α : Type u_1} [inst : Mul α] [self : HasDistribNeg α] (x y : α), x * -y = -(x * y)
This theorem asserts that the negation operation is right distributive over multiplication in a given algebraic structure. Specifically, for all elements `x` and `y` in a type `α` that has a multiplication operation and a negation operation, the product of `x` and the negation of `y` is equal to the negation of the product of `x` and `y`. In mathematical notation, it can be written as: `x * (-y) = -(x * y)`.
More concisely: For all types `α` with negation and multiplication operations, the negation of the product of two elements is equal to the product of their negations: `- (x * y) = x * (-y)`.
|
boole_mul
theorem boole_mul :
∀ {α : Type u_1} [inst : MulZeroOneClass α] (P : Prop) [inst_1 : Decidable P] (a : α),
(if P then 1 else 0) * a = if P then a else 0
This theorem is stating that for any type `α` that belongs to a `MulZeroOneClass` (a class of elements that supports multiplication, zero, and unit), and for any propositional `P`, which is decidable, and any element `a` of type `α`, the product of `a` and either 1 (if `P` is true) or 0 (if `P` is false) is equivalent to `a` if `P` is true, and 0 if `P` is false. In terms of mathematics, if `P` is true, then our multiplication result is `a`, otherwise it's 0.
More concisely: For any `α` in `MulZeroOneClass` and decidable proposition `P`, `a * (if P then 1 else 0) = a` if `P` is true, and `a * (if P then 1 else 0) = 0` if `P` is false.
|
NonUnitalNonAssocCommSemiring.mul_comm
theorem NonUnitalNonAssocCommSemiring.mul_comm :
∀ {α : Type u} [self : NonUnitalNonAssocCommSemiring α] (a b : α), a * b = b * a
This theorem states that in a non-unital, non-associative, commutative semiring (`NonUnitalNonAssocCommSemiring`), multiplication is commutative. That is, for any two elements `a` and `b` of this type, the result of multiplying `a` and `b` would be the same as multiplying `b` and `a`. In mathematical terms, this can be expressed as `a * b = b * a` for all `a`, `b` in the semiring.
More concisely: In a commutative non-unital, non-associative semiring, the multiplication operation is commutative.
|
RightDistribClass.right_distrib
theorem RightDistribClass.right_distrib :
∀ {R : Type u_1} [inst : Mul R] [inst_1 : Add R] [self : RightDistribClass R] (a b c : R),
(a + b) * c = a * c + b * c
The theorem `RightDistribClass.right_distrib` states that for any type `R` that has multiplication (`Mul R`) and addition (`Add R`) defined, and is a right distributive class (`RightDistribClass R`), multiplication distributes over addition from the right. This means that for all elements `a`, `b`, and `c` of `R`, the product of the sum of `a` and `b` with `c`, `(a + b) * c`, is equal to the sum of the product of `a` with `c` and the product of `b` with `c`, `a * c + b * c`. This corresponds to the standard distributive law in algebra.
More concisely: For any right distributive type `R` with multiplication and addition, `(a + b) * c = a * c + b * c` for all `a, b, c` in `R`.
|
Semiring.npow_zero
theorem Semiring.npow_zero : ∀ {α : Type u} [self : Semiring α] (x : α), Semiring.npow 0 x = 1
The theorem `Semiring.npow_zero` states that for any semiring `α` and any element `x` of `α`, if you raise `x` to the power of zero (interpreted in the natural numbers), you get the multiplicative identity of `α`, which is `1`. This is a formalization of the familiar mathematical concept that anything raised to the power of 0 equals 1, in the context of semirings.
More concisely: For any semiring `α` and its multiplicative identity `1`, for all `x` in `α`, `x^0 = 1`.
|
NonAssocRing.one_mul
theorem NonAssocRing.one_mul : ∀ {α : Type u_1} [self : NonAssocRing α] (a : α), 1 * a = a
This theorem states that for any given type `α`, which has a `NonAssocRing` structure, the number one (`1`) is a left neutral element for multiplication. This means that for any element `a` of type `α`, multiplying `1` with `a` from the left (i.e., `1 * a`) always yields `a`.
More concisely: For any type `α` with a `NonAssocRing` structure, the multiplicative identity `1` is a left identity for multiplication, i.e., `1 * a = a` for all `a` in `α`.
|
Ring.intCast_ofNat
theorem Ring.intCast_ofNat : ∀ {R : Type u} [self : Ring R] (n : ℕ), IntCast.intCast ↑n = ↑n
The theorem `Ring.intCast_ofNat` states that for any type `R` with a ring structure, the canonical homomorphism (mapping) from integers `ℤ` to `R`, when acting on natural numbers `ℕ` represented as integers, is the same as the canonical mapping from natural numbers `ℕ` to `R`. In simpler terms, when you take a natural number, treat it as an integer, and then cast it to the ring `R`, you get the same result as if you had cast the natural number directly to `R`. This brings a certain consistency to the way numbers are handled in mathematical structures in Lean 4.
More concisely: The theorem `Ring.intCast_ofNat` asserts that the natural number to ring homomorphism and the integer to ring homomorphism coincide for all rings `R`.
|
neg_mul_eq_neg_mul
theorem neg_mul_eq_neg_mul : ∀ {α : Type u} [inst : Mul α] [inst_1 : HasDistribNeg α] (a b : α), -(a * b) = -a * b := by
sorry
This theorem, named `neg_mul_eq_neg_mul`, states that for any type `α` that has a multiplication operation (denoted by `Mul α`) and a distributive negation operation (denoted by `HasDistribNeg α`), the negation of the product of two elements `a` and `b` (i.e., `-(a * b)`) is equal to the product of the negation of `a` and `b` (`-a * b`). This is a generalization of the property from number theory where the negation of a product is equivalent to multiplying one of the factors by negative one.
More concisely: For any type `α` with multiplication `Mul α` and distributive negation `HasDistribNeg α`, `-(a * b)` equals `-a * b` for all `a, b : α`.
|
Semiring.one_mul
theorem Semiring.one_mul : ∀ {α : Type u} [self : Semiring α] (a : α), 1 * a = a
This theorem states that one is a left neutral element for multiplication in a semiring. In other words, for any element 'a' in a semiring of type 'α', multiplying 'a' by one (1 * a) will always yield 'a'. This is a fundamental property in the algebraic structure called a semiring.
More concisely: In a semiring, for all elements 'a' of type 'α', one (1) acts as a left identity for multiplication, i.e., 1 * a = a.
|
Distrib.right_distrib
theorem Distrib.right_distrib : ∀ {R : Type u_1} [self : Distrib R] (a b c : R), (a + b) * c = a * c + b * c
This theorem states that multiplication is right distributive over addition in any type `R` that has a distributive law. In other words, for any elements `a`, `b`, and `c` of type `R`, the product of the sum of `a` and `b` with `c` is equal to the sum of the product of `a` with `c` and the product of `b` with `c`. This is essentially stating the well-known algebraic property `a * c + b * c = (a + b) * c`.
More concisely: For any type `R` with a distributive law and any elements `a`, `b`, and `c` of `R`, `(a + b) * c` equals the sum of `(a * c)` and `(b * c)`.
|
NonAssocSemiring.natCast_succ
theorem NonAssocSemiring.natCast_succ :
∀ {α : Type u} [self : NonAssocSemiring α] (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
This theorem states that for every natural number `n`, the canonical map from natural numbers `ℕ` to a non-associative semiring `α` preserves the addition operation, specifically the increment operation. In other words, when we increment `n` by `1` and then apply the canonical map, it is the same as applying the canonical map to `n` first and then incrementing the result by `1`. This property is a characteristic of homomorphisms, therefore the theorem asserts the homomorphism property of the canonical map `ℕ → α` for non-associative semirings.
More concisely: For every natural number `n` and non-associative semiring `α`, the canonical map from `ℕ` to `α` preserves the increment operation, i.e., `canonicalMap (n + 1) = canonicalMap n + 1`.
|
NonUnitalNonAssocCommRing.mul_comm
theorem NonUnitalNonAssocCommRing.mul_comm :
∀ {α : Type u} [self : NonUnitalNonAssocCommRing α] (a b : α), a * b = b * a
This theorem states that in any commutative non-unital, non-associative ring (where multiplication is not required to be associative and there may not be a multiplicative identity), multiplication is a commutative operation. In other words, for any two elements `a` and `b` in such a ring, the product `a * b` is equal to the product `b * a`.
More concisely: In any commutative non-unital ring, the multiplication is commutative, i.e., for all elements `a` and `b`, `a * b = b * a`.
|
NonUnitalNonAssocRing.left_distrib
theorem NonUnitalNonAssocRing.left_distrib :
∀ {α : Type u} [self : NonUnitalNonAssocRing α] (a b c : α), a * (b + c) = a * b + a * c
The theorem `NonUnitalNonAssocRing.left_distrib` is a statement in the context of NonUnitalNonAssocRings, which are particular mathematical structures. The theorem states that, for any three elements 'a', 'b', and 'c' of a NonUnitalNonAssocRing 'α', the operation of multiplication is left-distributive over addition. In other words, multiplying 'a' by the sum of 'b' and 'c' ('a' * (b + c)) is equivalent to the sum of 'a' multiplied by 'b' and 'a' multiplied by 'c' (a * b + a * c).
More concisely: For any elements a, b, and c in a NonUnitalNonAssocRing α, a * (b + c) = a * b + a * c.
|
add_mul
theorem add_mul :
∀ {R : Type x} [inst : Mul R] [inst_1 : Add R] [inst_2 : RightDistribClass R] (a b c : R),
(a + b) * c = a * c + b * c
This theorem, `add_mul`, is an alias of `right_distrib`, and states that for any given type `R` which has multiplication and addition operations, and also satisfies the property of right distribution (as specified by `RightDistribClass`), the multiplication of the sum of two elements `a` and `b` with a third element `c` is equal to the sum of the product of `a` and `c` and the product of `b` and `c`. In mathematical terms, it asserts the distributive law: $(a + b) * c = a * c + b * c$.
More concisely: The theorem asserts that for any type `R` with right-distributive multiplication and addition, we have $(a + b) \cdot c = a \cdot c + b \cdot c$.
|
NonUnitalNonAssocSemiring.left_distrib
theorem NonUnitalNonAssocSemiring.left_distrib :
∀ {α : Type u} [self : NonUnitalNonAssocSemiring α] (a b c : α), a * (b + c) = a * b + a * c
This theorem states that multiplication is left distributive over addition in the context of a non-unital non-associative semiring. Specifically, for any elements `a`, `b`, and `c` in this semiring, the product of `a` and the sum of `b` and `c` (`a * (b + c)`) is equal to the sum of the product of `a` and `b` and the product of `a` and `c` (`a * b + a * c`).
More concisely: In a non-unital non-associative semiring, the multiplication of an element with the sum of two other elements is equal to the sum of the products of that element with each of the other two elements. (a * (b + c) = a * b + a * c)
|
neg_mul_neg
theorem neg_mul_neg : ∀ {α : Type u} [inst : Mul α] [inst_1 : HasDistribNeg α] (a b : α), -a * -b = a * b
This theorem states that for any type `α` that has a multiplication operation and a negation operation, the product of the negation of `a` and the negation of `b` is equal to the product of `a` and `b`. In mathematical notation, it's saying that `(-a) * (-b) = a * b` for all elements `a` and `b` of type `α`.
More concisely: For any type `α` with multiplication and negation operations, the negation of their products equals the product of negations: `(-a) * (-b) = a * b`.
|
right_distrib
theorem right_distrib :
∀ {R : Type x} [inst : Mul R] [inst_1 : Add R] [inst_2 : RightDistribClass R] (a b c : R),
(a + b) * c = a * c + b * c
This theorem states that, for any type `R` that has multiplication (`Mul R`), addition (`Add R`), and satisfies the right distribution property (`RightDistribClass R`), the multiplication of the sum of two elements `a` and `b` with a third element `c` is equal to the sum of the products of `a` and `c` and `b` and `c`. In mathematical notation, it states that `(a + b) * c = a * c + b * c` for all `a`, `b`, `c` in `R`. This is known as the right distributive property of multiplication over addition.
More concisely: For any type `R` with multiplication and addition, and right distributive property, `(a + b) * c = a * c + b * c` for all `a, b, c` in `R`.
|
NonAssocRing.mul_one
theorem NonAssocRing.mul_one : ∀ {α : Type u_1} [self : NonAssocRing α] (a : α), a * 1 = a
This theorem states that for any nonassociative ring `α`, one (`1`) is a right neutral element with respect to the multiplication operation. That is, for any element `a` in `α`, the product of `a` and one is `a` itself. In mathematical notation, this could be written as `∀a∈α, a * 1 = a`.
More concisely: For any nonassociative ring `α`, the multiplicative identity `1` is a right identity for every element `a` in `α`, that is, `a * 1 = a`.
|
mul_sub
theorem mul_sub : ∀ {α : Type u} [inst : NonUnitalNonAssocRing α] (a b c : α), a * (b - c) = a * b - a * c
This is an alias of the theorem `mul_sub_left_distrib`. It states that for any type `α` that forms a `NonUnitalNonAssocRing` (a mathematical structure similar to a ring but without the requirement of having a multiplicative identity or associative multiplication), and for any three elements `a`, `b`, and `c` of that type, the property `a * (b - c) = a * b - a * c` holds. In mathematical terms, this expresses the left distributivity of multiplication over subtraction in such a structure.
More concisely: For any non-unital, non-associative ring `α`, the multiplication is left distributive over subtraction: `a * (b - c) = a * b - a * c`.
|
NonUnitalNonAssocSemiring.right_distrib
theorem NonUnitalNonAssocSemiring.right_distrib :
∀ {α : Type u} [self : NonUnitalNonAssocSemiring α] (a b c : α), (a + b) * c = a * c + b * c
This theorem states that multiplication is right distributive over addition in a non-unital non-associative semiring. Specifically, for any type `α` that forms a non-unital non-associative semiring and for any elements `a`, `b`, and `c` of this type, 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 property can be written as `(a + b) * c = a * c + b * c`.
More concisely: In a non-unital non-associative semiring, the multiplication is right distributive over addition, that is, `(a + b) * c = a * c + b * c` for all elements `a`, `b`, and `c`.
|
NonUnitalNonAssocRing.zero_mul
theorem NonUnitalNonAssocRing.zero_mul : ∀ {α : Type u} [self : NonUnitalNonAssocRing α] (a : α), 0 * a = 0
This theorem states that zero is a left absorbing element for multiplication in the context of a non-unital, non-associative ring. Specifically, for any element `a` in this non-unital, non-associative ring, the product of zero and `a` is always zero.
More concisely: In a non-unital, non-associative ring, zero multiplied with any element is equal to zero.
|
NonUnitalNonAssocSemiring.zero_mul
theorem NonUnitalNonAssocSemiring.zero_mul : ∀ {α : Type u} [self : NonUnitalNonAssocSemiring α] (a : α), 0 * a = 0
This theorem states that zero is a left absorbing element for multiplication in a non-unital, non-associative semiring. In other words, for any element "a" from a non-unital, non-associative semiring of any type "α", when you multiply "a" by zero (with zero on the left), the result will always be zero.
More concisely: For any non-unital, non-associative semiring type α and any element a in α, a * 0 = 0 holds.
|
NonUnitalCommSemiring.mul_comm
theorem NonUnitalCommSemiring.mul_comm : ∀ {α : Type u} [self : NonUnitalCommSemiring α] (a b : α), a * b = b * a := by
sorry
This theorem states that in a non-unital commutative semi-ring, the operation of multiplication is commutative. That is, for any two elements `a` and `b` of a non-unital commutative semi-ring `α`, the product `a * b` is equal to the product `b * a`. This means that the order in which the elements are multiplied does not affect the outcome in such a semi-ring.
More concisely: In a commutative semi-ring without identity, multiplication is commutative.
|
mul_two
theorem mul_two : ∀ {α : Type u} [inst : NonAssocSemiring α] (n : α), n * 2 = n + n
This theorem, `mul_two`, states that for any non-associative semiring `α` and for any element `n` in that semiring, multiplying `n` by 2 is equivalent to adding `n` to itself. Here, a non-associative semiring is a mathematical structure that extends the concept of a semiring by not requiring the multiplication operation to be associative.
More concisely: For any non-associative semiring `α` and element `n` in `α`, `n` multiplied by 2 is equivalent to `n` added to itself. (Or, `2 * n = n + n` in infix notation.)
|
mul_sub_right_distrib
theorem mul_sub_right_distrib :
∀ {α : Type u} [inst : NonUnitalNonAssocRing α] (a b c : α), (a - b) * c = a * c - b * c
This theorem states that for any type `α` that forms a `NonUnitalNonAssocRing`, the operation of multiplication distributes over subtraction from the right. Specifically, if you have three elements `a`, `b`, and `c` of type `α`, the product of the difference of `a` and `b` with `c` equals the difference of the product of `a` and `c` and the product of `b` and `c`. In LaTeX mathematics, this would be written as $(a - b) * c = a * c - b * c$.
More concisely: For any type `α` that is a non-unital non-associative ring, the distribution law holds for multiplication and subtraction: $(a - b) \cdot c = a \cdot c - b \cdot c$.
|
HasDistribNeg.neg_mul
theorem HasDistribNeg.neg_mul : ∀ {α : Type u_1} [inst : Mul α] [self : HasDistribNeg α] (x y : α), -x * y = -(x * y)
This theorem, `HasDistribNeg.neg_mul`, states that negation is left distributive over multiplication in any type `α` that has multiplication (`Mul α`) and a distributable negation operation (`HasDistribNeg α`). In other words, for any elements `x` and `y` of type `α`, the product of the negation of `x` and `y` is equal to the negation of the product of `x` and `y`. Mathematically, it's saying that for all `x` and `y`, `-x * y` equals `-(x * y)`.
More concisely: For any type `α` with multiplication and distributive negation, `- (x * y) = (-x) * y` for all `x, y` in `α`.
|
NonAssocRing.natCast_succ
theorem NonAssocRing.natCast_succ :
∀ {α : Type u_1} [self : NonAssocRing α] (n : ℕ), NatCast.natCast (n + 1) = NatCast.natCast n + 1
The theorem `NonAssocRing.natCast_succ` states that for any non-associative ring α and any natural number n, the canonical mapping from natural numbers to the ring α preserves addition. In other words, the operation of adding 1 to a natural number n and then applying the map is the same as applying the map to n and then adding 1 in the ring α. This effectively means that the canonical map `ℕ → R` behaves like a homomorphism.
More concisely: For any non-associative ring α and natural number n, the canonical map from ℕ to α preserves addition: n + 1 → (n : α) + 1 = (n + 1 : α).
|
mul_boole
theorem mul_boole :
∀ {α : Type u_1} [inst : MulZeroOneClass α] (P : Prop) [inst_1 : Decidable P] (a : α),
(a * if P then 1 else 0) = if P then a else 0
This theorem, `mul_boole`, states that for any type `α` that belongs to `MulZeroOneClass` (meaning `α` has multiplication, and has elements designated as zero and one), along with a proposition `P` and an element `a` of `α`, the product of `a` and `1` (if `P` is true) or `0` (if `P` is false) is equal to `a` (if `P` is true) or `0` (if `P` is false). Essentially, this theorem captures the idea that multiplicative identity and zero in a `MulZeroOneClass` work as expected in relation to a decidable proposition.
More concisely: For any type `α` in `MulZeroOneClass` and proposition `P`: `(1 * a) = a <=> P` and `(0 * a) = 0 <=> ≠P`, where `<=>` denotes logical equivalence.
|
mul_add_one
theorem mul_add_one :
∀ {α : Type u} [inst : Add α] [inst_1 : MulOneClass α] [inst_2 : LeftDistribClass α] (a b : α),
a * (b + 1) = a * b + a
This theorem, called `mul_add_one`, states that for any type `α` that is equipped with addition, multiplication, and the property that multiplication is left-distributive over addition, the multiplication of an element `a` with the sum of an element `b` and one is equal to the sum of `a` multipled by `b` and `a`. In other words, it's proving the principle of distribution for multiplication over addition, specifically when adding one, i.e., `a * (b + 1) = a * b + a`.
More concisely: For any type `α` with additions and multiplications satisfying left-distributivity, `a * (b + 1) = a * b + a`.
|
bit0_eq_two_mul
theorem bit0_eq_two_mul : ∀ {α : Type u} [inst : NonAssocSemiring α] (n : α), bit0 n = 2 * n
The theorem `bit0_eq_two_mul` states that for any type `α` that is an instance of a non-associative semiring (a structure with two binary operations that generalizes many algebraic structures such as rings, fields, etc.), the function `bit0` applied to any element `n` of `α` is equal to 2 multiplied by `n`. The `bit0` function is defined as the sum of `n` with itself, so effectively, this theorem asserts that doubling `n` through addition is the same as multiplying `n` by 2.
More concisely: For any non-associative semiring type `α`, the function `bit0` on `α` (defined as the sum of an element with itself) equals the multiplication by 2.
|
NonAssocSemiring.one_mul
theorem NonAssocSemiring.one_mul : ∀ {α : Type u} [self : NonAssocSemiring α] (a : α), 1 * a = a
This theorem states that for any non-associative semiring (a mathematical structure with two binary operations which we can think of as addition and multiplication), one (1) is a left neutral element for multiplication. In other words, for any element 'a' in this semiring, multiplying 'a' by one (1) on the left side (i.e., 1 * a) results in 'a'.
More concisely: For any non-associative semiring, one (1) acts as a left identity for multiplication, i.e., 1 * a = a for all elements a in the semiring.
|
Distrib.left_distrib
theorem Distrib.left_distrib : ∀ {R : Type u_1} [self : Distrib R] (a b c : R), a * (b + c) = a * b + a * c
The theorem `Distrib.left_distrib` states that for any type `R` that has a distributive property (defined by the typeclass `Distrib`), multiplication is left-distributive over addition. More specifically, for any three elements `a`, `b`, and `c` of type `R`, the product of `a` and the sum of `b` and `c` is equal to the sum of the products of `a` and `b` and of `a` and `c`. This is often written mathematically as `a * (b + c) = a * b + a * c`.
More concisely: For any type `R` with distributive multiplication and elements `a`, `b`, and `c`, `a * (b + c) = a * b + a * c`.
|
NonUnitalNonAssocRing.right_distrib
theorem NonUnitalNonAssocRing.right_distrib :
∀ {α : Type u} [self : NonUnitalNonAssocRing α] (a b c : α), (a + b) * c = a * c + b * c
This theorem states that multiplication is right distributive over addition in a non-unital non-associative ring. Specifically, for any three elements `a`, `b`, and `c` of any type `α`, which forms a non-unital non-associative ring, the product of the sum of `a` and `b` with `c` equals the sum of the product of `a` with `c` and the product of `b` with `c`. In mathematical terms, this is expressed as `(a + b) * c = a * c + b * c`.
More concisely: In a non-unital non-associative ring, the multiplication of the sum of two elements is distributive over the multiplication of each element with a third. That is, `(a + b) * c = a * c + b * c` for all `a`, `b`, and `c` of type `α`.
|
mul_neg_one
theorem mul_neg_one : ∀ {α : Type u} [inst : MulOneClass α] [inst_1 : HasDistribNeg α] (a : α), a * -1 = -a
This theorem states that, for any element `a` of a ring-type `α`, the product of `a` and the additive inverse of one equals the additive inverse of `a`. In mathematical terms, for all `a` in a ring `α`, `a * -1 = -a`. This theorem holds for all types `α` that have a multiplication operation (`MulOneClass α`) and an additive inverse operation (`HasDistribNeg α`).
More concisely: For any element `a` in a ring `α` with additive inverse, `a * (-1) = -(a)`.
|
neg_mul_eq_mul_neg
theorem neg_mul_eq_mul_neg : ∀ {α : Type u} [inst : Mul α] [inst_1 : HasDistribNeg α] (a b : α), -(a * b) = a * -b := by
sorry
This theorem states that for any type `α` that supports multiplication and negation operations, negating the product of two elements `a` and `b` (i.e., `-(a * b)`) is equivalent to multiplying `a` by the negation of `b` (i.e., `a * -b`). This is a common property in mathematics, especially in the field of ring theory.
More concisely: For any type `α` with multiplicative and negation operations, `-(a * b) = a * -b` for all `a, b : α`.
|
ite_mul
theorem ite_mul :
∀ {α : Type u_1} [inst : Mul α] (P : Prop) [inst_1 : Decidable P] (a b c : α),
(if P then a else b) * c = if P then a * c else b * c
This theorem, named `ite_mul`, states that for any type `α` that has a multiplication operation defined, a proposition `P` that can be decided (either true or false), and three elements `a`, `b`, `c` of the type `α`, the product of `c` and the element chosen by the if-then-else expression based on `P` is equal to the element chosen by the if-then-else expression based on `P` from the products `a * c` and `b * c`. In other words, regardless of whether `P` is true or false, the multiplication operation can be distributed over the if-then-else expression.
More concisely: For any type `α` with multiplication and any proposition `P` and elements `a, b, c` in `α`, `(a * c) * iff h : P then c else b = iff h then a * c else b * c`.
|
NonUnitalNonAssocSemiring.mul_zero
theorem NonUnitalNonAssocSemiring.mul_zero : ∀ {α : Type u} [self : NonUnitalNonAssocSemiring α] (a : α), a * 0 = 0
The theorem `NonUnitalNonAssocSemiring.mul_zero` states that for any non-unital, non-associative semiring, multiplying any element of the semiring by zero results in zero. In other words, zero acts as a right absorbing element for the multiplication operation in such a semiring. This is a fundamental property of multiplication in many algebraic structures.
More concisely: In a non-unital, non-associative semiring, for all elements x, x * 0 = 0.
|
neg_mul
theorem neg_mul : ∀ {α : Type u} [inst : Mul α] [inst_1 : HasDistribNeg α] (a b : α), -a * b = -(a * b)
This theorem, `neg_mul`, states that for all types `α` equipped with a multiplication operation (`Mul α`) and a distributive negation operation (`HasDistribNeg α`), the product of the negation of `a` and `b` is equal to the negation of the product of `a` and `b`. In mathematical terms, this can be expressed as `-a * b = -(a * b)`. This essentially captures the property of the number system where multiplying a negative number with a positive number yields the same result as negating the product of the positive counterparts.
More concisely: For all types `α` with multiplication `Mul α` and distributive negation `HasDistribNeg α`, `- (a : α) * b : α = - (a : α * b : α)`.
|
left_distrib
theorem left_distrib :
∀ {R : Type x} [inst : Mul R] [inst_1 : Add R] [inst_2 : LeftDistribClass R] (a b c : R),
a * (b + c) = a * b + a * c
This is a theorem stating the property of left distributivity in a certain algebraic structure. Specifically, for any type `R` that has operations of multiplication (`Mul R`) and addition (`Add R`) and follows the left distributive law (`LeftDistribClass R`), the theorem states that for any three elements `a`, `b`, and `c` of `R`, the result of multiplying `a` by the sum of `b` and `c` is equal to the sum of `a` multiplied by `b` and `a` multiplied by `c`. In mathematical terms, this is the well-known property `a * (b + c) = a * b + a * c`.
More concisely: For any element `a` in a commutative ring `R` with one and multiplicative identity, `a * (b + c) = a * b + a * c` holds for all `b, c` in `R`.
|
NonUnitalNonAssocRing.mul_zero
theorem NonUnitalNonAssocRing.mul_zero : ∀ {α : Type u} [self : NonUnitalNonAssocRing α] (a : α), a * 0 = 0
This theorem states that zero is a right absorbing element for the operation of multiplication in a non-unital, non-associative ring. In other words, for any element 'a' in a non-unital, non-associative ring 'α', when 'a' is multiplied by zero, the result is always zero.
More concisely: In a non-unital, non-associative ring, the multiplicative identity has no effect on any element 'a': a * 0 = 0.
|
NonUnitalRing.mul_assoc
theorem NonUnitalRing.mul_assoc : ∀ {α : Type u_1} [self : NonUnitalRing α] (a b c : α), a * b * c = a * (b * c) := by
sorry
This theorem states that multiplication is associative in a non-unital ring. Specifically, for any non-unital ring of a certain type `α`, and any three elements `a`, `b`, and `c` from this ring, the result of multiplying `a` with the product of `b` and `c` (i.e., `a * (b * c)`) is the same as the result of first multiplying `a` and `b`, and then multiplying the result with `c` (i.e., `(a * b) * c`). This property is fundamental to the operation of multiplication in rings.
More concisely: In a non-unital ring, the associativity of multiplication holds: (a * (b * c)) = ((a * b) * c) for all elements a, b, and c from the ring.
|
NonAssocRing.natCast_zero
theorem NonAssocRing.natCast_zero : ∀ {α : Type u_1} [self : NonAssocRing α], NatCast.natCast 0 = 0
The theorem `NonAssocRing.natCast_zero` states that for any type `α` which forms a non-associative ring, the canonical map from natural numbers `ℕ` to `α` sends `0` in the natural numbers to `0` in `α`. In other words, when `0` from the set of natural numbers is casted into the non-associative ring `α`, it will always be mapped to `0` in `α`.
More concisely: For any non-associative ring `α`, the canonical map from natural numbers to `α` maps the natural number `0` to the additive identity `0` in `α`.
|