mathlib3 documentation

algebra.char_p.local_ring

Characteristics of local rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main result #

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] :

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