instEssFiniteTypeQuotientIdeal

Mathlib.RingTheory.EssentialFiniteness

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

English

If S is EssFiniteType over R, then the quotient S/I is EssFiniteType over R for any ideal I of S.

Русский

Если S имеет EssFiniteType над R, то тождественный фактор S/I имеет EssFiniteType над R для любого идеала I в S.

LaTeX

$$EssFiniteType R S ⇒ EssFiniteType R (S / I)$$

Lean4

instance [EssFiniteType R S] (I : Ideal S) : EssFiniteType R (S ⧸ I) :=
  .comp R S _

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

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

Разделы

Аффилиация

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