Characteristic of quotient rings

theorem CharP.ker_intAlgebraMap_eq_span {R : Type u_1} [Ring R] (p : ℕ) [CharP R p] : RingHom.ker (algebraMap ℤ R) = Ideal.span {↑p}

theorem CharP.quotient (R : Type u_1) [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 CharP.quotient_iff {R : Type u_1} [CommRing R] (n : ℕ) [CharP R n] (I : Ideal R) : CharP (R ⧸ I) n ↔ ∀ (x : ℕ), ↑x ∈ I → ↑x = 0

CharP.quotient' as an Iff.

theorem CharP.quotient_iff_le_ker_natCast {R : Type u_1} [CommRing R] (n : ℕ) [CharP R n] (I : Ideal R) : CharP (R ⧸ I) n ↔ Ideal.comap (Nat.castRingHom R) I ≤ RingHom.ker (Nat.castRingHom R)

CharP.quotient_iff, but stated in terms of inclusions of ideals.

theorem Ideal.natCast_mem_of_charP_quotient {R : Type u_1} [CommRing R] (p : ℕ) (I : Ideal R) [CharP (R ⧸ I) p] : ↑p ∈ I

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