Characteristics of local rings

Main result

• charP_zero_or_prime_power: In a commutative local ring the characteristic is either zero or a prime power.

theorem charP_zero_or_prime_power (R : Type u_1) [CommRing R] [IsLocalRing R] (q : ℕ) [char_R_q : CharP R q] : q = 0 ∨ IsPrimePow q

In a local ring the characteristic is either zero or a prime power.