Noetherian quotient rings and quotient modules #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[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)