Documentation

Mathlib.RingTheory.KrullDimension.NonZeroDivisors

Krull dimension and non zero-divisors #

Main results #

theorem ringKrullDim_succ_le_of_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Surjective f) {r : R} (hr : r nonZeroDivisors R) (hr' : f r = 0) :

If R →+* S is surjective whose kernel contains a nonzerodivisor, then dim S + 1 ≤ dim R.