zeroLocus_radical — Mathlib

English

The zero locus does not change when passing to the radical of an ideal: zeroLocus(I.radical) = zeroLocus(I).

Русский

Нулевой локус не меняется при переходе к радикалу идеала: zeroLocus(I.radical) = zeroLocus(I).

LaTeX

$$$ \operatorname{zeroLocus}(I^{\mathrm{radical}}) = \operatorname{zeroLocus}(I) $$$

Lean4

@[simp]
theorem zeroLocus_radical (I : Ideal R) : zeroLocus (I.radical : Set R) = zeroLocus I :=
  vanishingIdeal_zeroLocus_eq_radical I ▸ (gc R).l_u_l_eq_l I

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