zeroLocus_mul — Mathlib

English

For ideals I and J in R, the zero locus of their product equals the union of the zero loci:

Русский

Для идеалов I и J в R нулевой локус произведения равен объединению нулевых локусов:

LaTeX

$$$\\mathrm{zeroLocus}(I J) = \\mathrm{zeroLocus}(I) \\cup \\mathrm{zeroLocus}(J).$$$

Lean4

theorem zeroLocus_mul (I J : Ideal R) : zeroLocus ((I * J : Ideal R) : Set R) = zeroLocus I ∪ zeroLocus J :=
  Set.ext fun x => x.2.mul_le

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