basicOpen_eq_zeroLocus_of_isIdempotentElem

Mathlib.RingTheory.Spectrum.Prime.Topology

URI: https://scilib.ai/kg/mathlib#PrimeSpectrum.basicOpen_eq_zeroLocus_of_isIdempotentElem

← MathLib Explorer

English

For an idempotent element e ∈ R, the basic open set D(e) equals the zero locus V(1−e).

Русский

Для идемпотентного элемента e верно D(e) = V(1−e).

LaTeX

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

Lean4

@[stacks 00EC]
theorem basicOpen_eq_zeroLocus_of_isIdempotentElem (e : R) (he : IsIdempotentElem e) :
    basicOpen e = zeroLocus {1 - e} :=
  basicOpen_eq_zeroLocus_of_mul_add _ _ (by simp [mul_sub, he.eq]) (by simp)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru