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 ∈ I → ↑x = 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.

theorem Ideal.Quotient.index_eq_zero {R : Type u_1} [CommRing R] (I : Ideal R) : ↑(AddSubgroup.index (Submodule.toAddSubgroup I)) = 0