nilradical_eq_sInf — Mathlib

English

The nilradical of a commutative ring R equals the infimum (intersection) of all prime ideals of R.

Русский

Нильрадикал коммутативного кольца $R$ равен пересечению всех простых идеалов $R$ (инфиминум по множеству простых идеалов).

LaTeX

$$nilradical R = sInf {J : Ideal R | J.IsPrime}$$

Lean4

theorem nilradical_eq_sInf (R : Type*) [CommSemiring R] : nilradical R = sInf {J : Ideal R | J.IsPrime} :=
  (Ideal.radical_eq_sInf ⊥).trans <| by simp_rw [and_iff_right bot_le]

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