Documentation

Mathlib.Algebra.CharP.Quotient

Characteristic of quotients rings #

theorem CharP.quotient (R : Type u) [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 Ix = 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 Ix = 0

CharP.quotient' as an Iff.

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

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