ResidueField

Mathlib.RingTheory.LocalRing.ResidueField.Ideal

URI: https://scilib.ai/kg/mathlib#Ideal.ResidueField

Lean4

/-- The residue field at a prime ideal, defined to be the residue field of the local ring
`Localization.Prime I`.
We also provide an `IsFractionRing (R ⧸ I) I.ResidueField` instance.
-/
abbrev ResidueField : Type _ :=
  IsLocalRing.ResidueField (Localization.AtPrime I)

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

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

Разделы

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

Аффилиация

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