isRadical_iff_quotient_reduced — Mathlib

English

For a commutative ring R and an ideal I, I is radical iff the quotient R/I is reduced.

Русский

Для коммутативного кольца R и идеала I справедливо: I радикален тогда и только тогда, когда R/I редуцировано (без ненулевых нильпотентов).

LaTeX

$$$$I \text{ radical} \;\Longleftrightarrow\; R/I \text{ is reduced}.$$$$

Lean4

theorem isRadical_iff_quotient_reduced {R : Type*} [CommRing R] (I : Ideal R) : I.IsRadical ↔ IsReduced (R ⧸ I) :=
  by
  conv_lhs => rw [← @Ideal.mk_ker R _ I]
  exact RingHom.ker_isRadical_iff_reduced_of_surjective Quotient.mk_surjective

Похожие утверждения