Characteristic of quotients rings #

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

theorem char_p.quotient (R : Type u) [comm_ring R] (p : ℕ) [hp1 : fact (nat.prime p)] (hp2 : ↑p ∈ nonunits R) :

theorem char_p.quotient' {R : Type u_1} [comm_ring R] (p : ℕ) [char_p R p] (I : ideal R) (h : ∀ (x : ℕ), ↑x ∈ I → ↑x = 0) :

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} [comm_ring R] (I : ideal R) :