# Typeclasses for power-associative structures #

In this file we define power-associativity for algebraic structures with a multiplication operation. The class is a Prop-valued mixin named NatPowAssoc.

## Results #

• npow_add a defining property: x ^ (k + n) = x ^ k * x ^ n
• npow_one a defining property: x ^ 1 = x
• npow_assoc strictly positive powers of an element have associative multiplication.
• npow_comm x ^ m * x ^ n = x ^ n * x ^ m for strictly positive m and n.
• npow_mul x ^ (m * n) = (x ^ m) ^ n for strictly positive m and n.
• npow_eq_pow monoid exponentiation coincides with semigroup exponentiation.

## Instances #

We also produce the following instances:

• NatPowAssoc for Monoids, Pi types and products.

## TODO #

class NatPowAssoc (M : Type u_2) [] [Pow M ] :

A mixin for power-associative multiplication.

• npow_add : ∀ (k n : ) (x : M), x ^ (k + n) = x ^ k * x ^ n

Multiplication is power-associative.

• npow_zero : ∀ (x : M), x ^ 0 = 1

Exponent zero is one.

• npow_one : ∀ (x : M), x ^ 1 = x

Exponent one is identity.

Instances
theorem NatPowAssoc.npow_add {M : Type u_2} [] [Pow M ] [self : ] (k : ) (n : ) (x : M) :
x ^ (k + n) = x ^ k * x ^ n

Multiplication is power-associative.

theorem NatPowAssoc.npow_zero {M : Type u_2} [] [Pow M ] [self : ] (x : M) :
x ^ 0 = 1

Exponent zero is one.

theorem NatPowAssoc.npow_one {M : Type u_2} [] [Pow M ] [self : ] (x : M) :
x ^ 1 = x

Exponent one is identity.

theorem npow_add {M : Type u_1} [] [Pow M ] [] (k : ) (n : ) (x : M) :
x ^ (k + n) = x ^ k * x ^ n
@[simp]
theorem npow_zero {M : Type u_1} [] [Pow M ] [] (x : M) :
x ^ 0 = 1
@[simp]
theorem npow_one {M : Type u_1} [] [Pow M ] [] (x : M) :
x ^ 1 = x
theorem npow_mul_assoc {M : Type u_1} [] [Pow M ] [] (k : ) (m : ) (n : ) (x : M) :
x ^ k * x ^ m * x ^ n = x ^ k * (x ^ m * x ^ n)
theorem npow_mul_comm {M : Type u_1} [] [Pow M ] [] (m : ) (n : ) (x : M) :
x ^ m * x ^ n = x ^ n * x ^ m
theorem npow_mul {M : Type u_1} [] [Pow M ] [] (x : M) (m : ) (n : ) :
x ^ (m * n) = (x ^ m) ^ n
theorem npow_mul' {M : Type u_1} [] [Pow M ] [] (x : M) (m : ) (n : ) :
x ^ (m * n) = (x ^ n) ^ m
theorem neg_npow_assoc {R : Type u_2} [] [Pow R ] [] (a : R) (b : R) (k : ) :
(-1) ^ k * a * b = (-1) ^ k * (a * b)
instance Pi.instNatPowAssoc {ι : Type u_2} {α : ιType u_3} [(i : ι) → MulOneClass (α i)] [(i : ι) → Pow (α i) ] [∀ (i : ι), NatPowAssoc (α i)] :
NatPowAssoc ((i : ι) → α i)
Equations
• =
instance Prod.instNatPowAssoc {M : Type u_1} {N : Type u_2} [] [Pow M ] [] [] [Pow N ] [] :
Equations
• =
instance Monoid.PowAssoc {M : Type u_1} [] :
Equations
• =
@[simp]
theorem Nat.cast_npow (R : Type u_2) [] [Pow R ] [] (n : ) (m : ) :
(n ^ m) = n ^ m
@[simp]
theorem Int.cast_npow (R : Type u_2) [] [Pow R ] [] (n : ) (m : ) :
(n ^ m) = n ^ m