Tags: vvs-/EGPT

doc(FieldTheory): fix typos (leanprover-community#36560)

Found by `PyCharm`'s code inspection tool. Fixes were made by Codex.

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

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

chore(Topology/Sets/Compacts): use `fast_instance%` (leanprover-commu…

…nity#37348)

Using `fast_instance%` here should remove some diamonds.

chore: remove stray adaptation_note (leanprover-community#37329)

follow-up to leanprover-community#37326

chore(PowerSeries): remove duplicate instances (leanprover-community#…

…37289)

Since `PowerSeries` is an abbrev for `MvPowerSeries`, all instances are inherited automatically. This PR removes the duplicate instances.

There is a bunch of material duplicated in `PowerSeries/Inverse.lean` which is already proved in `MvPowerSeries/Inverse.lean`. That may be removed in a future PR.

feat(EisensteinSeries): q-expansion coefficients and non-vanishing fo…

…r E_k (leanprover-community#37250)

## Summary
- Add `ArithmeticFunction.sigma_le_pow_succ`: crude bound `σ_k(n) ≤ n^{k+1}`
- Add `EisensteinSeries.E_qExpansion_coeff`: all q-expansion coefficients of normalised Eisenstein series E_k (constant term 1, higher terms `-(2k/B_k) * σ_{k-1}(m)`)
- Add `EisensteinSeries.E_qExpansion_coeff_zero`: constant coefficient is 1
- Add `EisensteinSeries.E_ne_zero`: E_k is non-zero for even k ≥ 3
- Improve docstring for `ModularFormClass.qExpansion`

### This is coming from the Sphere packing project.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

chore(Mathlib/Algebra/Lie/Subalgebra.lean): automated extraction (lea…

…nprover-community#37203)

This PR was automatically created from PR leanprover-community#34727 by @ocfnash via a [review comment](leanprover-community#34727 (comment)) by @jcommelin.

Co-authored-by: ocfnash <7734364+ocfnash@users.noreply.github.com>

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

feat: define bases of semisimple Lie algebras and add API (leanprover…

…-community#36298)

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

…er-community#36759)

Most of the diff is just re-sectioning.