isNoetherianRing

Mathlib.RingTheory.Ideal.Quotient.Noetherian

URI: https://scilib.ai/kg/mathlib#Ideal.Quotient.isNoetherianRing

← MathLib Explorer

English

IsNoetherianRing (R/I) holds for any ideal I when R is Noetherian.

Русский

Если R — Неттеново кольцо, то R/I — Неттеново для любого идеала I.

LaTeX

$$$$\text{IsNoetherianRing}(R/I).$$$$

Lean4

instance isNoetherianRing {R : Type*} [CommRing R] [IsNoetherianRing R] (I : Ideal R) : IsNoetherianRing (R ⧸ I) :=
  isNoetherianRing_iff.mpr <| isNoetherian_of_tower R <| inferInstance

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

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

Разделы

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

Аффилиация

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