The prime p divides (x - 1) ^ p ^ k when x ^ p ^ k = 1

In any ring, an element x with x ^ p ^ k = 1 for a prime p satisfies (p : A) ∣ (x - 1) ^ p ^ k: expanding 1 = (1 + (x - 1)) ^ p ^ k by the binomial theorem, the extreme terms are 1 and (x - 1) ^ p ^ k, and every other binomial coefficient (p ^ k).choose m with 0 < m < p ^ k is divisible by p. No commutativity is needed, because x - 1 commutes with 1.

This is the integral shadow of the freshman's dream (x - 1) ^ p ^ k = x ^ p ^ k - 1 = 0 in characteristic p. It is what makes the group-like elements g - 1, for g of p-power order in a group algebra over the p-adic integers, topologically nilpotent.

Main result

• Nat.Prime.dvd_sub_one_pow_of_pow_eq_one: (p : A) ∣ (x - 1) ^ p ^ k when x ^ p ^ k = 1.

theorem Nat.Prime.dvd_sub_one_pow_of_pow_eq_one {A : Type u_1} [Ring A] {p : ℕ} (hp : Prime p) {x : A} {k : ℕ} (hx : x ^ p ^ k = 1) : ↑p ∣ (x - 1) ^ p ^ k

If x ^ p ^ k = 1 in a ring, for a prime p, then p divides (x - 1) ^ p ^ k.