zeroLocus_subset_zeroLocus_iff — Mathlib

English

For ideals I,J, zeroLocus(I) ⊆ zeroLocus(J) iff J ≤ radical(I).

Русский

Для идеалов I, J верно: zeroLocus(I) ⊆ zeroLocus(J) тогда и только тогда, когда J ≤ radical(I).

LaTeX

$$$ \operatorname{zeroLocus}(I) \subseteq \operatorname{zeroLocus}(J) \iff J \le \operatorname{radical}(I) $$$

Lean4

theorem zeroLocus_subset_zeroLocus_iff (I J : Ideal R) :
    zeroLocus (I : Set R) ⊆ zeroLocus (J : Set R) ↔ J ≤ I.radical := by
  rw [subset_zeroLocus_iff_le_vanishingIdeal, vanishingIdeal_zeroLocus_eq_radical]

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