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) :