Reduced rings embed into their minimal-prime quotients

Since the minimal primes of a reduced ring intersect in 0, a reduced ring embeds into the product of its quotients by its minimal primes. No finiteness of the set of minimal primes is needed.

Main results

• Ideal.injective_pi_quotient_mk_minimalPrimes: a reduced ring embeds into the product of its quotients by its minimal primes.

theorem Ideal.injective_pi_quotient_mk_minimalPrimes (A : Type u_1) [CommRing A] [IsReduced A] : Function.Injective ⇑(RingHom.pi fun (p : ↑(minimalPrimes A)) => Quotient.mk ↑p)

A reduced ring embeds into the product of its quotients by its minimal primes: the intersection of the minimal primes is the nilradical, which is 0.