Commute.zpow_right
theorem Commute.zpow_right : ∀ {G : Type w} [inst : Group G] {a b : G}, Commute a b → ∀ (m : ℤ), Commute a (b ^ m) := by
sorry
This theorem states that for any type `G` that forms a group, given two elements `a` and `b` of `G` that commute with each other (i.e., `a * b = b * a`), and given any integer `m`, the element `a` will also commute with `b` raised to the power of `m` (i.e., `a * (b ^ m) = (b ^ m) * a`).
More concisely: If `a` and `b` are group elements that commute, then `a` commutes with `b` raised to any power.
|
AddCommute.zsmul_add
theorem AddCommute.zsmul_add :
∀ {α : Type u_1} [inst : SubtractionMonoid α] {a b : α}, AddCommute a b → ∀ (i : ℤ), i • (a + b) = i • a + i • b
The theorem `AddCommute.zsmul_add` states that for any type `α` that is a subtraction monoid, and for any elements `a` and `b` of type `α` that commute under addition (i.e., `a + b = b + a`), the integer scaling of the sum equals the sum of the integer scalings. More specifically, for any integer `i`, `i` times the sum of `a` and `b` equals `i` times `a` plus `i` times `b`. This generalizes the distributive property of multiplication over addition to the context of subtraction monoids and integer scalings.
More concisely: For any subtraction monoid type `α` and commuting elements `a` and `b` of type `α`, the scaling of their sum with an integer `i` equals the scaling of `a` with `i` plus the scaling of `b` with `i`.
|
zpow_mul'
theorem zpow_mul' : ∀ {α : Type u_1} [inst : DivisionMonoid α] (a : α) (m n : ℤ), a ^ (m * n) = (a ^ n) ^ m
This theorem states that for any type `α` that forms a division monoid, and for any element `a` of this type, along with integers `m` and `n`, the power of `a` raised to the product of `m` and `n` is equal to `a` raised to the power of `n`, which is in turn raised to the power of `m`. In LaTeX terms, this would read: \(a^{mn} = (a^n)^m\).
More concisely: For any element `a` of a type `α` forming a division monoid and integers `m` and `n`, `a^(mn) = (a^n)^m`.
|
neg_zsmul
theorem neg_zsmul : ∀ {α : Type u_1} [inst : SubtractionMonoid α] (a : α) (n : ℤ), -n • a = -(n • a)
This theorem, `neg_zsmul`, states that for any type `α` that forms a SubtractionMonoid (an algebraic structure with an operation that combines any two elements to form a third and an operation that subtracts one element from another), and any element `a` of type `α`, the operation of scalar multiplication by the negative of an integer `n` applied to `a` is equal to the negation of the result of scalar multiplication by `n` applied to `a`. In simpler terms, it asserts that the negative of `n` times `a` equals to the negative of (`n` times `a`).
More concisely: For any type `α` that forms a SubtractionMonoid and any element `a` of type `α`, we have -(n * a) = n \* (-a) for any integer `n`.
|
pow_two
theorem pow_two : ∀ {M : Type u} [inst : Monoid M] (a : M), a ^ 2 = a * a
This theorem, `pow_two`, states that for any type `M` that is a monoid (an algebraic structure with a single associative binary operation and an identity element), the square of any element `a` of `M` (noted as `a ^ 2`) is equal to the product of `a` with itself (`a * a`). This is a fundamental property of squaring in the context of monoids.
More concisely: For any monoid `M` and its element `a`, `a ^ 2 = a * a`.
|
inv_pow
theorem inv_pow : ∀ {α : Type u_1} [inst : DivisionMonoid α] (a : α) (n : ℕ), a⁻¹ ^ n = (a ^ n)⁻¹
This theorem states that for any given type `α` which forms a division monoid, for any element `a` of type `α` and any natural number `n`, the inverse of `a` raised to the power of `n` is equal to the inverse of `a` raised to the power of `n`. In mathematical terms, it can be expressed as `(a⁻¹) ^ n = (a ^ n)⁻¹`. This theorem holds for all division monoids, a kind of algebraic structure that includes operations of multiplication and inverse.
More concisely: For any division monoid type `α` and its element `a`, the inverse of `a` raised to the power of a natural number `n` equals the inverse of `a` raised to the power of `n`, i.e., `(a⁻¹) ^ n = (a ^ n)⁻¹`.
|
one_nsmul
theorem one_nsmul : ∀ {A : Type y} [inst : AddMonoid A] (a : A), 1 • a = a
This theorem states that for any type `A` that is an additive monoid, the operation of scalar multiplication of any element `a` of type `A` by 1 results in `a` itself. In mathematical terms, it's saying that in any additive monoid, multiplying an element by the scalar 1 does not change the element, which mirrors the well-known property in regular arithmetic that any number multiplied by 1 remains the same.
More concisely: For any additive monoid type `A` and its element `a`, 1 * a = a.
|
zpow_add
theorem zpow_add : ∀ {G : Type w} [inst : Group G] (a : G) (m n : ℤ), a ^ (m + n) = a ^ m * a ^ n
This theorem, `zpow_add`, states that for any type `G` that forms a group, for any element `a` of `G`, and for any two integers `m` and `n`, the power of `a` raised to the sum of `m` and `n` is equal to the product of `a` raised to the power of `m` and `a` raised to the power of `n`. In mathematical terms, it expresses the rule that $a^{(m+n)} = a^m * a^n$ for all `a` in `G` and all integers `m` and `n`.
More concisely: For any group `G` and elements `a` in `G` and integers `m` and `n`, `a^(m + n) = a^m * a^n`.
|
zsmul_sub
theorem zsmul_sub : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b : α) (n : ℤ), n • (a - b) = n • a - n • b
This theorem states that for any type `α` that forms a commutative monoid under subtraction, and for any elements `a` and `b` of this type and any integer `n`, the operation of scaling (multiplying) the difference between `a` and `b` by `n` is equivalent to subtracting the scaled `b` from the scaled `a`. In mathematical terms, it asserts that $n \cdot (a - b) = n \cdot a - n \cdot b$ for all `a`, `b` in `α` and integer `n`.
More concisely: For any commutative monoid `α` under subtraction and integers `n`, `a`, `b` in `α`, we have `n * (a - b) = n * a - n * b`.
|
zsmul_induction_right
theorem zsmul_induction_right :
∀ {G : Type w} [inst : AddGroup G] {g : G} {P : G → Prop},
P 0 → (∀ (a : G), P a → P (a + g)) → (∀ (a : G), P a → P (a + -g)) → ∀ (n : ℤ), P (n • g)
This theorem states that, in order to prove a certain property holds for all multiples of a given element `g` in an additive group `G`, it's enough to show that this property is preserved when `g` or `-g` is added on the right to any element `a` that already has the property. The property must also hold for the zero element. This rule is specifically for additive subgroups generated by a single element; for those generated by more than one element, refer to the theorem `AddSubgroup.closure_induction_right`. The property is represented as a predicate `P : G → Prop`. The multiples of `g` are represented as `n • g`, where `n` is an integer.
More concisely: If a predicate `P` is closed under addition with a fixed group element `g` from an additive group `G` and `P` holds for the zero element, then `P` holds for all multiples of `g` in `G`.
|
add_zsmul
theorem add_zsmul : ∀ {G : Type w} [inst : AddGroup G] (a : G) (m n : ℤ), (m + n) • a = m • a + n • a
This theorem, `add_zsmul`, in Lean 4 states that for any type `G` that has an addition group structure, and any element `a` of `G` and any two integers `m` and `n`, the operation of scalar multiplication by (`m + n`) on `a` is equal to the sum of the operations of scalar multiplication by `m` on `a` and scalar multiplication by `n` on `a`. In other words, the scalar multiplication distributes over integer addition in the context of addition groups.
More concisely: For any additive group `G` and elements `a` in `G` and integers `m` and `n`, the scalar multiplication `(m + n) * a` equals the sum `(m * a) + (n * a)`.
|
div_zpow
theorem div_zpow : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b : α) (n : ℤ), (a / b) ^ n = a ^ n / b ^ n := by
sorry
This theorem states that for any type `α` which has a Division Commutative Monoid structure, and for any two elements `a` and `b` of this type, and any integer `n`, the nth power of the division of `a` and `b` is equal to the division of `a` to the power of `n` and `b` to the power of `n`. In mathematical terms, for any $\alpha$ which is a Division Commutative Monoid, $(a / b)^n = a^n / b^n$ for all $a$, $b$ in $\alpha$ and for all integers $n$.
More concisely: For any Division Commutative Monoid `α`, `(a / b)^n = a^n / b^n` for all `a, b ∈ α` and `n ∈ ℤ`.
|
zpow_add_one
theorem zpow_add_one : ∀ {G : Type w} [inst : Group G] (a : G) (n : ℤ), a ^ (n + 1) = a ^ n * a
This theorem states that for any group `G`, any element `a` of `G`, and any integer `n`, raising `a` to the power of `n + 1` is the same as multiplying `a` raised to the power `n` by `a`. This is a generalization of the familiar power rule from elementary arithmetic, but applied to groups and integer exponents.
More concisely: For any group `G`, any of its element `a`, and any integer `n`, the power `a^(n+1)` equals the product `a^n * a`.
|
zsmul_induction_left
theorem zsmul_induction_left :
∀ {G : Type w} [inst : AddGroup G] {g : G} {P : G → Prop},
P 0 → (∀ (a : G), P a → P (g + a)) → (∀ (a : G), P a → P (-g + a)) → ∀ (n : ℤ), P (n • g)
This theorem, `zsmul_induction_left`, states that for any type `G` that is an additive group, and for any property `P` and element `g` of `G`, if `P` holds for the zero element, and if `P` is preserved under the operation of adding `g` and `-g` from the left to any element `a` for which `P` holds, then `P` will hold for all integer multiples of `g`. This is an induction principle on integers that helps in showing a property holds for all multiples of a given element in an additive group. For additive subgroups generated by more than one element, one should refer to `AddSubgroup.closure_induction_left`.
More concisely: If `G` is an additive group, `P` is a property that holds for the zero element and is preserved under left multiplication by `g`, then `P` holds for all integer multiples of `g` in `G`.
|
zpow_one
theorem zpow_one : ∀ {G : Type w} [inst : DivInvMonoid G] (a : G), a ^ 1 = a
This theorem, `zpow_one`, states that for any type `G` that has an instance of the `DivInvMonoid` typeclass, the first power of any element `a` of `G` is equal to `a` itself. In mathematical terms, this corresponds to the common rule a^1 = a for any a in some division-inverse monoid.
More concisely: For any type `G` with `DivInvMonoid` instance, the power operation raises any element `a` in `G` to the first power, yielding `a` itself. (In mathematical notation: ∀ (G : Type) [DivInvMonoid G], ∀ (a : G), a ^ 1 = a)
|
mul_zsmul
theorem mul_zsmul : ∀ {α : Type u_1} [inst : SubtractionMonoid α] (a : α) (m n : ℤ), (m * n) • a = m • n • a
This theorem, `mul_zsmul`, states that for any type `α` that is a subtraction monoid, and any element 'a' of this type along with two integers 'm' and 'n', the operation of scalar multiplication of 'a' by the product of 'm' and 'n' is equivalent to first scalar multiplying 'a' by 'n' and then scalar multiplying the result by 'm'. That is, `(m * n) • a` is equal to `m • n • a`. This theorem illustrates an important property of integers and subtraction monoids, essentially a kind of associativity that involves integer multiplication and scalar multiplication.
More concisely: For any subtraction monoid type `α` and elements `a`, `m`, and `n`, `(m * n) • a` equals `m • (n • a)`.
|
AddCommute.add_nsmul
theorem AddCommute.add_nsmul :
∀ {M : Type u} [inst : AddMonoid M] {a b : M}, AddCommute a b → ∀ (n : ℕ), n • (a + b) = n • a + n • b
This theorem states that for any types `M` that is an additive monoid and any two elements `a` and `b` of `M` that commute with respect to addition (`AddCommute a b`), and for any natural number `n`, the n-fold scalars of the sum of `a` and `b` (`n • (a + b)`) equals to the sum of the n-fold scalars of `a` and `b` (`n • a + n • b`). In other words, the process of scaling and addition can be interchanged when `a` and `b` are commutative with respect to addition.
More concisely: For any commuting additive monoid elements `a` and `b` and natural number `n`, the scalars `n • a` and `n • b` commute, and `n • (a + b)` equals the sum `n • a + n • b`.
|
neg_nsmul
theorem neg_nsmul : ∀ {α : Type u_1} [inst : SubtractionMonoid α] (a : α) (n : ℕ), n • -a = -(n • a)
This theorem states that for all types `α` (assuming `α` is a subtraction monoid), for any element `a` of `α` and any natural number `n`, the negation of `a` n-times scaled is equal to the negation of `a` scaled n-times. In other words, it expresses that scaling a negative number `n` times is equivalent to negating the number first and then scaling it `n` times. This is a property of subtraction monoids, a kind of algebraic structure.
More concisely: For any subtraction monoid type `α` and element `a` in `α`, negating and scaling `a` by a natural number `n` is equivalent: `-(a * n) = (-a) * n`.
|
nsmul_eq_mod_nsmul
theorem nsmul_eq_mod_nsmul :
∀ {M : Type u_2} [inst : AddMonoid M] {x : M} (m : ℕ) {n : ℕ}, n • x = 0 → m • x = (m % n) • x
This theorem states that for any type `M` that forms an additive monoid and for any element `x` of this type `M`, if the `n`-fold addition of `x` equals zero (denoted as `n • x = 0`), then the `m`-fold addition of `x` is equal to the `(m mod n)`-fold addition of `x` (denoted as `m • x = (m % n) • x`). In other words, if adding `x` to itself `n` times results in zero, then adding `x` to itself `m` times is equivalent to adding `x` to itself `m mod n` times.
More concisely: If `M` is an additive monoid and `x` is an element of `M` such that `n • x = 0`, then `m • x = (m % n) • x` for all natural numbers `m` and `n`.
|
pow_mul'
theorem pow_mul' : ∀ {M : Type u} [inst : Monoid M] (a : M) (m n : ℕ), a ^ (m * n) = (a ^ n) ^ m
This theorem states that for any given type `M` that forms a monoid, for any element `a` of type `M`, and any two natural numbers `m` and `n`, the power of `a` raised to the product of `m` and `n` is equal to the power of `a` raised to `n`, and then that result raised to `m`. In more mathematical terms, it's saying that \(a^{m*n} = (a^n)^m\) for any monoid element `a` and natural numbers `m` and `n`.
More concisely: For any monoid `M` and element `a` in `M`, and natural numbers `m` and `n`, the equality `a^(mn) = (a^n)^m` holds.
|
zpow_induction_left
theorem zpow_induction_left :
∀ {G : Type w} [inst : Group G] {g : G} {P : G → Prop},
P 1 → (∀ (a : G), P a → P (g * a)) → (∀ (a : G), P a → P (g⁻¹ * a)) → ∀ (n : ℤ), P (g ^ n)
This theorem states that, for a given group `G`, element `g` from `G`, and a property `P` applicable to elements of `G`, if `P` holds for the identity element `1`, and if `P` holds for an element `a`, it also holds for `g * a` and `g⁻¹ * a`, then it can be concluded that `P` holds for all integer powers of `g`. For subgroups generated by more than one element, one can refer to `Subgroup.closure_induction_left`.
More concisely: If a property `P` holds for the identity element and for every element `a` in a group `G`, then `P` holds for all integer powers of any element `g` in `G`.
|
zsmul_neg'
theorem zsmul_neg' : ∀ {α : Type u_1} [inst : SubtractionMonoid α] (a : α) (n : ℤ), n • -a = -n • a
This theorem, `zsmul_neg'`, states that for any type `α` that is a subtraction monoid, for any element `a` of type `α` and for any integer `n`, the product of `n` and the negation of `a` is equal to the negation of the product of `n` and `a`. In mathematical terms, it states that `n` times `-a` is equal to `-n` times `a`. This theorem can be seen as a property of distribution over negation in the context of multiplication with integers in any subtraction monoid.
More concisely: For any subtraction monoid type `α` and any integer `n`, `n` times the negation of an element `a` equals the negation of `n` times `a`.
|
two_nsmul
theorem two_nsmul : ∀ {M : Type u} [inst : AddMonoid M] (a : M), 2 • a = a + a
This theorem states that for any given type `M`, which has an additive monoid structure, the double scalar multiplication of any element `a` of type `M` is equal to the element `a` added to itself. This is more simply expressed as `2 * a = a + a`.
More concisely: For any additive monoid type `M`, the operation of multiplication by 2 is equivalent to the addition of an element with itself, i.e., `2 * a = a + a` for all `a` in `M`.
|
one_pow
theorem one_pow : ∀ {M : Type u} [inst : Monoid M] (n : ℕ), 1 ^ n = 1
This theorem states that for any natural number `n`, the nth power of `1` in any Monoid `M` is `1`. In other words, for any monoidal structure (which is a type `M` endowed with an associative binary operation and an identity element), raising the identity element (`1` in this context) to any natural number power results in the identity element. This is a generalization of the familiar rule from elementary arithmetic that any power of 1 is 1.
More concisely: For any monoid, raising its identity element to any natural number power yields the identity element.
|
zpow_bit0
theorem zpow_bit0 : ∀ {α : Type u_1} [inst : DivisionMonoid α] (a : α) (n : ℤ), a ^ bit0 n = a ^ n * a ^ n
The theorem `zpow_bit0` states that for any type `α` that has a division monoid structure (meaning multiplication and division operations are defined), and for any element `a` of type `α` and any integer `n`, the expression `a` raised to the power of `bit0 n` (which is defined as `n + n`) equals the product of `a` raised to the power of `n` and `a` raised to the power of `n`. In mathematical terms, this can be written as: for every element `a` in a division monoid and every integer `n`, we have \(a^{2n} = a^n \cdot a^n\).
More concisely: For any division monoid element `a` and integer `n`, the power `a^(2n)` equals the product of powers `a^(n) * a^(n)`.
|
two_zsmul
theorem two_zsmul : ∀ {G : Type w} [inst : SubNegMonoid G] (a : G), 2 • a = a + a
This theorem states that for all types `G` which are a subtype of `SubNegMonoid`, the double scalar multiplication of any element `a` of type `G` is equal to the sum of `a` with itself. In other words, in any subtractive negation monoid, multiplying any element by 2 is the same as adding that element to itself. This is an abstract algebraic property that is familiar from ordinary arithmetic, where multiplying a number by 2 gives the same result as adding the number to itself.
More concisely: For any subtractive negation monoid type `G`, the operation of multiplying an element `a` in `G` by 2 equals the operation of adding `a` to itself.
|
AddCommute.zsmul_right
theorem AddCommute.zsmul_right :
∀ {G : Type w} [inst : AddGroup G] {a b : G}, AddCommute a b → ∀ (m : ℤ), AddCommute a (m • b)
The theorem `AddCommute.zsmul_right` states that for any type `G` that is an additive group, given two elements `a` and `b` of `G` that commute additively (i.e., `a + b = b + a`), and any integer `m`, the operation `a` and `m • b` (where `m • b` signifies the operation of scalar multiplication of `b` by `m`) also commute additively. This means that if `a` and `b` commute in the group `G`, then `a` also commutes with any integer multiple of `b`.
More concisely: If `a` and `b` are elements of an additive group `G` that commute (i.e., `a + b = b + a`), then for any integer `m`, `a` commutes with `m • b` (`a + (m • b) = (m • b) + a`).
|
pow_one
theorem pow_one : ∀ {M : Type u} [inst : Monoid M] (a : M), a ^ 1 = a
This theorem, named `pow_one`, states that for any type M that has a monoid structure, the monoid operation applied to any element "a" of that type and the number 1 is equal to the element "a" itself.
In other words, for any monoid (a mathematical structure with an associative binary operation and an identity element), raising any element to the power of 1 keeps the element unchanged. This is a basic property of powers in mathematics, and here it's confirmed to hold in the context of abstract algebraic structures called monoids.
More concisely: For any monoid M and its identity element 1, for all a in M, a ^ 1 = a holds. (Here, ^ represents the monoid operation.)
|
pow_bit0'
theorem pow_bit0' : ∀ {M : Type u} [inst : Monoid M] (a : M) (n : ℕ), a ^ bit0 n = (a * a) ^ n
The theorem `pow_bit0'` states that for any type `M` which is equipped with a monoid structure, and for any element `a` of this monoid and natural number `n`, raising `a` to the power of `bit0 n` (where `bit0` is a function that doubles a number) is equal to raising `a * a` to the power of `n`. In mathematical notation, this is saying that $a^{2n} = (a * a)^n$ for `a` in a monoid `M` and `n` a natural number.
More concisely: For any monoid element `a` and natural number `n`, $(a \cdot a)^n = a^{2n}$.
|
pow_bit0
theorem pow_bit0 : ∀ {M : Type u} [inst : Monoid M] (a : M) (n : ℕ), a ^ bit0 n = a ^ n * a ^ n
The theorem `pow_bit0` states that for any type `M` that is a monoid, for any element `a` of `M` and any natural number `n`, the power of `a` raised to `bit0 n` equals the product of `a` raised to `n` and `a` raised to `n`. In mathematical terms, it means that a^(2n) = a^n * a^n for any monoid element `a` and any natural number `n`. Here, `bit0 n` represents the operation of doubling `n` in Lean.
More concisely: For any monoid `M` and element `a` in `M`, the power `a^(2n)` equals the product `a^n * a^n` for any natural number `n`.
|
pow_add
theorem pow_add : ∀ {M : Type u} [inst : Monoid M] (a : M) (m n : ℕ), a ^ (m + n) = a ^ m * a ^ n
This theorem, named `pow_add`, states that for any type `M` that forms a monoid and any element `a` of type `M`, the power of `a` raised to the sum of two natural numbers `m` and `n` is equal to the product of `a` raised to the power `m` and `a` raised to the power `n`. In mathematical notation, this would be expressed as \(a^{m+n} = a^m \times a^n\). This theorem essentially mirrors the exponential law from elementary algebra.
More concisely: For any monoid `M` and element `a` in `M`, `a^(m + n) = a^m * a^n`.
|
mul_nsmul'
theorem mul_nsmul' : ∀ {M : Type u} [inst : AddMonoid M] (a : M) (m n : ℕ), (m * n) • a = m • n • a
This theorem states that for any type `M` that forms an additive monoid, and for any element `a` of type `M` and any natural numbers `m` and `n`, the operation of scalar multiplication (denoted by `•`) satisfies the property that multiplying `m` and `n` and then scalar multiplying `a` is equivalent to first scalar multiplying `a` by `n` and then scalar multiplying the result by `m`. This can be viewed as a kind of associative law for scalar multiplication by natural numbers in an additive monoid.
More concisely: For any additive monoid type `M` and its element `a`, and natural numbers `m` and `n`, the scalar multiplication operation `•` satisfies the property that `(m * n) • a = m • (n • a)`.
|
Commute.mul_zpow
theorem Commute.mul_zpow :
∀ {α : Type u_1} [inst : DivisionMonoid α] {a b : α}, Commute a b → ∀ (i : ℤ), (a * b) ^ i = a ^ i * b ^ i := by
sorry
This theorem states that for any type `α` that is a division monoid, given any two elements `a` and `b` of type `α` that commute (meaning `a * b = b * a`), and an integer `i`, the `i`th integer power of the product `a * b` is equal to the product of the `i`th integer powers of `a` and `b`. In other words, `(a * b) ^ i = a ^ i * b ^ i` for all `a`, `b` that commute and all integers `i`. This shows the distribution of exponentiation over multiplication for commuting elements in a division monoid.
More concisely: For any commuting elements `a` and `b` in a division monoid `α`, and any integer `i`, the `i`th power of their product equals the product of their `i`th powers: `(a * b) ^ i = a ^ i * b ^ i`.
|
mul_pow
theorem mul_pow : ∀ {M : Type u} [inst : CommMonoid M] (a b : M) (n : ℕ), (a * b) ^ n = a ^ n * b ^ n
This theorem, `mul_pow`, states that for any type `M` that forms a commutative monoid (denoted by `CommMonoid M`), for any elements `a` and `b` of that type `M`, and for any natural number `n`, the nth power of the product of `a` and `b` is equal to the product of the nth power of `a` and the nth power of `b`. In mathematical terms, it could be represented as $(a * b)^n = a^n * b^n$ for all `a`, `b` in `M` and `n` in ℕ.
More concisely: For any commutative monoid `M`, and elements `a` and `b` in `M`, the nth powers of their product equal the product of their nth powers, i.e., $(a * b)^n = a^n * b^n$ for all `n` in ℕ.
|
pow_mul
theorem pow_mul : ∀ {M : Type u} [inst : Monoid M] (a : M) (m n : ℕ), a ^ (m * n) = (a ^ m) ^ n
This theorem states that for any type `M` that forms a monoid, and any element `a` of type `M`, the exponentiation of `a` by the product of two natural numbers `m` and `n` is equal to the result of raising `a` to the power of `m` and then raising that result to the power of `n`. In simpler terms, it asserts the identity `a^(m*n) = (a^m)^n` for any monoid element `a` and natural numbers `m` and `n`.
More concisely: For any monoid `M` and element `a` in `M`, and natural numbers `m` and `n`, `a^(m * n) = (a^m)^n`.
|
inv_zpow'
theorem inv_zpow' : ∀ {α : Type u_1} [inst : DivisionMonoid α] (a : α) (n : ℤ), a⁻¹ ^ n = a ^ (-n)
This theorem states that for any type `α` that forms a division monoid, and any element `a` of type `α` and an integer `n`, the inverse of `a` raised to the power of `n` equals `a` raised to the power of `-n`. In mathematical terms, if `a` is an element of a division monoid and `n` is an integer, then `(1/a)^n = a^(-n)`.
More concisely: For any division monoid element `a` and integer `n`, `(1/a)^n = a^(-n)`.
|
mul_nsmul
theorem mul_nsmul : ∀ {M : Type u} [inst : AddMonoid M] (a : M) (m n : ℕ), (m * n) • a = n • m • a
This theorem states that for any type `M` which is an Additive Monoid and any element `a` of `M`, the operation of scaling `a` by the product of two natural numbers `m` and `n` is equivalent to scaling `a` by `m` first and then scaling the result by `n`. Here, the notation `n • a` signifies the operation of adding `a` to itself `n` times, which is a generalization of multiplication for elements of an Additive Monoid.
More concisely: For any additive monoid type M and elements a, m, n, the operation m * n * a equals (m * a) * n. (Scaling an additive monoid element by the product of two natural numbers is equivalent to scaling it by each factor separately.)
|
zsmul_zero
theorem zsmul_zero : ∀ {α : Type u_1} [inst : SubtractionMonoid α] (n : ℤ), n • 0 = 0
This theorem states that for any integer `n` and any type `α` that is a subtraction monoid, the `n`-fold scalar multiplication (denoted `n • 0`) of the zero element of `α` is also the zero element of `α`. In other words, repeating the zero element of `α` `n` times results in the zero element, in any subtraction monoid `α`. This is a basic property in abstract algebra that expresses how scalar multiplication interacts with the zero element.
More concisely: For any integer `n` and subtraction monoid `α`, the `n`-fold scalar multiplication of its zero element is the zero element.
|
zpow_induction_right
theorem zpow_induction_right :
∀ {G : Type w} [inst : Group G] {g : G} {P : G → Prop},
P 1 → (∀ (a : G), P a → P (a * g)) → (∀ (a : G), P a → P (a * g⁻¹)) → ∀ (n : ℤ), P (g ^ n)
This theorem, `zpow_induction_right`, states that to prove a property (denoted by `P`) for all integral powers of an element `g` in a group `G`, it is sufficient to show that the property is preserved when an element satisfying the property is multiplied by `g` or the inverse of `g` (`g⁻¹`) from the right. Specifically, the property should hold for the identity element (1), and if it holds for any element `a` in the group, then it should also hold for `a * g` and `a * g⁻¹`. If these conditions are met, then the property holds for `g` raised to any integer power `n`. For the case of subgroups generated by more than one element, refer to `Subgroup.closure_induction_right`.
More concisely: If a property holds for the identity element and is closed under right multiplication and right multiplication by the inverse in a group, then it holds for all integral powers of any element in the group.
|
zpow_mul
theorem zpow_mul : ∀ {α : Type u_1} [inst : DivisionMonoid α] (a : α) (m n : ℤ), a ^ (m * n) = (a ^ m) ^ n
This theorem, `zpow_mul`, states that for any type `α` that has a DivisionMonoid structure, and for any object `a` of type `α` and any integers `m` and `n`, the power of `a` to the product of `m` and `n` is the same as the power of `a` to the `m` raised to the `n`. In mathematical terms, it essentially states that `a^(m*n) = (a^m)^n`. This is a standard property of exponentiation in the context of division monoids.
More concisely: For any object `a` in a type `α` with DivisionMonoid structure, `a^(m*n) = (a^m)^n`.
|
zsmul_neg
theorem zsmul_neg : ∀ {α : Type u_1} [inst : SubtractionMonoid α] (a : α) (n : ℤ), n • -a = -(n • a)
This theorem, `zsmul_neg`, states that for any given type `α` that is a subtraction monoid and any integer `n`, the scaled multiplication of `n` and the negation of `a` (`n • -a`) is equal to the negation of the scaled multiplication of `n` and `a` (`-(n • a)`). In other words, it expresses that the property of distributivity over multiplication and negation holds in the context of scaled multiplication and integers.
More concisely: For any subtraction monoid type `α` and integer `n`, `n * (-a) = -(n * a)`.
|
div_pow
theorem div_pow : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b : α) (n : ℕ), (a / b) ^ n = a ^ n / b ^ n := by
sorry
This theorem, `div_pow`, states that for any type `α` that forms a division commutative monoid, for any elements `a` and `b` of type `α` and any natural number `n`, the nth power of the division of `a` by `b` is equal to the division of the nth power of `a` by the nth power of `b`. In mathematical notation, this would be expressed as $(a / b)^n = a^n / b^n$.
More concisely: For any divisive commutative monoid type `α` and elements `a` and `b` of type `α`, the division of `a` by `b` raised to the power of a natural number `n` equals the power of `a` raised to `n` divided by the power of `b` raised to `n`.
|
sq
theorem sq : ∀ {M : Type u} [inst : Monoid M] (a : M), a ^ 2 = a * a
This theorem, known as an alias of `pow_two`, states that for any given type `M` that is a monoid, the square (`^ 2`) of any element (`a`) of `M` is equal to the element multiplied by itself (`a * a`). Most of the lemmas about powers of two refer to this as `sq`.
More concisely: For any monoid M and its element a, the square of a (a ^ 2) equals the product of a with itself (a * a).
|
pow_eq_pow_mod
theorem pow_eq_pow_mod : ∀ {M : Type u_2} [inst : Monoid M] {x : M} (m : ℕ) {n : ℕ}, x ^ n = 1 → x ^ m = x ^ (m % n)
This theorem states that in any monoid `M`, if a certain element `x` raised to the power of `n` equals `1`, then raising `x` to any power `m` is equivalent to raising `x` to the power of `m` modulo `n`. Essentially, it's expressing a property of powers in monoid structures that mirrors a similar property of integers: if an integer `x` to the power of `n` is `1`, then `x` to the power of `m` is the same as `x` to the power of `m` modulo `n`.
More concisely: In any monoid `M` and for all natural numbers `n` and `m`, if `x^n = 1` then `x^m = x^m % n`.
|
mul_zsmul'
theorem mul_zsmul' : ∀ {α : Type u_1} [inst : SubtractionMonoid α] (a : α) (m n : ℤ), (m * n) • a = n • m • a := by
sorry
This theorem, named `mul_zsmul'`, states that for any type `α` that forms a subtraction monoid, and any element `a` of this type `α` and any two integers `m` and `n`, the operation of "scalar multiplication" by the product of `m` and `n` on `a` is the same as first scalar multiplying `a` by `m` and then by `n`. In other words, it says that scalar multiplication is associative with respect to integer multiplication.
More concisely: For any subtraction monoid type `α` and its elements `a`, and integers `m` and `n`, the operation of scalar multiplication by the product of `m` and `n` on `a` equals the scalar multiplication of `a` by `m` followed by scalar multiplication by `n`.
|
one_zsmul
theorem one_zsmul : ∀ {G : Type w} [inst : SubNegMonoid G] (a : G), 1 • a = a
This theorem states that for any type `G` which is a subnegmonoid (i.e., a structure with subtraction and a unary negation operation), the scalar multiplication of any element `a` of type `G` by 1 results in the element `a` itself. In other words, 1 is the multiplicative identity in the scalar multiplication operation for any element of a subnegmonoid.
More concisely: For any subnegmonoid type `G` and element `a` in `G`, 1 * a = a.
|
add_one_zsmul
theorem add_one_zsmul : ∀ {G : Type w} [inst : AddGroup G] (a : G) (n : ℤ), (n + 1) • a = n • a + a
This theorem states that for any type `G` that has an addition group structure, and for any element `a` of type `G` and any integer `n`, the statement `(n + 1) • a = n • a + a` holds. In simpler terms, it means that adding 1 to `n` and then performing the scalar multiplication operation on `a` is equal to performing the scalar multiplication operation on `n` and `a`, and then adding `a`.
More concisely: For any additive group `G` and element `a` in `G`, and any integer `n`, the equation `(n + 1) * a = n * a + a` holds.
|
one_zpow
theorem one_zpow : ∀ {α : Type u_1} [inst : DivisionMonoid α] (n : ℤ), 1 ^ n = 1
This theorem states that for any type `α` that is a `DivisionMonoid` and for any integer `n`, raising 1 to the power `n` will always yield 1. In mathematical terms, this is the principle that any power of 1 is still 1, which holds true for all division monoids and integers.
More concisely: For any division monoid `α` and integer `n`, 1 raised to the power of `n` equals 1.
|
zpow_mul_comm
theorem zpow_mul_comm : ∀ {G : Type w} [inst : Group G] (a : G) (m n : ℤ), a ^ m * a ^ n = a ^ n * a ^ m
This theorem states that in any group `G`, for any element `a` in `G` and any two integers `m` and `n`, the multiplication of `a` raised to the power `m` and `a` raised to the power `n` is commutative. In other words, `a` to the power of `m` times `a` to the power of `n` is equal to `a` to the power of `n` times `a` to the power of `m`. This property is known as the commutativity of multiplication of powers in a group.
More concisely: In any group, for all elements a, integers m and n, the powers a^m and a^n commute, that is, a^m * a^n = a^n * a^m.
|
add_nsmul
theorem add_nsmul : ∀ {A : Type y} [inst : AddMonoid A] (a : A) (m n : ℕ), (m + n) • a = m • a + n • a
This theorem states that for any type `A` that is an additive monoid, and for any element `a` of `A` and natural numbers `m` and `n`, the scalars `m` and `n` can distribute over the addition operation in `A`. More formally, if we perform an `n`-times scalar multiplication operation on `a` and add that to the result of an `m`-times scalar multiplication operation on `a`, the result is the same as performing an `(m + n)`-times scalar multiplication operation on `a`. In mathematical notation, this can be written as `(m + n) * a = m * a + n * a`, where `*` is the scalar multiplication operation.
More concisely: For any additive monoid type `A` and elements `a` in `A` and natural numbers `m` and `n`, the distributive property holds: `(m + n) * a = m * a + n * a`.
|
zsmul_add
theorem zsmul_add : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b : α) (n : ℤ), n • (a + b) = n • a + n • b
This theorem, `zsmul_add`, states that for any type `α` which is a commutative monoid under subtraction (denoted `SubtractionCommMonoid α`), for any elements `a` and `b` of this type and any integer `n`, the operation of scalar multiplication distributes over addition. In mathematical terms, it says that `n` times the sum of `a` and `b` equals `n` times `a` plus `n` times `b`. This is a generalization of the distributive law in algebra.
More concisely: For any commutative monoid under subtraction `α` and integers `n`, `a`, `b` in `α`, we have `n * (a + b) = n * a + n * b`.
|
inv_zpow
theorem inv_zpow : ∀ {α : Type u_1} [inst : DivisionMonoid α] (a : α) (n : ℤ), a⁻¹ ^ n = (a ^ n)⁻¹
This theorem states that for any type `α` that forms a division monoid, and for any element `a` of type `α` and any integer `n`, the inverse of `a` raised to the power of `n` is equal to the inverse of `a` raised to the power of `n`. In mathematical terms, this can be written as $(a^{-1})^n = (a^n)^{-1}$ for all `a` in the division monoid and all integers `n`.
More concisely: For all division monoids `α`, and for all `a` in `α` and integer `n`, $(a^{-1})^n = (a^n)^{-1}$.
|
mul_zpow
theorem mul_zpow : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b : α) (n : ℤ), (a * b) ^ n = a ^ n * b ^ n := by
sorry
This theorem states that for any type `α` that forms a commutative division monoid, for any elements `a` and `b` of this type `α`, and for any integer `n`, the `n`th power of the product of `a` and `b` is equal to the product of the `n`th power of `a` and the `n`th power of `b`. In mathematical notation, this is saying that for all `a`, `b` in `α` and all integers `n`, `(a * b) ^ n = a ^ n * b ^ n`.
More concisely: For any commutative division monoid type `α` and elements `a, b` in `α`, and for any integer `n`, their `n`th powers satisfy the commutative property: `(a * b) ^ n = a ^ n * b ^ n`.
|
Commute.mul_pow
theorem Commute.mul_pow :
∀ {M : Type u} [inst : Monoid M] {a b : M}, Commute a b → ∀ (n : ℕ), (a * b) ^ n = a ^ n * b ^ n
This theorem states that for any monoid `M`, given two elements `a` and `b` from `M` that commute (i.e., `a * b = b * a`), for any natural number `n`, the `n`th power of the product `a * b` is equal to the product of `a` to the power of `n` and `b` to the power of `n`. In mathematical notation, if `a` and `b` commute, then $(a * b) ^ n = a^n * b^n$ for all natural numbers `n`.
More concisely: For any commuting elements `a` and `b` in a monoid and any natural number `n`, their `n`th powers satisfy the identity `(a * b)^n = a^n * b^n`.
|
pow_right_comm
theorem pow_right_comm : ∀ {M : Type u} [inst : Monoid M] (a : M) (m n : ℕ), (a ^ m) ^ n = (a ^ n) ^ m
This theorem, `pow_right_comm`, states that for any type `M` equipped with a monoid structure, the power operation is right-commutative. That is, for any element `a` of `M` and natural numbers `m` and `n`, raising `a` to the power of `m` and then to the power of `n` is the same as raising `a` to the power of `n` and then to the power of `m`. In other words, `(a ^ m) ^ n = (a ^ n) ^ m` holds for all `a` in `M` and `m, n` in `ℕ`.
More concisely: For all types `M` with a monoid structure and all elements `a` in `M` and natural numbers `m` and `n`, `(a ^ m) ^ n = (a ^ n) ^ m`.
|
zpow_neg
theorem zpow_neg : ∀ {α : Type u_1} [inst : DivisionMonoid α] (a : α) (n : ℤ), a ^ (-n) = (a ^ n)⁻¹
This theorem, `zpow_neg`, states that for any type `α` that forms a division monoid (i.e., a set equipped with an associative binary operation that has an identity element and each element has a unique inverse), and for any element `a` of `α` and an integer `n`, the negative power of `a` to `n` (i.e., `a` raised to the power `-n`) is equal to the inverse of `a` raised to the power `n` (i.e., `(a ^ n)⁻¹`). In mathematical notation, this would be expressed as $a^{-n} = (a^n)^{-1}$.
More concisely: For any element `a` in a division monoid `α` and integer `n`, `a^(-n) = (a^n)⁻¹`.
|
nsmul_zero
theorem nsmul_zero : ∀ {A : Type y} [inst : AddMonoid A] (n : ℕ), n • 0 = 0
This theorem states that for any natural number `n` and any type `A` that is an additive monoid, the scalar multiplication of `n` with the zero element of `A` is also the zero element of `A`. In more mathematical terms, this theorem says that for any `n` in ℕ and any additive monoid `A`, `n` times `0` equals `0`.
More concisely: For any natural number `n` and additive monoid `A`, the product of `n` and the zero element of `A` is equal to the zero element of `A`.
|
zpow_sub
theorem zpow_sub : ∀ {G : Type w} [inst : Group G] (a : G) (m n : ℤ), a ^ (m - n) = a ^ m * (a ^ n)⁻¹
This theorem states that for any group `G` and an element `a` of `G`, the power of `a` raised to the difference of two integers `m` and `n` is equal to the product of `a` raised to the `m` and the inverse of `a` raised to the `n`. In mathematical notation, this would be written as \(a^{(m - n)} = a^m * (a^n)^{-1}\).
More concisely: For any group `G` and its element `a`, the power of `a` raised to the difference of two integers `m` and `n` equals the product of `a` raised to the power of `m` and the inverse of `a` raised to the power of `n`: `(a^m)*(a^n)^-1 = a^(m-n)`.
|
nsmul_add
theorem nsmul_add : ∀ {M : Type u} [inst : AddCommMonoid M] (a b : M) (n : ℕ), n • (a + b) = n • a + n • b
This theorem, `nsmul_add`, is about the operations in an additive commutative monoid, represented by the type variable `M`. It states that for any elements `a` and `b` from the monoid, and any natural number `n`, the operation of n-fold addition (denoted by `n •`) distributes over the monoid addition operation. In mathematical terms, for any `a`, `b` in `M` and natural number `n`, `n` times the sum of `a` and `b` (`n • (a + b)`) is equal to the sum of `n` times `a` and `n` times `b` (`n • a + n • b`).
More concisely: For any additive commutative monoid `M`, and natural number `n`, the operation of `n-fold addition` distributes over the monoid addition operation, i.e., `n • (a + b) = n • a + n • b` for all `a, b` in `M`.
|