charP_zero_or_prime_power

theorem charP_zero_or_prime_power : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : LocalRing R] (q : ℕ) [char_R_q : CharP R q], q = 0 ∨ IsPrimePow q

This theorem states that for any commutative ring `R` that also has the structure of a local ring, and for any natural number `q` which is the characteristic of the ring `R`, the characteristic `q` is either equal to zero or it is a prime power. A number is said to be a prime power if there exists a prime number `p` and a positive natural number `k` such that `p` raised to the power `k` equals the number.

More concisely: In a commutative local ring R, the characteristic is either 0 or a prime power.