mathlib documentation


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 ( 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) :
char_p (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.