Positive Natural Number Exponentiation for Semigroups

This file defines and instantiates an exponentiation operation on semigroups. Exponentiation is typically defined for natural number exponents, but here we require non-zero natural numbers (ℕ+) because x^0 is not well-defined in a semigroup context.

This file also contains lemmas about the properties of this exponentiation operation and of the ℕ+ type.

Main definitions

• Semigroup.pNatPow - Definition of exponentiation in semigroups using positive naturals.

Main theorems

In the following statements, x y : S and m n : ℕ+ where S is a semigroup:

• Semigroup.pow_add - x ^ m * x ^ n = x ^ (m + n).
• Semigroup.mul_pow_mul - (x * y) ^ n * x = x * (y * x) ^ n.
• Semigroup.pow_mul_comm - x ^ m * x ^ n = x ^ n * x ^ m.
• Semigroup.pow_mul_comm' - x ^ n * x = x * x ^ n.
• Semigroup.pow_mul - (x ^ n) ^ m = x ^ (m * n).
• Semigroup.pow_right_comm - (x ^ m) ^ n = (x ^ n) ^ m.
• Monoid.pow_pNat_to_nat - x ^ n = x ^ (n : ℕ).
• WithOne.pow_eq - (↑x : WithOne S) ^ n = ↑(x ^ n).

Implementation notes

The simp-tagged lemmas collectively normalize power expressions when calling simp. For example, (a * b) ^ n * (a * b) ^ m * a ^ 1 normalizes to a * (b * a) ^ (n + m).

References

Analogous definitions and lemmas for exponentiation in monoids can be found in Mathlib.Algebra.Group.Defs.

Blueprint

This file does not have any blueprint entries.

theorem PNat.exists_eq_add_of_lt {m n : ℕ+} (m_lt_n : m < n) : ∃ (k : ℕ+), n = k + m

If m < n for positive naturals, then there exists a positive k such that n = k + m.

@[simp]

theorem PNat.add_sub_cancel' {m n : ℕ+} (m_lt_n : m < n) : m + (n - m) = n

For positive naturals, if m < n then m + (n - m) = n.

theorem PNat.n_lt_2nm (n m : ℕ+) : n < 2 * n * m

For positive naturals, n < 2 * n * m.

def Semigroup.pNatPow {S : Type u_1} [Semigroup S] (x : S) (n : ℕ+) : S

Exponentiation for semigroups over positive naturals.

Equations

• Semigroup.pNatPow x n = n.recOn x fun (x_1 : ℕ+) (ih : S) => ih * x

instance Semigroup.hPow {S : Type u_1} [Semigroup S] : Pow S ℕ+

Provides the notation a ^ n for pNatPow a n.

Equations

• Semigroup.hPow = { pow := Semigroup.pNatPow }

@[simp]

theorem Semigroup.pow_one {S : Type u_1} [Semigroup S] (x : S) : x ^ 1 = x

For any element of a semigroup, raising it to the power 1 gives back the element itself.

@[simp]

theorem Semigroup.pow_succ {S : Type u_1} [Semigroup S] (x : S) (n : ℕ+) : x ^ n * x = x ^ (n + 1)

Exponentiation satisfies the successor property.

@[simp]

theorem Semigroup.pow_add {S : Type u_1} [Semigroup S] (x : S) (n m : ℕ+) : x ^ m * x ^ n = x ^ (m + n)

Multiplying powers with the same base is equivalent to exponentiating by the sum.

@[simp]

theorem Semigroup.mul_pow_mul {S : Type u_1} [Semigroup S] (x y : S) (n : ℕ+) : (x * y) ^ n * x = x * (y * x) ^ n

Multiplicative associativity for powers.

theorem Semigroup.pow_mul_comm {S : Type u_1} [Semigroup S] (x : S) (n m : ℕ+) : x ^ m * x ^ n = x ^ n * x ^ m

Powers of the same element commute with each other.

@[simp]

theorem Semigroup.pow_mul_comm' {S : Type u_1} [Semigroup S] (x : S) (n : ℕ+) : x ^ n * x = x * x ^ n

Every power of an element commutes with the element itself.

@[simp]

theorem Semigroup.pow_mul {S : Type u_1} [Semigroup S] (x : S) (n m : ℕ+) : (x ^ n) ^ m = x ^ (m * n)

Taking the power of a power is equivalent to exponentiating by the product.

theorem Semigroup.pow_right_comm {S : Type u_1} [Semigroup S] (x : S) (n m : ℕ+) : (x ^ m) ^ n = (x ^ n) ^ m

Right-associated powers can be rearranged due to commutativity of exponent multiplication.

theorem Monoid.pow_pNat_to_nat {M : Type u_1} [Monoid M] (x : M) (n : ℕ+) : x ^ n = x ^ ↑n

Bridge between positive natural powers and standard natural number powers in monoids.

theorem WithOne.pow_eq {S : Type u_1} [Semigroup S] (x : S) (n : ℕ+) : ↑x ^ n = ↑(x ^ n)

Taking powers in the adjunction S¹ corresponds to taking powers in the semigroup S and then embedding the result.