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

• to_additive?

class NatPowAssoc (M : Type u_2) [MulOneClass M] [Pow M ℕ] : Prop

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.

theorem npow_add {M : Type u_1} [MulOneClass M] [Pow M ℕ] [NatPowAssoc M] (k n : ℕ) (x : M) : x ^ (k + n) = x ^ k * x ^ n

@[simp]

theorem npow_zero {M : Type u_1} [MulOneClass M] [Pow M ℕ] [NatPowAssoc M] (x : M) : x ^ 0 = 1

@[simp]

theorem npow_one {M : Type u_1} [MulOneClass M] [Pow M ℕ] [NatPowAssoc M] (x : M) : x ^ 1 = x

theorem npow_mul_assoc {M : Type u_1} [MulOneClass M] [Pow M ℕ] [NatPowAssoc 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} [MulOneClass M] [Pow M ℕ] [NatPowAssoc M] (m n : ℕ) (x : M) : x ^ m * x ^ n = x ^ n * x ^ m

theorem npow_mul {M : Type u_1} [MulOneClass M] [Pow M ℕ] [NatPowAssoc M] (x : M) (m n : ℕ) : x ^ (m * n) = (x ^ m) ^ n

theorem npow_mul' {M : Type u_1} [MulOneClass M] [Pow M ℕ] [NatPowAssoc M] (x : M) (m n : ℕ) : x ^ (m * n) = (x ^ n) ^ m

theorem neg_npow_assoc {R : Type u_2} [NonAssocRing R] [Pow R ℕ] [NatPowAssoc R] (a 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)

instance Prod.instNatPowAssoc {M : Type u_1} {N : Type u_2} [MulOneClass M] [Pow M ℕ] [NatPowAssoc M] [MulOneClass N] [Pow N ℕ] [NatPowAssoc N] : NatPowAssoc (M × N)

instance Monoid.PowAssoc {M : Type u_1} [Monoid M] : NatPowAssoc M

@[simp]

theorem Nat.cast_npow (R : Type u_2) [NonAssocSemiring R] [Pow R ℕ] [NatPowAssoc R] (n m : ℕ) : ↑(n ^ m) = ↑n ^ m

@[simp]

theorem Int.cast_npow (R : Type u_2) [NonAssocRing R] [Pow R ℕ] [NatPowAssoc R] (n : ℤ) (m : ℕ) : ↑(n ^ m) = ↑n ^ m