Changelog

fix: improve `recall` impl / error reporting (#8740) …

fix(Tactic/Recall): allow different universe variable names (#37145) …

ci: add permissions to rm_set_option.yml (#37169) …

feat(RingTheory): adds lemmas/instances related to integral maps to a field and residue fields (#36790) …

feat(RingTheory/AdicCompletion): completeness of `AdicCompletion` (#35670) …

chore: golf using `grind` and `simp` (#36645) …

chore(NumberTheory/RamificationInerta/Basic): split file (#37173) …

chore: modulize tests (4/N) (#36981)

feat(AlgebraicTopology/SimplicialSet): nondegenerate simplices in `Δ[p] ⊗ Δ[q]` of maximal dimension (#36987) …

fix(scripts/autolabel): only drop dependent labels (#37176) …

chore: golf rcases + subst (#37136) …

chore: remove unnecessary `backward.inferInstanceAs.wrap` (#37154) …

chore(Algebra/Colimit/Ring): use `deriving` for `CommRing DirectLimit` (#37139) …

chore(Algebra/Order/Nonneg/Lattice): clean up instances (#37157) …

feat(RingTheory/Localization/Integral): generalize `IsFractionRing.integerNormalization_eq_zero_iff` (#37003) …

refactor: make `Unitization` into a one-field structure (#37014) …

feat(RingTheory/Length): length of a module along a quotient map (#37126) …

chore: reduce use of `RestrictScalars` (#36694) …

refactor(GroupTheory/Commutator/Basic): to_additivize commutators (#34784) …

feat(LinearAlgebra): dimension of `P →ᵃ[R] W` (#36006)

chore(GroupTheory/Coxeter/Length): deprecate nat subtraction lemmas (#37152) …

feat(Topology/UniformSpace/Closeds): `(Nonempty)Compacts.toCloseds` is a closed embedding (#34270)

ci: add global timeout to rm_set_option.py (#37163) …

feat(Analysis/Convex/Cone): min and max tensor products are equal when one factor is simplicial and generating (#34848) …

chore(Tactic/Recall): suppress unused variable linter (#37143) …

chore(NumberField): clean up `RingOfIntegers` instances (#37153) …

chore(Padics/PadicNumbers): delta derive the instances (#37140) …

feat: decompose ideal-Cartan intersection via coroot spans (#37142) …

refactor(NumberTheory/RamificationInertia/Basic): remove the ring homomorphism from `Ideal.ramificationIdx` (#37156) …

feat(Analysis/Topology): Generalize Riesz' theorem to locally compact… (#36447) …

chore(GroupTheory/Coxeter/Length): remove backward.privateInPublic (#37150) …

feat: define bases of semisimple Lie algebras and add API (#36298)

feat(scripts/autolabel): collect label dependencies transitively (#36242) …

feat(Tactic/Recall): allow docstrings on `recall` (#37141) …

chore(TrivSqZeroExt): clean up instances (#37137) …

feat: affine isomorphisms between spaces of affine maps (#35998) …

ci: add workflow to remove unnecessary set_option lines (#37128) …

feat(Topology/Category): `TopCat` is cartesian monoidal (#37097)

chore(RingTheory/AdjoinRoot): clean up instances (#37127) …

chore(GroupTheory/FreeAbelianGroup): clean up instances more (#37125) …

chore: remove declarations deprecated between 2021-03-24 and 2025-09-24 (#37118) …

feat(SetTheory/Ordinal): fundamental sequences (#37019) …

chore(DirectSum): clean up instances (#37135) …

chore: avoid `by change; infer_instance` (#37102) …

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

feat(NumberTheory/Primorial): expand API for primorial (#36962) …

doc(Topology): fix typos (#37089) …

doc(Analysis): fix typos (#37088) …

chore: golf using `grind` and `simp` (#36684) …

chore: golf proofs (#36014) …