doc-next-gen

Mathlib.Algebra.Group.NatPowAssoc

Module docstring

{"# 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?

"}

NatPowAssoc structure
(M : Type*) [MulOneClass M] [Pow M ℕ]
Full source 
/-- A mixin for power-associative multiplication. -/
class NatPowAssoc (M : Type*) [MulOneClass M] [Pow M ℕ] : Prop where
  /-- Multiplication is power-associative. -/
  protected npow_add : ∀ (k n : ℕ) (x : M), x ^ (k + n) = x ^ k * x ^ n
  /-- Exponent zero is one. -/
  protected npow_zero : ∀ (x : M), x ^ 0 = 1
  /-- Exponent one is identity. -/
  protected npow_one : ∀ (x : M), x ^ 1 = x
Power-associative multiplication
Informal description
A structure that serves as a mixin for power-associative multiplication in algebraic structures. A type `M` with a multiplication operation and natural number exponentiation is power-associative if the operation satisfies the property that for any element `x` in `M` and natural numbers `k` and `n`, the exponentiation `x ^ (k + n)` equals `x ^ k * x ^ n`.
npow_add theorem
(k n : ℕ) (x : M) : x ^ (k + n) = x ^ k * x ^ n
Full source 
theorem npow_add (k n : ℕ) (x : M) : x ^ (k + n) = x ^ k * x ^ n  :=
  NatPowAssoc.npow_add k n x
Power-Associative Exponent Addition Rule: $x^{k + n} = x^k \cdot x^n$
Informal description
For any element $x$ in a power-associative multiplication structure $M$ and for any natural numbers $k$ and $n$, the exponentiation satisfies $x^{k + n} = x^k \cdot x^n$.
npow_zero theorem
(x : M) : x ^ 0 = 1
Full source 
@[simp]
theorem npow_zero (x : M) : x ^ 0 = 1 :=
  NatPowAssoc.npow_zero x
Zero Exponent Identity in Power-Associative Structures
Informal description
For any element $x$ in a power-associative multiplication structure $M$, raising $x$ to the power of $0$ yields the multiplicative identity $1$, i.e., $x^0 = 1$.
npow_one theorem
(x : M) : x ^ 1 = x
Full source 
@[simp]
theorem npow_one (x : M) : x ^ 1 = x :=
  NatPowAssoc.npow_one x
First Power Identity in Power-Associative Structures
Informal description
For any element $x$ in a power-associative multiplication structure $M$, raising $x$ to the power of $1$ yields $x$ itself, i.e., $x^1 = x$.
npow_mul_assoc theorem
(k m n : ℕ) (x : M) : (x ^ k * x ^ m) * x ^ n = x ^ k * (x ^ m * x ^ n)
Full source 
theorem npow_mul_assoc (k m n : ℕ) (x : M) :
    (x ^ k * x ^ m) * x ^ n = x ^ k * (x ^ m * x ^ n) := by
  simp only [← npow_add, add_assoc]
Associativity of Powers in Power-Associative Structures: $(x^k \cdot x^m) \cdot x^n = x^k \cdot (x^m \cdot x^n)$
Informal description
For any natural numbers $k$, $m$, $n$ and any element $x$ in a power-associative multiplication structure $M$, the following associativity property holds: $$(x^k \cdot x^m) \cdot x^n = x^k \cdot (x^m \cdot x^n).$$
npow_mul_comm theorem
(m n : ℕ) (x : M) : x ^ m * x ^ n = x ^ n * x ^ m
Full source 
theorem npow_mul_comm (m n : ℕ) (x : M) :
    x ^ m * x ^ n = x ^ n * x ^ m := by simp only [← npow_add, add_comm]
Commutativity of Powers in Power-Associative Structures: $x^m \cdot x^n = x^n \cdot x^m$
Informal description
For any natural numbers $m$ and $n$, and any element $x$ in a power-associative multiplication structure $M$, the product of $x^m$ and $x^n$ equals the product of $x^n$ and $x^m$, i.e., $x^m \cdot x^n = x^n \cdot x^m$.
npow_mul theorem
(x : M) (m n : ℕ) : x ^ (m * n) = (x ^ m) ^ n
Full source 
theorem npow_mul (x : M) (m n : ℕ) : x ^ (m * n) = (x ^ m) ^ n := by
  induction n with
  | zero => rw [npow_zero, Nat.mul_zero, npow_zero]
  | succ n ih => rw [mul_add, npow_add, ih, mul_one, npow_add, npow_one]
Power-Associative Exponent Multiplication Rule: $x^{m \cdot n} = (x^m)^n$
Informal description
For any element $x$ in a power-associative multiplication structure $M$ and for any natural numbers $m$ and $n$, the exponentiation satisfies $x^{m \cdot n} = (x^m)^n$.
npow_mul' theorem
(x : M) (m n : ℕ) : x ^ (m * n) = (x ^ n) ^ m
Full source 
theorem npow_mul' (x : M) (m n : ℕ) : x ^ (m * n) = (x ^ n) ^ m := by
  rw [mul_comm]
  exact npow_mul x n m
Power-Associative Exponent Multiplication Rule (Symmetric Form): $x^{m \cdot n} = (x^n)^m$
Informal description
For any element $x$ in a power-associative multiplication structure $M$ and for any natural numbers $m$ and $n$, the exponentiation satisfies $x^{m \cdot n} = (x^n)^m$.
neg_npow_assoc theorem
{R : Type*} [NonAssocRing R] [Pow R ℕ] [NatPowAssoc R] (a b : R) (k : ℕ) : (-1) ^ k * a * b = (-1) ^ k * (a * b)
Full source 
theorem neg_npow_assoc {R : Type*} [NonAssocRing R] [Pow R ℕ] [NatPowAssoc R] (a b : R) (k : ℕ) :
    (-1)^k * a * b = (-1)^k * (a * b) := by
  induction k with
  | zero => simp only [npow_zero, one_mul]
  | succ k ih =>
    rw [npow_add, npow_one, ← neg_mul_comm, mul_one]
    simp only [neg_mul, ih]
Power-Associative Scalar Multiplication with $(-1)^k$ in Non-Associative Rings
Informal description
Let $R$ be a non-associative ring with power-associative natural number exponentiation. For any elements $a, b \in R$ and any natural number $k$, we have $(-1)^k \cdot a \cdot b = (-1)^k \cdot (a \cdot b)$.
Pi.instNatPowAssoc instance
{ι : Type*} {α : ι → Type*} [∀ i, MulOneClass <| α i] [∀ i, Pow (α i) ℕ] [∀ i, NatPowAssoc <| α i] : NatPowAssoc (∀ i, α i)
Full source 
instance Pi.instNatPowAssoc {ι : Type*} {α : ι → Type*} [∀ i, MulOneClass <| α i] [∀ i, Pow (α i) ℕ]
    [∀ i, NatPowAssoc <| α i] : NatPowAssoc (∀ i, α i) where
    npow_add _ _ _ := by ext; simp [npow_add]
    npow_zero _ := by ext; simp
    npow_one _ := by ext; simp
Power-Associative Structure on Product Types
Informal description
For any family of types $(\alpha_i)_{i \in \iota}$ where each $\alpha_i$ is equipped with a multiplication operation, a multiplicative identity, and a power-associative natural number exponentiation, the product type $\prod_{i \in \iota} \alpha_i$ inherits a power-associative structure with pointwise operations.
Prod.instNatPowAssoc instance
{N : Type*} [MulOneClass M] [Pow M ℕ] [NatPowAssoc M] [MulOneClass N] [Pow N ℕ] [NatPowAssoc N] : NatPowAssoc (M × N)
Full source 
instance Prod.instNatPowAssoc {N : Type*} [MulOneClass M] [Pow M ℕ] [NatPowAssoc M] [MulOneClass N]
    [Pow N ℕ] [NatPowAssoc N] : NatPowAssoc (M × N) where
  npow_add _ _ _ := by ext <;> simp [npow_add]
  npow_zero _ := by ext <;> simp
  npow_one _ := by ext <;> simp
Power-Associative Structure on Product Types
Informal description
For any two types $M$ and $N$ each equipped with a multiplicative structure with a unit element and power-associative natural number exponentiation, the product type $M \times N$ inherits a power-associative structure where exponentiation is defined componentwise.
Monoid.PowAssoc instance
: NatPowAssoc M
Full source 
instance Monoid.PowAssoc : NatPowAssoc M where
  npow_add _ _ _ := pow_add _ _ _
  npow_zero _ := pow_zero _
  npow_one _ := pow_one _
Monoids are Power-Associative
Informal description
Every monoid is power-associative, meaning that for any element $x$ in the monoid and natural numbers $k$ and $n$, the exponentiation $x^{k+n}$ equals $x^k \cdot x^n$.
Nat.cast_npow theorem
(R : Type*) [NonAssocSemiring R] [Pow R ℕ] [NatPowAssoc R] (n m : ℕ) : (↑(n ^ m) : R) = (↑n : R) ^ m
Full source 
@[simp, norm_cast]
theorem Nat.cast_npow (R : Type*) [NonAssocSemiring R] [Pow R ℕ] [NatPowAssoc R] (n m : ℕ) :
    (↑(n ^ m) : R) = (↑n : R) ^ m := by
  induction m with
  | zero => simp only [pow_zero, Nat.cast_one, npow_zero]
  | succ m ih => rw [npow_add, npow_add, Nat.cast_mul, ih, npow_one, npow_one]
Natural Number Power Preservation Under Casting in Power-Associative Semirings
Informal description
Let $R$ be a non-associative semiring equipped with a power operation $R \times \mathbb{N} \to R$ that is power-associative. For any natural numbers $n$ and $m$, the canonical homomorphism from $\mathbb{N}$ to $R$ satisfies $(n^m)_R = (n_R)^m$, where $(\cdot)_R$ denotes the image under the canonical homomorphism.
Int.cast_npow theorem
(R : Type*) [NonAssocRing R] [Pow R ℕ] [NatPowAssoc R] (n : ℤ) : ∀ (m : ℕ), @Int.cast R NonAssocRing.toIntCast (n ^ m) = (n : R) ^ m
Full source 
@[simp, norm_cast]
theorem Int.cast_npow (R : Type*) [NonAssocRing R] [Pow R ℕ] [NatPowAssoc R]
    (n : ℤ) : ∀(m : ℕ), @Int.cast R NonAssocRing.toIntCast (n ^ m) = (n : R) ^ m
  | 0 => by
    rw [pow_zero, npow_zero, Int.cast_one]
  | m + 1 => by
    rw [npow_add, npow_one, Int.cast_mul, Int.cast_npow R n m, npow_add, npow_one]
Integer Power Preservation Under Casting in Power-Associative Rings
Informal description
Let $R$ be a non-associative ring equipped with a power operation $R \times \mathbb{N} \to R$ that is power-associative. For any integer $n \in \mathbb{Z}$ and natural number $m \in \mathbb{N}$, the canonical integer cast of $n^m$ in $R$ equals the $m$-th power of the integer cast of $n$ in $R$, i.e., $(n^m)_R = (n_R)^m$.