Characteristics of local rings #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Main result #
char_p_zero_or_prime_power: In a commutative local ring the characteristics is either zero or a prime power.
theorem
char_p_zero_or_prime_power
(R : Type u_1)
[comm_ring R]
[local_ring R]
(q : ℕ)
[char_R_q : char_p R q] :
q = 0 ∨ is_prime_pow q
In a local ring the characteristics is either zero or a prime power.