v4.29.0-rc6

feat(RingTheory): add the class `HasFiniteQuotients` (#35530)

As discussed on [Zulip](https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Rings.20with.20finite.20quotients/with/574554760), 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.