ppow_add
theorem ppow_add :
∀ {M : Type u_1} [inst : Mul M] [inst_1 : Pow M ℕ+] [inst_2 : PNatPowAssoc M] (k n : ℕ+) (x : M),
x ^ (k + n) = x ^ k * x ^ n
This theorem, `ppow_add`, states that for any type `M` that supports multiplication and exponentiation by positive natural numbers, and for which this exponentiation operation is associative, raising a value `x` of this type to the power of the sum of two positive natural numbers `k` and `n` is the same as raising `x` to the power `k`, multiplying the result by `x` raised to the power `n`. This is analogous to the exponent addition rule in basic algebra, where `x^(a+b) = x^a * x^b`.
More concisely: For any type `M` with associative exponentiation by natural numbers, `x^(k + n) = x^k * x^n`.
|
PNatPowAssoc.ppow_one
theorem PNatPowAssoc.ppow_one :
∀ {M : Type u_2} [inst : Mul M] [inst_1 : Pow M ℕ+] [self : PNatPowAssoc M] (x : M), x ^ 1 = x
This theorem is stating that raising any element `x` of a type `M`, which has defined multiplication operation and a power operation to a positive natural number, to the power of 1 is an identity operation. In other words, for any such `x`, `x ^ 1` will be equal to `x` itself. This holds true for all `x` in `M`, making it a universal property. This is an instance of the mathematical principle that any number raised to the power of 1 is itself.
More concisely: For all types `M` with defined multiplication and power operations, and for all elements `x` in `M`, `x ^ 1` equals `x`.
|
ppow_one
theorem ppow_one : ∀ {M : Type u_1} [inst : Mul M] [inst_1 : Pow M ℕ+] [inst : PNatPowAssoc M] (x : M), x ^ 1 = x := by
sorry
This theorem states that for any type `M` that has a multiplication operation and a power operation that takes a positive natural number, and assuming that the power operation is associative with the multiplication, raising any element `x` of `M` to the power of `1` will result in `x` itself. In mathematical notation, this can be expressed as \(x^1 = x\) for any `x` in `M`.
More concisely: For any type `M` with multiplication and power operations, if the power operation is associative with multiplication, then for all `x` in `M`, `x^1 = x`.
|
PNatPowAssoc.ppow_add
theorem PNatPowAssoc.ppow_add :
∀ {M : Type u_2} [inst : Mul M] [inst_1 : Pow M ℕ+] [self : PNatPowAssoc M] (k n : ℕ+) (x : M),
x ^ (k + n) = x ^ k * x ^ n
This theorem states that multiplication is power-associative in the context of positive natural numbers. Specifically, for any type `M` that supports multiplication and exponentiation operations, and for any positive natural numbers `k` and `n`, and any element `x` of `M`, the power of `x` by the sum of `k` and `n` (`x ^ (k + n)`) is equal to the product of `x` to the power `k` and `x` to the power `n` (`x ^ k * x ^ n`). This is analogous to the property of exponents in arithmetic where `(x^(a+b)) = x^a * x^b`.
More concisely: For any type `M` with multiplication and exponentiation, and for all positive natural numbers `k` and `n` and element `x` in `M`, `x ^ (k + n)` equals `x ^ k * x ^ n`.
|