Northcott property for the norm of ideals in rings with finite quotients

For a ring with finite quotients, there are only finitely many ideals of bounded norm, see Ring.HasFiniteQuotients.finite_cardQuot_le. This file records the resulting Northcott instances.

instance Ring.HasFiniteQuotients.instNorthcottIdealNatCardQuot {R : Type u_1} [CommRing R] [HasFiniteQuotients R] : Northcott fun (p : Ideal R) => Submodule.cardQuot p

instance Ring.HasFiniteQuotients.instNorthcottIdealNatCoeMonoidWithZeroHomAbsNorm {R : Type u_1} [CommRing R] [HasFiniteQuotients R] [IsDedekindDomain R] : Northcott fun (I : Ideal R) => Ideal.absNorm I

instance Ring.HasFiniteQuotients.instNorthcottHeightOneSpectrumNatCoeMonoidWithZeroHomIdealAbsNormAsIdeal {R : Type u_1} [CommRing R] [HasFiniteQuotients R] [IsDedekindDomain R] : Northcott fun (p : IsDedekindDomain.HeightOneSpectrum R) => Ideal.absNorm p.asIdeal