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 PNatPowAssoc, where PNat means only strictly positive powers are considered.

Results

• ppow_add a defining property: x ^ (k + n) = x ^ k * x ^ n
• ppow_one a defining property: x ^ 1 = x
• ppow_assoc strictly positive powers of an element have associative multiplication.
• ppow_comm x ^ m * x ^ n = x ^ n * x ^ m for strictly positive m and n.
• ppow_mul x ^ (m * n) = (x ^ m) ^ n for strictly positive m and n.
• ppow_eq_pow monoid exponentiation coincides with semigroup exponentiation.

Instances

• PNatPowAssoc for products and Pi types

TODO

• NatPowAssoc for MulOneClass - more or less the same flow
• It seems unlikely that anyone will want NatSMulAssoc and PNatSMulAssoc as additive versions of power-associativity, but we have found that it is not hard to write.

class PNatPowAssoc (M : Type u_2) [Mul M] [Pow M ℕ+] : Prop

A Prop-valued mixin for power-associative multiplication in the non-unital setting.

• ppow_add (k n : ℕ+) (x : M) : x ^ (k + n) = x ^ k * x ^ n

  Multiplication is power-associative.

• ppow_one (x : M) : x ^ 1 = x

  Exponent one is identity.

theorem ppow_add {M : Type u_1} [Mul M] [Pow M ℕ+] [PNatPowAssoc M] (k n : ℕ+) (x : M) : x ^ (k + n) = x ^ k * x ^ n

@[simp]

theorem ppow_one {M : Type u_1} [Mul M] [Pow M ℕ+] [PNatPowAssoc M] (x : M) : x ^ 1 = x

theorem ppow_mul_assoc {M : Type u_1} [Mul M] [Pow M ℕ+] [PNatPowAssoc M] (k m n : ℕ+) (x : M) : x ^ k * x ^ m * x ^ n = x ^ k * (x ^ m * x ^ n)

theorem ppow_mul_comm {M : Type u_1} [Mul M] [Pow M ℕ+] [PNatPowAssoc M] (m n : ℕ+) (x : M) : x ^ m * x ^ n = x ^ n * x ^ m

theorem ppow_mul {M : Type u_1} [Mul M] [Pow M ℕ+] [PNatPowAssoc M] (x : M) (m n : ℕ+) : x ^ (m * n) = (x ^ m) ^ n

theorem ppow_mul' {M : Type u_1} [Mul M] [Pow M ℕ+] [PNatPowAssoc M] (x : M) (m n : ℕ+) : x ^ (m * n) = (x ^ n) ^ m

instance Pi.instPNatPowAssoc {ι : Type u_2} {α : ι → Type u_3} [(i : ι) → Mul (α i)] [(i : ι) → Pow (α i) ℕ+] [∀ (i : ι), PNatPowAssoc (α i)] : PNatPowAssoc ((i : ι) → α i)

instance Prod.instPNatPowAssoc {M : Type u_1} {N : Type u_2} [Mul M] [Pow M ℕ+] [PNatPowAssoc M] [Mul N] [Pow N ℕ+] [PNatPowAssoc N] : PNatPowAssoc (M × N)

theorem ppow_eq_pow {M : Type u_1} [Monoid M] [Pow M ℕ+] [PNatPowAssoc M] (x : M) (n : ℕ+) : x ^ n = x ^ ↑n