Powers in monoids and groups

Main results

• TauCeti.pow_eq_pow_of_pow_succ_eq_pow: if a ^ (n + 1) = a ^ n then a ^ k = a ^ n for all k ≥ n.
• TauCeti.pow_pow_eq_self_of_pow_sq_eq_self: if a ^ (q ^ 2) = a then (a ^ q) ^ q = a.
• TauCeti.mul_zpow_mul_mul_zpow: in a commutative group, integer powers of monomials a ^ i * b ^ j multiply by adding their exponent vectors.
• TauCeti.eq_mul_zpow_sub_iff_mul_zpow_eq: in a group, a = b * h ^ (n - m) if and only if a * h ^ m = b * h ^ n.

theorem TauCeti.pow_eq_pow_of_pow_succ_eq_pow {M : Type u_1} [Monoid M] {a : M} {n : ℕ} (h : a ^ (n + 1) = a ^ n) {k : ℕ} (hk : n ≤ k) : a ^ k = a ^ n

Once the powers of a repeat once, they are constant from that point on.

theorem TauCeti.pow_pow_eq_self_of_pow_sq_eq_self {M : Type u_1} [Monoid M] {a : M} {q : ℕ} (ha : a ^ q ^ 2 = a) : (a ^ q) ^ q = a

If a ^ (q ^ 2) = a then (a ^ q) ^ q = a. For example, an element of a field with q ^ 2 elements is fixed by applying the q-power map twice.

theorem TauCeti.mul_zpow_mul_mul_zpow {G : Type u_2} [CommGroup G] (a b : G) (i j k i' j' k' : ℤ) : (a ^ i * b ^ j) ^ k * (a ^ i' * b ^ j') ^ k' = a ^ (i * k + i' * k') * b ^ (j * k + j' * k')

In a commutative group, (a ^ i * b ^ j) ^ k * (a ^ i' * b ^ j') ^ k' is the monomial with exponents (i * k + i' * k', j * k + j' * k'): the integer matrix with columns (i, j) and (i', j') acts on the exponent vector (k, k').

theorem TauCeti.eq_mul_zpow_sub_iff_mul_zpow_eq {G : Type u_2} [Group G] {a b h : G} {m n : ℤ} : a = b * h ^ (n - m) ↔ a * h ^ m = b * h ^ n

Moving a power of h across an equation: a = b * h ^ (n - m) if and only if a * h ^ m = b * h ^ n.