Localizations

Mathlib.AlgebraicGeometry.Modules.Tilde

URI: https://scilib.ai/kg/mathlib#ModuleCat.Tilde.Localizations

Lean4

/-- For an `R`-module `M` and a point `P` in `Spec R`, `Localizations P` is the localized module
`M` at the prime ideal `P`. -/
abbrev Localizations (P : PrimeSpectrum.Top R) :=
  LocalizedModule P.asIdeal.primeCompl M

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

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

Разделы

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

Аффилиация

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