instEssFiniteTypeLocalization

Mathlib.RingTheory.EssentialFiniteness

URI: https://scilib.ai/kg/mathlib#Algebra.instEssFiniteTypeLocalization

← MathLib Explorer

English

If I is EssFiniteType over S, then the localization of S at M is EssFiniteType over R.

Русский

Если S имеет EssFiniteType над R и локализация S по M, то она имеет EssFiniteType над R.

LaTeX

$$EssFiniteType R S ⇒ EssFiniteType R (Localization M)$$

Lean4

instance [EssFiniteType R S] (M : Submonoid S) : EssFiniteType R (Localization M) :=
  have : EssFiniteType S (Localization M) := .of_isLocalization _ M
  .comp R S _

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

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

Разделы

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

Аффилиация

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