\import Algebra.Ring
\import Algebra.Ring.Ideal

\class NoetherianCRing \extends CRing
  | isNoetherian (I : Nat -> Ideal \this) : (\Pi (n : Nat) -> Ideal.IsFinitelyGenerated {I n}) -> Ideal.ChainCondition I