mathlib documentation

algebra.char_p.quotient

Characteristic of quotients rings #

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 Ix = 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.