Changelog

chore(deps): bump the actions-version-updates group across 1 directory with 11 updates (#45153) …

fix(Cache): retry uploads and report missing transfers (#44940) …

doc: add external proofs to the 100 theorems list (#44489) …

ci: pin ensure-sha-pinned-actions to the leanprover-community fork (#45143) …

feat(Algebra/QuadraticAlgebra): classify quadratic algebras over ℚ (#42393) …

chore(LinearAlgebra/Matrix/Rank): remove unnecessary `nontriviality`s (#45117)

feat(Analysis/Matrix/Normed): prove `‖A i j‖ ≤ ‖A‖` for the operator norm (#44969) …

chore: more filter generalizations in tsum/tprod lemmas (#44511) …

chore: deprecate `FP.Float` (#44425) …

chore: fix a non-reducible diamond in `MvPowerSeries` (#44400) …

feat(Analysis/Normed/Ring/WithAbs): more API for `AbsoluteValue.under` (#43841) …

chore: whitespace fixes (#45125) …

chore(Analysis/Calculus/FDeriv/Analytic): tag more @[fun_prop] (#45102)

chore: bump ProofWidgets to v0.0.118 (#45113) …

feat: use `IsApply` for `FiniteMeasure` (#45123)

feat: use `IsApply` for `BoundedContinuousFunction` (#45087)

feat: use `IsApply` for `SimpleFunc` (#45077)

chore: generalize lemmas about measurability of biUnion (#45097) …

refactor: `Cardinal.card_le_iff` → `Ordinal.card_le_iff` (#45105) …

chore: modulize `docs` (#45107) …

feat(Tactic/Linter/Header): access library root without cwd (#45061) …

feat(CategoryTheory/Abelian/TorsionTheory): Introduce torsion theory for abelian categories (#36744) …

chore: update Mathlib dependencies 2026-10-20 (#45100) …

feat(Tactic/Linter/Header): suggest formatting imports according to the style convention (#44507) …

fix(Linter/UnusedTactic): don't use `IO.Ref` for extensibility (#42536) …

doc(Topology/Algebra/Monoid/Defs): fix docstring typo (#45092) …

chore(GroupTheory/Nilpotent): split off material on lower central series (#43348) …

chore: revert "feat: enable Verso if no syntax or doc-gen changes (#45031)" (#45094) …

chore(Data/Finsupp/Quotient): automated extraction from #28013 (#45090) …

chore(Data/Finset/Union): tag biUnion lemmas with grind (#43806) …

feat: lattice lemmas about `Submodule.toAffineSubspace` (#43415)

chore(Algebra/MonoidAlgebra/Basic): automated extraction from #28013 (#45088) …

feat(CategoryTheory): kan extensions from isos (#41484) …

chore(RingTheory/IntegralClosure/IsIntegralClosure/Basic): automated extraction from #28013 (#45086) …

chore: remove unused tactics (#45073) …

feat(Tactic/Hessenberg): an algorithm that computes the characteristic polynomial of an Hessenberg matrix (#44431) …

feat(Analysis/SpecialFunctions): the recurrence relation of bessel function J (#43853) …

feat: add some lemmas that closures of some sets are compact (#39382) …

fix(rm_set_option.py): don't cause build warnings (#45074) …

chore: reformat imports (#45071) …

fix(Topology/Algebra/InfiniteSum/ENNReal): add missing deprecation alias (#45070) …

feat(Combinatorics/SimpleGraph/Paths): add lemma about the first dart if dropLast is a path (#40963) …

feat: enable Verso if no syntax or doc-gen changes (#45031) …

chore: fix uses of `notation3` (#45041) …

chore: update Mathlib dependencies 2026-10-20 (#45065) …

fix(scripts/mk_all): don't add a linter exception to the generated fi… (#45052) …

chore: update Mathlib dependencies 2026-10-20 (#45060) …

feat(Topology/Algebra/InfiniteSum): Generalize ENNReal lemmas (#38489) …

chore: additivize the profinite completion (#44627) …

fix(Translate): don't panic when `existing` is missing (#45049) …