Changelog

doc(MeasureTheory): ensure only a single H1 header per file (#31618) …

doc(Data): misc. improvements (#31431) …

chore(LinearAlgebra/AffineSpace): golf entire `attach_affineCombination_of_injective` using `simp` (#31363)

feat: generalize continuity results for the continuous functional calculus (#30594) …

feat(Topology/Separation): condition for regularity given a subbasis (#31387)

feat(Geometry/Euclidean/Angle/Bisector): oriented angle bisection and equal distance (#30477) …

feat(Analysis/InnerProductSpace/Basic): add a simp lemma (#30793) …

chore: update Mathlib dependencies 2025-11-14 (#31627) …

feat: Subgroup.mem_sup for arbitrary groups when one of the subgroups is normal (#31458) …

doc(MathlibTest): demote repeated H1 headers to H2 (#31385) …

feat(CategoryTheory): some API for transporting monoidal morphism properties (#31345)

feat(AlgebraicTopology): Edge and CompStruct for simplicial sets (#31265) …

feat(Algebra/Homology): sandwich a comm group between two finite comm groups (#31227) …

perf(reassoc, to_app, elementwise): don't pass the same proof to the kernel again (#30650) …

chore: remove some superfluous imports (#31616)

chore(MeasureTheory/MeasurableSpace): golf `measurableSet_generateFrom_singleton_iff` using `grind` (#31273)

chore: rename `private mk` to `of` for some bundled categories (#31622) …

chore: rename FiniteDimensional.of_fintype_basis (#31543) …

feat: Eisenstein q exp identity (#27606) …

chore(Analysis/LocallyConvex): rename a boundedness lemma (#31620) …

chore(Data/PNat): deprecate `gcd_eq_left` (#31606)

chore(Tactic/Translate): rename the `ToAdditive` folder (#31612) …

chore(Combinatorics/SimpleGraph): golf `circulantGraph_eq_symm` using `grind` (#31605)

chore(Data/Set): golf `image_sUnion` using `grind` (#31602)

chore(Data/List): golf `ofFn_eq_pmap` using `ext; grind` (#31598)

feat: totally bounded sets have finite covers (#31537) …

feat: small tweaks to `PointwiseConvergenceCLM` (#31535) …

feat(Geometry/Euclidean/Incenter): `incenter_mem_interior` (#31493) …

chore(Algebra): move `QuadraticAlgebra` to `QuadraticAlgebra/Defs` (#31490) …

feat(Analysis/Convex/Combination): `centerMass_const`, `centerMass_congr` (#31451) …

chore(Order/UnorderedInterval): add basic uIoo lemmas (#31438) …

doc(AlgebraicTopology/SingularSet): fix typos (#31428) …

doc(Archive): ensure only a single H1 header per file (#31384) …

chore(Logic/Equiv): golf entire `Perm.subtypeCongr.symm` using `rfl` (#31237)

feat(Analysis): use new notation for Fourier transform on Schwartz functions and simplify presentation (#31114) …

feat(Geometry/Euclidean/Projection): `orthogonalProjectionSpan_congr` (#31055) …

feat: add differentiation for ContDiffMapSupportedIn (#30201) …

chore: bump toolchain to v4.25.0 (#31619)

feat: drop a finiteness assumptions in covariance results (#31569)

feat(MeasureTheory/Measure): `comap_apply` version for measurable equivs (#31398) …

chore(Finsupp): move `mapRange.equiv` earlier (#31324) …

chore(Control/Fix): remove redundant import (#31614)

chore: add grind annotations for homomorphisms (#29576)

chore(Order): remove redundant instance fields (#30752) …

feat: `to_dual` attribute (#27887) …

feat: ringOfIntegersEquiv_symm_coe (#31300) …

feat(UnitInterval): `x : I` and its symmetric sum to 1 (#31396)

feat: the graph made of all non-diag edges is complete (#31443)

feat: Add Filter.frequently_exists and Filter.frequently_exists_finite (#31527) …

feat(gcongr): use mdata instead of template (#30739) …