v4.30.0-rc1

chore: bump toolchain to v4.30.0-rc1 (#37564)

Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
Co-authored-by: Robin Arnez <152706811+Rob23oba@users.noreply.github.com>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Joscha <joscha@plugh.de>
Co-authored-by: mathlib-nightly-testing[bot] <258991302+mathlib-nightly-testing[bot]@users.noreply.github.com>

v4.29.0

chore: bump toolchain to v4.29.0 (#37377)

Co-authored-by: Joscha <joscha@plugh.de>

v4.29.0-rc8

chore: bump toolchain to v4.29.0-rc8 (#37133)

v4.29.0-rc7

feat: `∃ a, f a ≤ x < f (succ a)` for a normal function `f` (#36759)

Most of the diff is just re-sectioning.

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.

v4.29.0-rc4

feat(ContinuousMultilinearMap): generalize some definitions (#34491)

... from normes spaces to topological vector spaces

v4.29.0-rc3

chore: bump toolchain to v4.29.0-rc3 (#35942)

Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com>
Co-authored-by: mathlib-nightly-testing[bot] <258991302+mathlib-nightly-testing[bot]@users.noreply.github.com>

v4.29.0-rc2

chore(Tactic): improve `econstructor` and `fconstructor` tactic docst…