mathlib documentation

ring_theory.quotient_noetherian

Noetherian quotient rings and quotient modules #

source
@[protected, instance]
def ideal.quotient.is_noetherian_ring {R : Type u_1} [comm_ring R] [h : is_noetherian_ring R] (I : ideal R) :
is_noetherian_ring (R ⧸ I)