ofPrime_localization

Mathlib.RingTheory.Valuation.ValuationSubring

URI: https://scilib.ai/kg/mathlib#ValuationSubring.ofPrime_localization

← MathLib Explorer

English

There is a localization-at-prime for A.ofPrime P with respect to P.

Русский

Существует локализация на простом идеале P для A.ofPrime P.

LaTeX

$$IsLocalization.AtPrime (A.ofPrime P) P$$

Lean4

instance ofPrime_localization (A : ValuationSubring K) (P : Ideal A) [P.IsPrime] :
    IsLocalization.AtPrime (A.ofPrime P) P := by
  apply Localization.subalgebra.isLocalization_ofField K P.primeCompl P.primeCompl_le_nonZeroDivisors

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

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

Разделы

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

Аффилиация

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