Commit 2026-03-10 06:45 5c8398df

feat(RingTheory): add the class HasFiniteQuotients (#35530) As discussed on Zulip, this PR add the class of commutative rings R such that, for all nonzero ideals I of R, the quotient R ⧸ I is finite and prove several results including:

• If R has finite quotients then it has dimension ≤ 1
• If R has finite quotients then it is a Noetherian ring
• Assume that R a finite quotients and that S is a domain and a finite R-module. Then S has finite quotients
• A domain that is also a finite ℤ-module has finite quotients. Also add two instances:
• Assume that S is a finite R-module and that S ⧸ J is a (R ⧸ I)-module with I, resp. J, an ideal of R, resp. S, then S ⧸ J is a finite (R ⧸ I)-module.
• For nonzero n , ℤ ⧸ Ideal.span {n} is finite.