zeroLocus_nilradical — Mathlib

English

The zero locus of a join of two ideals equals the intersection of their zero loci.

Русский

Нулевой локус суммы двух идеалов равен пересечению их нулевых локусов.

LaTeX

$$$ \operatorname{zeroLocus}((I \lor J) : Set R) = \operatorname{zeroLocus}(I) \cap \operatorname{zeroLocus}(J) $$$

Lean4

@[simp]
theorem zeroLocus_nilradical : zeroLocus (nilradical R : Set R) = Set.univ := by
  rw [nilradical, zeroLocus_radical, Ideal.zero_eq_bot, zeroLocus_bot]

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