zeroLocus_empty_of_one_mem — Mathlib

English

If a subset s of A contains the unit element 1, then the vanishing locus of s in the projective spectrum is empty.

Русский

Если подмножество s ⊆ A содержит единицу 1, то множество обнуления vanishing в проективном спектре пусто.

LaTeX

$$$ (1 \in s) \Rightarrow \ zeroLocus_{\mathcal{A}}(s) = \emptyset $$$

Lean4

theorem zeroLocus_empty_of_one_mem {s : Set A} (h : (1 : A) ∈ s) : zeroLocus 𝒜 s = ∅ :=
  Set.eq_empty_iff_forall_notMem.mpr fun x hx =>
    (inferInstance : x.asHomogeneousIdeal.toIdeal.IsPrime).ne_top <|
      x.asHomogeneousIdeal.toIdeal.eq_top_iff_one.mpr <| hx h

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