vanishingIdeal_zeroLocus_eq_radical

English

For any ideal I of R, vanishingIdeal(zeroLocus(I)) equals the radical of I.

Русский

Для любого идеала I кольца R равняется radical(I) равен vanishingIdeal(zeroLocus(I)).

LaTeX

$$$ \operatorname{vanishingIdeal}(\operatorname{zeroLocus}(I)) = \operatorname{radical}(I) $$$

Lean4

@[simp]
theorem vanishingIdeal_zeroLocus_eq_radical (I : Ideal R) : vanishingIdeal (zeroLocus (I : Set R)) = I.radical :=
  Ideal.ext fun f => by
    rw [mem_vanishingIdeal, Ideal.radical_eq_sInf, Submodule.mem_sInf]
    exact ⟨fun h x hx => h ⟨x, hx.2⟩ hx.1, fun h x hx => h x.1 ⟨hx, x.2⟩⟩

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