zeroLocus_empty_of_one_mem — Mathlib

English

If 1 belongs to a set, then the zero locus is empty.

Русский

Если 1 принадлежит множеству, то нулевой локус пуст.

LaTeX

$$$ (1) \in s \Rightarrow \operatorname{zeroLocus}(s) = \emptyset $$$

Lean4

theorem zeroLocus_empty_of_one_mem {s : Set R} (h : (1 : R) ∈ s) : zeroLocus s = ∅ :=
  by
  rw [Set.eq_empty_iff_forall_notMem]
  intro x hx
  rw [mem_zeroLocus] at hx
  have x_prime : x.asIdeal.IsPrime := by infer_instance
  have eq_top : x.asIdeal = ⊤ := by
    rw [Ideal.eq_top_iff_one]
    exact hx h
  apply x_prime.ne_top eq_top

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