IsNoetherianRing — Mathlib

English

A (semi)ring is Noetherian if it is Noetherian as a module over itself, i.e., all its ideals are finitely generated.

Русский

Кольцо (полугруппа) называется Нётеровым, если оно является Нётеровым как модуль над самим собой, то есть все его идеалы конечножгенерированы.

LaTeX

$$$\\text{IsNoetherianRing}(R) \\equiv \\text{IsNoetherian}(R,R)$$$

Lean4

/-- A (semi)ring is Noetherian if it is Noetherian as a module over itself,
i.e. all its ideals are finitely generated. -/
abbrev IsNoetherianRing (R) [Semiring R] :=
  IsNoetherian R R

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