piLocalizationToMaximal_surjective

Mathlib.RingTheory.Spectrum.Maximal.Localization

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

← MathLib Explorer

English

The map piLocalizationToMaximal is surjective.

Русский

Отображение piLocalizationToMaximal сюръективно.

LaTeX

$$$\mathrm{piLocalizationToMaximal}(R)$ is surjective$$

Lean4

theorem piLocalizationToMaximal_surjective : Function.Surjective (piLocalizationToMaximal R) := fun r ↦
  ⟨fun I ↦ if h : I.1.IsMaximal then r ⟨_, h⟩ else 0, funext fun _ ↦ dif_pos _⟩

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

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

Разделы

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

Аффилиация

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