Documentation

Mathlib.Algebra.Group.PNatPowAssoc

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 #

Instances #

TODO #

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

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.

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

    Multiplication is power-associative.

    theorem PNatPowAssoc.ppow_one {M : Type u_2} [Mul M] [Pow M ℕ+] [self : PNatPowAssoc M] (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)
    Equations
    • =
    instance Prod.instPNatPowAssoc {M : Type u_1} {N : Type u_2} [Mul M] [Pow M ℕ+] [PNatPowAssoc M] [Mul N] [Pow N ℕ+] [PNatPowAssoc N] :
    Equations
    • =
    theorem ppow_eq_pow {M : Type u_1} [Monoid M] [Pow M ℕ+] [PNatPowAssoc M] (x : M) (n : ℕ+) :
    x ^ n = x ^ n