Changelog

chore: deprecate removed modules (#32762)

feat(Analysis/Distribution): definition of tempered distributions (#31757) …

chore: use `Set.Nonempty` everywhere (#32697)

feat(NumberTheory/ArithmeticFunction/Carmichael): Carmichael totient function (#32414) …

feat(Combinatorics/SimpleGraph/Acyclic): `IsAcyclic` -> `IsBipartite` (#32568) …

chore(*): adaptations for batteries#1545 (#32581) …

chore: uniformize theorem naming (#32726) …

fix(ci): use bot token for discover-lean-pr-testing merges (#32722) …

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

doc: add mutual references to doc strings of `AEMeasurable` and `NullMeasurable` (#32593)

feat(CategoryTheory): combine pullback cones in the functor category (#32618)

fix(NumberTheory/MahlerMeasure): add missing public section (#32727) …

chore: replace `omega` with `lia` where possible (#32666) …

chore: absorb steps into terminal `grind` (#32713) …

doc: fix typos in the docstring of `Sigmoid` (#32700) …

doc(1000.yml): mention the Riemann mapping theorem (#32689)

feat: specialize `[pre, post]comp_uniformConvergenceCLM` to `CompactConvergenceCLM` (#32395)

feat: colex order on finsupps (#31019)

chore(RingTheory/Smooth): demote superseded `instance` to `theorem` (#32720) …

feat(LinearAlgebra/PiTensorProduct): add version of `subsingletonEquiv` for dependent case (#32598) …

feat(Polynomial/Roots): add a theorem for computing roots (#32357) …

refactor: have `MetrizableSpace` not depend on `MetricSpace` (#27946) …

doc(GroupTheory/Coset): mention RightActions notation for right cosets (#32718) …

fix(Algebra/Field): ensure `Field.toGrindField.toInv` is def-eq to `Field.toInv` (#32711) …

chore: add missing deprecations (#32705) …

chore: notation `R⟦Γ⟧ = HahnSeries Γ R` (#32670) …

feat(Algebra/Homology): more API for the HomComplex from a single cochain complex (#32461)

feat(CategoryTheory/Localization): inverse in `SmallShiftedHom` (#32442) …

feat(Algebra): add Subsemigroup.op (#32428) …

feat(CategoryTheory): the Yoneda embedding for a locally small category (#32424) …

feat(CategoryTheory): commutation of bifunctors with shifts in two variables (#32303) …

refactor(Geometry/Euclidean/Projection): redefine projection and reflection for affine subspaces (#27378) …

feat(RingTheory/Perfectoid): Fontaine's theta map is surjective (#26384) …

feat: add `@[grind inj]` to `Finset.coe_injective` (#32714) …

feat(CategoryTheory): right Bousfield localization (#32469) …

feat(CategoryTheory): more preservation properties of functors (#32423) …

feat(CategoryTheory): monomorphisms in Type are stable under coproducts (#32515) …

feat(CategoryTheory/Sites): the category structure on the points of a site (#31711)

doc(undergrad/overview): add test functions and distributions (#32707)

refactor: re-prove Euler's partition theorem from Glaisher's theorem (#31873) …

chore: test `initialize` in private module linter (#32695) …

feat(CategoryTheory): the opposite of a triangulated category is triangulated (#32535)

feat(Geometry/Euclidean/Incenter): `orthRadius` lemmas (#31733) …

feat(Analysis/Distribution): composition of temperate growth functions (#32297) …

feat(Trigonometry): add tanh_eq (#32694) …

feat(Topology/AddCircle): remove `0 < p` condition from `finite_torsion` (#32691)

feat(Combinatorics/SimpleGraph/Walk): lemmas about the first and last darts/edges (#31416)

chore: use `Set.Nonempty` in ProperlyDiscontinuous (#32693) …

refactor: add gcongr tag to IsMeagre.mono (#32686) …

feat(Analysis/Calculus): norm bound for iterated derivatives of composition with CLM (#32572)