zeroLocus_mul_ideal — Mathlib

English

The vanishing locus of the product of two ideals I and J equals the union of their vanishing loci.

Русский

Для произведения идеалов I и J нуль-множество равно объединению нуль-множеств.

LaTeX

$$$ \operatorname{zeroLocus}_{\mathcal{A}}((I J) : Set A) = \operatorname{zeroLocus}_{\mathcal{A}}(I) \cup \operatorname{zeroLocus}_{\mathcal{A}}(J) $$$

Lean4

theorem zeroLocus_mul_ideal (I J : Ideal A) : zeroLocus 𝒜 ((I * J : Ideal A) : Set A) = zeroLocus 𝒜 I ∪ zeroLocus 𝒜 J :=
  Set.ext fun x => x.isPrime.mul_le

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