zeroLocus_eq_basicOpen_of_isIdempotentElem

English

For idempotent e, the zero locus of {e} equals the basic open of 1−e; i.e., V({e}) = D(1−e).

Русский

Для идемпотентного e нулевое множество {e} совпадает с базовым открытым D(1−e).

LaTeX

$$\\mathrm{V}({e}) = \\mathrm{D}(1 - e)$$

Lean4

@[stacks 00EC]
theorem zeroLocus_eq_basicOpen_of_isIdempotentElem (e : R) (he : IsIdempotentElem e) :
    zeroLocus { e } = basicOpen (1 - e) := by
  rw [basicOpen_eq_zeroLocus_of_isIdempotentElem _ he.one_sub, sub_sub_cancel]

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