zeroLocus_sup — Mathlib

English

zeroLocus of the join equals the intersection, i.e., zeroLocus(I ⊔ J) = zeroLocus(I) ∩ zeroLocus(J).

Русский

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

LaTeX

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

Lean4

theorem zeroLocus_sup (I J : Ideal R) : zeroLocus ((I ⊔ J : Ideal R) : Set R) = zeroLocus I ∩ zeroLocus J :=
  (gc R).l_sup

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