Documentation

Mathlib.Algebra.Group.NatPowAssoc

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 #

Instances #

We also produce the following instances:

TODO #

class NatPowAssoc (M : Type u_2) [MulOneClass M] [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} :
    ∀ {inst : MulOneClass M} {inst_1 : Pow M } [self : NatPowAssoc M] (k n : ) (x : M), x ^ (k + n) = x ^ k * x ^ n

    Multiplication is power-associative.

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

    Exponent zero is one.

    theorem NatPowAssoc.npow_one {M : Type u_2} :
    ∀ {inst : MulOneClass M} {inst_1 : Pow M } [self : NatPowAssoc M] (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 : 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} [MulOneClass M] [Pow M ] [NatPowAssoc M] [MulOneClass N] [Pow N ] [NatPowAssoc N] :
    Equations
    • =
    instance Monoid.PowAssoc {M : Type u_1} [Monoid M] :
    Equations
    • =
    @[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