Changelog

chore: remove some 'nonrec' (#19907) …

chore: run 'lake build AesopTest' on nightlies (#29697) …

chore: generalize `ContinuousAffineMap.contLinear` to `IsTopologicalAddTorsor` (#29617)

feat(gcongr): `@[gcongr]` for `gcd` and `IsCoprime` (#29889) …

fix(Tactic/ToAdditive/Frontend): swap `reorderForall` and `applyReplacementForall` (#29119) …

feat(Algebra/Homology): define projective dimension as a number (#29882) …

chore(Data/Nat/Init): remove `@[instance]` from `instAtLeastTwo` (#29832) …

chore: clean up some proofs about locally compact valuation (#28669)

chore: remove redundant `haveI`/`letI` (#29908) …

chore(Geometry/Euclidean/SignedDist): use `normalize` (#29897) …

feat(Order/Filter/Basic): `gcongr` for `EventuallyEq` (#29747) …

feat(Tactic/FieldSimp): handle inequalities (#29364) …

feat: norm_num extension for abs (#29223) …

chore(MeasureTheory): semilinearize composition of integrals with CLM (#29853)

feat(MeasureTheory/Integral/IntegrableOn): add `IntegrableOn.of_inter_support` (#29895) …

feat(MeasureTheory): Convolution of `dirac`s (#29826) …

feat(MeasureTheory): Add `mconv_smul_left` and `mconv_smul_right` (#29825)

feat(ProbabilityTheory): Add `moment_def` and `moment_one` (#29902) …

chore: update Mathlib dependencies 2025-09-23 (#29905) …

feat: the complete graph is connected iff nonempty (#29901) …

feat(NumberTheory/ModularForms): integrand for Petersson product (#29640) …

feat(Data/Set/Card): every finset of card less than `ENat.card α` doesn't contain some element (#29900) …

feat: extensible `push` and `pull` tactics (#21965) …

fix(Cache): misleading ProofWidgets fetch failure (#29886) …

feat: range of the continuous functional calculus (#29561) …

feat(CategoryTheory/Sites): jointly surjective precoverage (#29883) …

feat(Topology/Constructions): `piMap` is inducing / embedding / etc (#29648) …

feat(Ring/DedekindDomain): formula for the splitting of prime ideals in an extension (#27105) …

feat: some lemmas about closed maps (#29144) …

feat(LinearAlgebra/AffineSpace/Ordered): add `lineMap_le_lineMap_iff_of_lt'` (#27257) …

feat(Algebra/Homology): the derived category of a linear abelian category is linear (#26031)

chore(Analysis/Normed/Completeness): Generalize extend to uniform groups (#29869) …

feat(ConstMulAction): prove `set_smul_closure_subset` (#29859) …

chore(MeasureTheory): Semilinearize integrable_comp of CLM and CLE (#29852)

feat(Data/Matrix): add `vecMul_fromRows` and `fromCols_mulVec` (#29784) …

chore(InnerProductSpace/OfNorm): golf (#29783) …

feat: restricted power series form a ring (#26089) …

feat: grind annotations for `Finset.sdiff` (#29427) …

chore(Algebra/Category/Grp): don't import `AddCircle` in `Injective.lean` (#29811) …

feat(Tactic/Ring): handle `ℤ`-scalar multiplication in the ring tactic (#29782) …

feat(NumberTheory/ModularForms): tweak def of slash-action (#29804) …

docs(Analysis/Calculus/Gradient/Basic): decapitalize (#29847)

chore(Data/Nat/Choose): add le-version of a bound and fix name of the lt-version (#29821)

chore(RingTheory/AdicValuation): golf using WithZero.log (#27108) …

feat(Geometry/Euclidean/Sphere/Power): use side condition `p ∈ line[ℝ, a, b]` (#29344) …

feat(Algebra): add `mem_closure_iff_of_fintype` and `mem_closure_finset'` (#29793) …

feat(Topology/Maps): `IsOpenMap` and `ClusterPt` (#23240)

feat: isomorphic monoid objects have isomorphic hom monoids (#29830) …

chore: reduce `open Fin.NatCast` (#29840) …

feat(Analysis/Convex/Between): interior of a 1-simplex (#29418) …