instAtPrimeSubtypeMemSubringToSubringOfPrime

Mathlib.RingTheory.LocalRing.LocalSubring

URI: https://scilib.ai/kg/mathlib#LocalSubring.instAtPrimeSubtypeMemSubringToSubringOfPrime

English

IsLocalization.AtPrime (ofPrime A P).toSubring P holds; AtPrime structure on localization at prime.

Русский

IsLocalization.AtPrime для локализации по простому A P обеспечивает структуру AtPrime.

LaTeX

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

Lean4

instance : IsLocalization.AtPrime (ofPrime A P).toSubring P :=
  IsLocalization.isLocalization_of_algEquiv _ (ofPrimeEquiv A P)

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

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

Разделы

Аффилиация

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