Characteristics of local rings #
Main result #
charP_zero_or_prime_power: In a commutative local ring the characteristics 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 characteristics is either zero or a prime power.