zeroLocus_span — Mathlib

English

The zero locus depends only on the span of s: zeroLocus(span s) = zeroLocus(s).

Русский

Нулевая локация зависит только от линейного обобщения s: zeroLocus(span s) = zeroLocus(s).

LaTeX

$$$\\operatorname{zeroLocus}(\\\\operatorname{Ideal.span} s) = \\operatorname{zeroLocus}(s)$$$

Lean4

@[simp]
theorem zeroLocus_span (s : Set R) : zeroLocus (Ideal.span s : Set R) = zeroLocus s :=
  by
  ext x
  exact (Submodule.gi R R).gc s x.asIdeal

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