instIsNoetherianRing

Mathlib.RingTheory.AdjoinRoot

URI: https://scilib.ai/kg/mathlib#AdjoinRoot.instIsNoetherianRing

English

If R is Noetherian and f ∈ R[X], then AdjoinRoot f is a Noetherian ring (hence finite type over R).

Русский

Если R — кольцо Нётерово и f ∈ R[X], то AdjoinRoot f является Нётеровым кольцом.

LaTeX

$$IsNoetherianRing(AdjoinRoot f) holds if IsNoetherianRing(R)$$

Lean4

instance [CommRing R] [IsNoetherianRing R] {f : R[X]} : IsNoetherianRing (AdjoinRoot f) :=
  Ideal.Quotient.isNoetherianRing _

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

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

Разделы

Аффилиация

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