isIdempotentElemEquivClopens_symm_top

Mathlib.RingTheory.Spectrum.Prime.Topology

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

English

The idempotent corresponding to the top clopen (the whole space) is the unit element 1 of the ring.

Русский

Идемпотент, соответствующий верхнему клозоподмножеству (всей спектр), равен единице кольца.

LaTeX

$$e^{−1}(\top) = ⟨1, ·\;\rbrace⟩$$

Lean4

theorem isIdempotentElemEquivClopens_symm_top : isIdempotentElemEquivClopens.symm ⊤ = ⟨(1 : R), .one⟩ :=
  map_top _

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

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

Разделы

Аффилиация

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