Characteristic of quotients rings #

theorem CharP.quotient (R : Type u) [CommRing R] (p : ) [hp1 : Fact (Nat.Prime p)] (hp2 : p nonunits R) :
CharP (R Ideal.span {p}) p
theorem CharP.quotient' {R : Type u_1} [CommRing R] (p : ) [CharP R p] (I : Ideal R) (h : ∀ (x : ), x Ix = 0) :
CharP (R I) p

If an ideal does not contain any coercions of natural numbers other than zero, then its quotient inherits the characteristic of the underlying ring.