zeroLocus_subset_zeroLocus_singleton_iff

English

For f,g in R, zeroLocus({f}) ⊆ zeroLocus({g}) iff g ∈ radical(span{f}).

Русский

Для элементов f,g кольца R, zeroLocus({f}) ⊆ zeroLocus({g}) тогда и только тогда, когда g ∈ radical(span{f}).

LaTeX

$$$ \operatorname{zeroLocus}(\{f\}) \subseteq \operatorname{zeroLocus}(\{g\}) \iff g \in \operatorname{radical}(\operatorname{span} \{f\}) $$$

Lean4

theorem zeroLocus_subset_zeroLocus_singleton_iff (f g : R) :
    zeroLocus ({ f } : Set R) ⊆ zeroLocus { g } ↔ g ∈ (Ideal.span ({ f } : Set R)).radical := by
  rw [← zeroLocus_span { f }, ← zeroLocus_span { g }, zeroLocus_subset_zeroLocus_iff, Ideal.span_le,
    Set.singleton_subset_iff, SetLike.mem_coe]

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