NatPowAssoc.npow_add
theorem NatPowAssoc.npow_add :
∀ {M : Type u_2} [inst : MulOneClass M] [inst_1 : Pow M ℕ] [self : NatPowAssoc M] (k n : ℕ) (x : M),
x ^ (k + n) = x ^ k * x ^ n
This theorem states that in the context of any type `M` that has multiplication and power operations defined on it, and furthermore, respects the associativity of natural number powers (i.e., `NatPowAssoc`), the power of `x` raised to the sum of `k` and `n` is equal to the product of `x` raised to the power `k` and `x` raised to the power `n`. In mathematical notation, it asserts the identity $x^{k+n} = x^k x^n$ for any `x` in `M` and natural numbers `k` and `n`.
More concisely: For any type `M` with multiplication and power operations, and for natural numbers `k` and `n`, `x^(k + n) = x^k * x^n`.
|
npow_add
theorem npow_add :
∀ {M : Type u_1} [inst : MulOneClass M] [inst_1 : Pow M ℕ] [inst_2 : NatPowAssoc M] (k n : ℕ) (x : M),
x ^ (k + n) = x ^ k * x ^ n
This theorem states that for any type `M` that has a multiplication and identity operation (`MulOneClass`), a power operation (`Pow`), and satisfies associativity for the natural number power operation (`NatPowAssoc`), and for any natural numbers `k` and `n`, and any element `x` of type `M`, the power of `x` raised to the sum of `k` and `n` equals the product of `x` raised to `k` and `x` raised to `n`. In mathematical notation, this is equivalent to saying that $x^{k+n} = x^k \cdot x^n$. This is basically the power of a sum property in arithmetic.
More concisely: For any `M` with `MulOneClass`, `Pow`, and `NatPowAssoc`, and for all natural numbers `k` and `n` and `x` in `M`, `x^(k + n) = x^k * x^n`.
|
NatPowAssoc.npow_one
theorem NatPowAssoc.npow_one :
∀ {M : Type u_2} [inst : MulOneClass M] [inst_1 : Pow M ℕ] [self : NatPowAssoc M] (x : M), x ^ 1 = x
This theorem, titled "Exponent one is identity", establishes that for any type `M` that has a multiplication and a one (i.e., belongs to the `MulOneClass`), and a definition of exponentiation (`Pow M ℕ`), raising any instance `x` of `M` to the power of 1 is equal to `x` itself. This is essentially stating the fundamental mathematical property that anything raised to the power of 1 is itself.
More concisely: For any type `M` in the `MulOneClass` with multiplication and one, and defined exponentiation, raising any element `x` of `M` to the power of 1 equals `x` itself. (i.e., `∀ (x : M), x ^ 1 = x`).
|
npow_one
theorem npow_one :
∀ {M : Type u_1} [inst : MulOneClass M] [inst_1 : Pow M ℕ] [inst : NatPowAssoc M] (x : M), x ^ 1 = x
This theorem states that for any type `M` that forms a multiplication monoid with an associated natural number power operation, raising any element `x` of `M` to the power of 1 yields `x` itself. In mathematical terms, for any `x` in `M`, `x^1 = x`.
More concisely: For any multiplication monoid `M` with power operation, the power `x^1` of any `x` in `M` equals `x`.
|
NatPowAssoc.npow_zero
theorem NatPowAssoc.npow_zero :
∀ {M : Type u_2} [inst : MulOneClass M] [inst_1 : Pow M ℕ] [self : NatPowAssoc M] (x : M), x ^ 0 = 1
This theorem, named `NatPowAssoc.npow_zero`, states that for any type `M`, which is part of a `MulOneClass` (a structure with multiplication and a multiplicative identity element '1') and has a power operation defined with natural numbers (`ℕ`), raising any element `x` of `M` to the power of zero yields the multiplicative identity '1'. This theorem is a formalization of the mathematical principle that any number (excluding zero for non-multiplicative structures) to the power of zero equals one.
More concisely: For any type `M` in a `MulOneClass` with natural number powers, `x^0 = 1` for all `x` in `M`.
|
npow_zero
theorem npow_zero :
∀ {M : Type u_1} [inst : MulOneClass M] [inst_1 : Pow M ℕ] [inst_2 : NatPowAssoc M] (x : M), x ^ 0 = 1
This theorem states that for any type `M` that has a multiplication operation and a unity (i.e., there exists a `MulOneClass` instance), and has a power operation with natural numbers (i.e., there exists a `Pow M ℕ` instance), and multiplication and power are associative (i.e., there exists a `NatPowAssoc` instance), then any element `x` of type `M` raised to the power of zero is equal to the unity. In mathematical terms, for any `x` in `M`, `x ^ 0 = 1`.
More concisely: If `M` is a type with a multiplication, unity, and power operations, and multiplication and power are associative, then for all `x` in `M`, `x ^ 0 = 1`.
|