mapPiEvalRingHom_bijective

Mathlib.RingTheory.Localization.AtPrime.Basic

URI: https://scilib.ai/kg/mathlib#Localization.AtPrime.mapPiEvalRingHom_bijective

English

The map pi-evaluation for primes is bijective.

Русский

Оценочное отображение по первичным идеалам является биективным.

LaTeX

$$$\\mathrm{mapPiEvalRingHom}\\, I\\; \\text{ is bijective}$$$

Lean4

theorem mapPiEvalRingHom_bijective : Function.Bijective (mapPiEvalRingHom I) :=
  Localization.mapPiEvalRingHom_bijective _

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

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

Разделы

Аффилиация

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