isNoetherianRing

Mathlib.RingTheory.PrincipalIdealDomain

URI: https://scilib.ai/kg/mathlib#PrincipalIdealRing.isNoetherianRing

← MathLib Explorer

English

In a domain, the generator of the principal ideal span{r} is associated to r.

Русский

В области, порождающий элемент идеала span{r} ассоциирован с r.

LaTeX

$$Associated (generator (Ideal.span { r })) r$$

Lean4

instance (priority := 100) _root_.PrincipalIdealRing.isNoetherianRing [IsPrincipalIdealRing R] : IsNoetherianRing R
    where noetherian S := (IsPrincipalIdealRing.principal S).fg

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

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

Разделы

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

Аффилиация

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