zeroLocus_singleton_mul — Mathlib

English

For elements f and g in R, the zero locus of the product fg equals the union of the zero loci of f and g as singletons:

Русский

Для элементов f и g в R нулевой локус произведения fg равен объединению нулевых локусов одиночек f и g:

LaTeX

$$$\\mathrm{zeroLocus}({f g}) = \\mathrm{zeroLocus}({f}) \\cup \\mathrm{zeroLocus}({g}).$$$

Lean4

theorem zeroLocus_singleton_mul (f g : R) : zeroLocus ({f * g} : Set R) = zeroLocus { f } ∪ zeroLocus { g } :=
  Set.ext fun x => by simpa using x.2.mul_mem_iff_mem_or_mem

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