feat: MiM PR report

[adomani]

---

[github-actions]

PR summary 7048ffa529

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[github-actions]

January 2026 in Mathlib summary

Commits to mathlib4 between 2026-01-01 and 2026-01-31

Between 2026-01-01 and 2026-01-31 there were

• 471 commits to master and
• 479 closed PRs

PR #33409 Joseph Myers: feat(LinearAlgebra/AffineSpace/Ceva): Ceva's theorem

PR #34076 Thomas Browning: refactor(GroupTheory/CommutingProbability): clean up using `grind`

PR #32886 Junyan Xu: refactor(Algebra/Order): change `MulArchimedeanClass.subgroup` to `FiniteArchimedeanClass.subgroup`
PR #33007 Violeta Hernández Palacios: feat: `stdPart x = sSup {r | r < x}`
PR #33320 Violeta Hernández Palacios: feat(Algebra/Order/SuccPred): simplify n+1 ≤ ... and ... < n+1

PR #33779 Thomas Browning: refactor: generalize `isPrimary_of_isMaximal_radical` to `CommSemiring`
PR #33781 Thomas Browning: feat(Ideal/IsPrimary): `Ideal.isPrimary` preserved by `Ideal.comap`
PR #33804 Thomas Browning: feat(RingTheory/Localization/Ideal): `map` distributes over `inf`
PR #33806 Thomas Browning: feat(RingTheory/Localization/Ideal): generalize `comap_map_of_isPrime_disjoint` to primary ideals
PR #33892 Thomas Browning: feat(Algebra/Module/Submodule/Pointwise): add `smul_iSup'`
PR #33918 Thomas Browning: feat(RingTheory/Ideal/Operations): equality version of `IsPrime.inf_le'`
PR #33919 Thomas Browning: feat(Algebra/Polynomial/Roots): Action of group on `rootSet`
PR #34060 Thomas Browning: feat(RingTheory/Ideal/Colon): add a few API lemmas
PR #34064 Junyan Xu: feat: Orzech property implies stable finiteness

PR #25925 Bolton Bailey: feat: file for lemmas about MvPolynomials over NoZeroDivisors
PR #28411 Zheng Chu: feat(LinearAlgebra/AffineSpace/Simplex/Centroid): define centroid and medians
PR #30563 Yaël Dillies: chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree` wlog
PR #30799 Yaël Dillies: refactor: unify the two versions of `pow_eq_one_iff`
PR #31749 Yaël Dillies: refactor: make `LinearOrderedCommMonoidWithZero`s cancellative
PR #32773 Hagb (Junyu Guo 郭俊余): feat(Algebra/GroupWithZero/NonZeroDivisors): add some lemmas about multiplication
PR #32836 Yaël Dillies: feat(Algebra): characterise when a submodule constructor is equal to `⊥`
PR #32946 Thomas Browning: refactor(Algebra/Polynomial/Factors): Deprecate file
PR #33161 Yuval Filmus: feat(Polynomial/Derivative): iterated derivative of product of linear factors
PR #33185 Junyan Xu: feat(Algebra): MulAction/SMulWithZero by Nat/Int
PR #33186 Ruben Van de Velde: feat: some lemmas about finsum/finprod
PR #33194 Yuval Filmus: feat(LinearAlgebra/Lagrange): refactored proof of leadingCoeff_eq_sum
PR #33216 stepan2698-cpu: feat: Schur's lemma over an algebraically closed field
PR #33271 jano-wol: feat: prove invtSubmoduleToLieIdeal_top
PR #33301 Monica Omar: chore(Algebra/Central/End): generalize `Algebra.IsCentral.instEnd`
PR #33306 Yuval Filmus: feat(Polynomial/Derivative): formulas for iterated derivatives of P * X^m
PR #33353 Oliver Nash: chore: use `IsScalarTower.algebraMap_eq` to golf two proofs
PR #33405 Monica Omar: chore(Algebra): move `LinearMap.mul{Left, Right, LeftRight}` to earlier file
PR #33433 Julien Michel: feat(Algebra): leading coeff of sum of polynomials with same degree is sum of leading coeffs
PR #33436 Zhao Yuyang 赵雨扬: feat: lemmas about `(Add)MonoidAlgebra.mapRangeRingHom`
PR #33446 Harald Husum: doc(Algebra): fix file refs
PR #33453 Yaël Dillies: feat(Algebra/Group/Equiv): `MulEquiv.funUnique`
PR #33492 Yaël Dillies: feat(Algebra/MonoidAlgebra): `R[M][N] ≃+* R[N][M]`
PR #33508 Yury G. Kudryashov: feat(BigOperators/Finprod): add `finsum_cond_pos`
PR #33515 Yury G. Kudryashov: feat(Algebra/Group/Action): add `smul_set_eq_univ`
PR #33544 Yaël Dillies: chore(LinearAlgebra): make one more argument implicit in `ker_toSpanSingleton`
PR #33552 Yaël Dillies: feat: a non-domain cannot act faithfully on a domain
PR #33562 Kim Morrison: feat(ConvexSpace): complete `proof_wanted` statements
PR #33570 Kim Morrison: chore(Algebra/Order): remove unnecessary @[expose] from public sections
PR #33571 Kim Morrison: chore(Algebra/Group): remove unnecessary @[expose] from public sections
PR #33572 Kim Morrison: chore(Algebra): remove unnecessary @[expose] from public sections
PR #33585 Yury G. Kudryashov: feat(LinearAlgebra/Prod): add `range_prodMap`
PR #33590 Oliver Nash: chore: promote `Matrix.det` from an `abbrev` into a `def`
PR #33602 Monica Omar: chore(Algebra): some cleanup
PR #33615 Monica Omar: feat(Algebra/Algebra/Equiv): `f.conj (mulLeft R x) = mulLeft R (f x)`
PR #33620 Harald Husum: doc(Algebra): fix file refs
PR #33638 Yury G. Kudryashov: fix(Finprod): fix a `to_additive` name
PR #33643 Violeta Hernández Palacios: feat: `r < stdPart x → r < x`
PR #33674 euprunin: feat(Algebra/Algebra/Subalgebra): remove unnecessary assumptions in `iSup_induction` and `iSup_induction'`
PR #33698 Artie Khovanov: feat(Algebra/Ring): characteristic of semireal ring
PR #33699 Artie Khovanov: chore(Algebra/Ring): semireal definition lemmas
PR #33719 Thomas Browning: chore(Algebra/Exact): refactor using `to_additive`
PR #33734 euprunin: chore(Algebra/GroupWithZero): deprecate `mul_mem_nonZeroDivisors{Left,Right}_of_mem_nonZeroDivisors{Left,Right}`
PR #33748 Ruben Van de Velde: feat: Matrix.IsSymm.inv
PR #33758 Michael Rothgang: chore: remove superfluous disabling of the whitespace linter
PR #33761 ooovi: feat(Algebra/Module/Submodule): behaviour of `restrictScalars` under lattice operations
PR #33769 Junyan Xu: feat(LinearAlgebra): add `Module.IsPrincipal`
PR #33775 Junyan Xu: chore(Algebra): deduplicate `IsReduced` lemmas
PR #33785 Violeta Hernández Palacios: feat: small lemmas on `ArchimedeanClass`
PR #33794 Sebastian Ullrich: perf(RingTheory/Polynomial/DegreeLT): optimize proof for kernel checking
PR #33796 Jonathan Reich: feat(LinearAlgebra/Matrix/Trace): the trace map is surjective
PR #33828 Monica Omar: chore(Algebra/Group/Center): golf some stuff
PR #33836 EvKitsios: feat: add lemma `le_abs_of_dvd`
PR #33846 Oliver Nash: feat: the rank of the ℤ-span of the roots of a root system is the dimension
PR #33849 Yury G. Kudryashov: refactor(Algebra/ModEq): generalize to monoids
PR #33871 Yaël Dillies: feat(Algebra): more `Module.IsTorsionFree` API
PR #33900 Ruben Van de Velde: fix: generalize TransvectionStruct.det_toMatrix_prod to CommRing
PR #33908 Andrew Yang: perf: set `IsScalarTower.right` to high priority
PR #33934 Thomas Browning: chore(Algebra/Polynomial/Splits): deprecate `Splits.splits` and `splits_iff_splits`
PR #33938 Jovan Gerbscheid: chore(Algebra/Notation/Defs): add missing `to_additive`
PR #33946 Jovan Gerbscheid: chore(Algebra/*/Shrink): use `noncomputable section` with `to_additive`
PR #33951 Violeta Hernández Palacios: chore: remove duplicate instance
PR #34001 Antoine Chambert-Loir: chore(Algebra/BigOperators/GroupWithZero/Action): generalize lemma
PR #34056 Junyan Xu: perf(Algebra): higher priority for `Algebra.to_smulCommClass`
PR #34065 Marcelo Lynch: ci: Fix propagating linting errors
PR #34083 Fengyang Wang: feat(Algebra/Group/Indicator): add Pi. mulIndicator_singleton

PR #32412 Brian Nugent: feat: add Artinian schemes
PR #33472 Andrew Yang: feat(AlgebraicGeometry): properties of `coprod.map` and `coprod.desc`
PR #33476 Andrew Yang: feat(AlgebraicGeometry): universal property of relative normalization
PR #33556 Andrew Yang: feat(AlgebraicGeometry): fpqc descent implies fppf descent
PR #33655 euprunin: feat(AlgebraicGeometry/EllipticCurve/Projective): remove unnecessary assumptions in `WeierstrassCurve.Projective.toAffine_slope_of_eq`
PR #33805 Andrew Yang: feat(AlgebraicGeometry): relative normalization in coproduct
PR #33898 Christian Merten: feat(AlgebraicGeometry): relative gluing
PR #33937 Christian Merten: refactor(AlgebraicGeometry/Cover): make `Scheme.Cover.Hom` an `abbrev` for `ZeroHypercover.Hom`
PR #33982 Andrew Yang: feat(AlgebraicGeometry): being locally artinian is local
PR #34014 Christian Merten: feat(AlgebraicGeometry): `Scheme` has disjoint coproducts

PR #28126 Sebi-Kumar: feat(AlgebraicTopology/FundamentalGroupoid): relate equality in fundamental groupoid to homotopy
PR #31325 Joël Riou: feat(AlgebraicTopology): a computable monoidal functor instance for `hoFunctor`
PR #32266 Joël Riou: feat(AlgebraicTopology): finite simplicial sets are `ℵ₀`-presentable
PR #33447 Yury G. Kudryashov: feat(FundamentalGroupoid): define simply connected sets

PR #32273 Joseph Myers: feat(Analysis/Convex/Side): affine combinations on same / opposite side of face of a simplex as a vertex

PR #30706 Zhao Yuyang 赵雨扬: refactor(Analysis/NormedSpace/Exponential): remove the `𝕂` argument from `exp`
PR #30886 Yury G. Kudryashov: feat(DifferentialForm): exterior derivative applied to vector fields
PR #31988 Winston Yin: feat: uniqueness API for implicit function of `IsContDiffImplicitAt`
PR #32480 Anatole Dedecker: feat: define `PolynormableSpace`
PR #32481 Anatole Dedecker: feat: add `PolynormableSpace.banach_steinhaus`
PR #32770 Moritz Doll: feat(Analysis/TemperedDistribution): derivatives
PR #32841 Terence Prime: feat(Analysis/Normed/Group/Seminorm): define SupSet instances
PR #32911 Andrew Yang: feat(Analysis): ℘ is analytic
PR #32992 Moritz Doll: feat(Analysis/Fourier): Fourier transform of the convolution
PR #33000 David Loeffler: feat(Analysis/Analytic): analytic order of a composition
PR #33116 Gregory C. Wickham: feat(Analysis/CStarAlgebra): GNS construction
PR #33230 Moritz Doll: feat(Analysis/TemperedDistribution): Fourier transform of the dirac delta
PR #33231 Stefan Kebekus: feat: use new predicate `Meromorphic` in Value Distribution Theory
PR #33259 Yuval Filmus: feat(Trigonometric/Chebyshev/Extremal): Chebyshev polynomials are extremal in terms of leading coefficient
PR #33289 Julien Michel: feat(Analysis/SpecialFunctions/Integrals): add `∫ x : ℝ in a..b, (c ^ 2 + x ^ 2)⁻¹`
PR #33352 Monica Omar: feat(Analysis/InnerProductSpace/Positive): `f.symm.IsPositive` iff `f.IsPositive`
PR #33404 Moritz Doll: feat(Analysis/SchwartzSpace): scalar multiplication with linear factors
PR #33415 Moritz Doll: chore(Analysis/SchwartzSpace): explicit variables for `derivCLM` and `fderivCLM`
PR #33423 Yury G. Kudryashov: feat: prove `Complex.arg_exp` etc
PR #33439 Monica Omar: feat(Analysis/InnerProductSpace): define rank-one operators
PR #33451 Harald Husum: doc(Analysis): fix file refs
PR #33455 Yi.Yuan: doc(1000.yaml): Add decls of Prokhorov's theorem, Parseval's theorem
PR #33459 Sebastien Gouezel: feat: FTaylorSeries of the composition with an affine map
PR #33509 Yury G. Kudryashov: feat(CauchyIntegral): add a version of the Cauchy integral theorem
PR #33511 Yury G. Kudryashov: feat(Schwarz): generalize domain
PR #33522 ajirving: feat(Analysis/Asymptotics): Adds Asymptotics.IsEquivalent.Log
PR #33563 Yury G. Kudryashov: feat(Schwarz): add a version for maps with derivative zero
PR #33565 Kim Morrison: chore(Analysis/Calculus): remove unnecessary @[expose] from public sections
PR #33567 Kim Morrison: chore(Analysis/SpecialFunctions): remove unnecessary @[expose] from public sections
PR #33568 Kim Morrison: chore(Analysis/Normed): remove unnecessary @[expose] from public sections
PR #33569 Kim Morrison: chore(Analysis/Complex): remove unnecessary @[expose] from public sections
PR #33582 Yury G. Kudryashov: feat(ContDiffHolder/Moreira): define $C^{k+(α)}$ maps
PR #33597 Moritz Doll: feat(Analysis/Distribution): more lemmas for temperate growth functions
PR #33617 Jireh Loreaux: feat: continuity of common functions involving the continuous functional calculus
PR #33627 Jireh Loreaux: feat: upper hemicontinuity of the spectrum in Banach algebras
PR #33630 Yury G. Kudryashov: feat(UnitDisc): define `Pow 𝔻 ℕ+`
PR #33633 Moritz Doll: chore(Analysis/Fourier): split type class, add continuity one
PR #33637 Monica Omar: feat(Analysis/Matrix/Order): `det (abs A) = |det A|` and `det (sqrt A) = √(det A)`
PR #33639 Yury G. Kudryashov: chore(UnitDisc): review API
PR #33671 Sebastien Gouezel: chore: more `fun_prop` attributes and lemmas
PR #33703 Stefan Kebekus: feat: Upgrade theorem `MeromorphicAt.comp_analyticAt`
PR #33704 Stefan Kebekus: feat: behavior under addition of the characteristic function of Value Distribution Theory
PR #33723 Andrew Yang: feat(Analytic): `℘'(z)² = 4 ℘(z)³ - g₂ ℘(z) - g₃`
PR #33739 Moritz Doll: chore(Analysis/InnerProductSpace): the Laplacian is `k`-linear
PR #33741 Moritz Doll: feat(Analysis/SchwartzSpace): additional lemmas for `smulLeftCLM`
PR #33751 Moritz Doll: feat(Analysis/FourierSchwartz): self-adjointness for the inverse Fourier transform
PR #33752 Moritz Doll: feat(Analysis/FourierSchwartz): the derivative of the Fourier transform
PR #33763 Salvatore Mercuri: doc: add note in `Asymptotics` docstring about the existential pattern
PR #33855 Monica Omar: feat(Analysis/RCLike): square root on `RCLike`
PR #33858 Moritz Doll: feat(Analysis/Fourier): the convolution on Schwartz functions
PR #33859 Moritz Doll: feat(Analysis/TemperedDistribution): coercion of multiplication of `Lp` functions
PR #33869 Anatole Dedecker: chore(Asymptotics/Lemmas): weaken Normed -> Seminormed
PR #33889 Stefan Kebekus: feat: establish function properties of the Nevanlinna functions
PR #33940 Yongxi (Aaron) Lin: doc: correct a statement in the file of Poisson's summation formula
PR #33943 Yury G. Kudryashov: feat(Asymptotics/TVS): add more lemmas
PR #34047 Michael Rothgang: chore: deprecate Analysis/Normed/Order/Basic

PR #31707 Nailin Guan: feat(Homology): map between `Ext` induced by exact functor
PR #33652 Violeta Hernández Palacios: fix: `zsmul` lemmas that were about `nsmul` instead

PR #30373 Sina Hazratpour: feat(CategoryTheory): LCCC sections (constructing right adjoint to `Over.ChosenPullback.pullback`)
PR #31332 Sina Hazratpour: feat(CategoryTheory): Exponentiable morphisms
PR #32816 Joël Riou: feat(CategoryTheory): computing Ext-groups using a projective resolution
PR #33045 Christian Merten: feat(CategoryTheory/MorphismProperty): `ind P` is stable under composition if `P` is
PR #33084 Joël Riou: feat(CategoryTheory): MorphismProperty induced on a quotient category
PR #33113 Sina Hazratpour: feat(Category Theory): A natural isomorphism connecting Over.iteratedSlice and Over.map
PR #33179 Joël Riou: feat(CategoryTheory/Sites): relation between `IsPrestack` and the full faithfulness of `toDescentData`
PR #33195 Joël Riou: feat(CategoryTheory/Sites): stacks
PR #33237 Jovan Gerbscheid: feat(CategoryTheory/Functor): use `@[to_dual]`
PR #33358 Joël Riou: feat(Algebra/Homology): functoriality of `ProjectiveResolution.extMk`
PR #33360 Joël Riou: feat(Algebra/Homology): functoriality of `extMk` with respect to the injective resolution
PR #33412 Robin Carlier: chore(CategoryTheory/Pi/Monoidal): monoidal `Functor.pi` and `Functor.pi'`
PR #33457 Sina Hazratpour: doc(CategoryTheory): a doc-string fix
PR #33471 euprunin: chore(CategoryTheory): golf proofs
PR #33531 Harald Husum: doc(CategoryTheory): fix typos
PR #33536 Andrew Yang: feat(CategoryTheory): lifting colimit cocone to `Over`
PR #33537 Andrew Yang: feat(CategoryTheory): `FinCategory` instance on `Pairwise`
PR #33577 Kim Morrison: chore(CategoryTheory): remove unnecessary @[expose] from public sections
PR #33730 Harald Husum: chore(CategoryTheory): fix whitespace
PR #33820 Robin Carlier: feat(CategoryTheory): use `push` attribute for `CategoryTheory.inv`.
PR #33834 Jovan Gerbscheid: feat(CategoryTheory/NatTrans): use to_dual
PR #33848 Robin Carlier: perf(CategoryTheory/Limits/Pullback/Categorical/Basic): abstract `CatCommSqOver`
PR #33867 Robin Carlier: perf(CategoryTheory/Monoidal/Closed/FunctorCategory/Groupoid): remove universe mvars
PR #33877 Joël Riou: feat(CategoryTheory/Category/Preorder): isIso_homOfLE
PR #33879 Joël Riou: feat(CategoryTheory/ComposableArrows): isIso_iff
PR #33883 Joël Riou: feat(CategoryTheory/ObjectProperty): various additions
PR #33886 Joël Riou: feat(CategoryTheory/Triangulated): functors to `Triangle`
PR #33888 Joël Riou: feat(CategoryTheory/Shift): more API for NatTrans.CommShift
PR #33931 Christian Merten: chore(CategoryTheory/MorphismProperty): improve def-eqs and add missing `MorphismProperty.Over.map` isomorphisms
PR #33932 Christian Merten: chore(CategoryTheory/MorphismProperty): add trivial instances for `HasOfPostcompProperty`, etc.
PR #33933 Christian Merten: feat(CategoryTheory/Limits/MorphismProperty): `MorphismProperty.Over.pullback` preserves finite limits
PR #33945 Jovan Gerbscheid: chore(CategoryTheory/Iso): address FIXME
PR #33957 Christian Merten: feat(CategoryTheory/MorphismProperty): add `P.CostructuredArrow Q F X`
PR #33968 blizzard_inc: chore(CategoryTheory/Limits/Shapes/Pullback): Split `CommSq`
PR #34009 Christian Merten: feat(CategoryTheory/Sites): API for hypercovers in subcanonical topologies

PR #30129 Vlad Tsyrklevich: feat(SimpleGraph): define and prove basic theory of vertex covers
PR #32043 thomaskwaring: feat(Combinatorics/SimpleGraph/Acyclic): characterise maximal acyclic subgraphs
PR #32238 Yaël Dillies: feat(Combinatorics/SimpleGraph): distributivity of box product over sum
PR #32702 SnirBroshi: chore(Combinatorics/SimpleGraph/Connectivity): move `Finite ConnectedComponent` instance from `WalkCounting.lean` to `Connected.lean`
PR #33523 Joseph Myers: feat(Combinatorics/Tiling/Tile): tiles and protosets for tilings
PR #33622 Vlad Tsyrklevich: refactor(Combinatorics/SimpleGraph/VertexCover): assumes containment instead of injective hom
PR #33673 SnirBroshi: chore(Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity): rename `.rfl` to `.refl`
PR #33798 Paul Lezeau: feat(Combinatorics/SimpleGraph/Basic): decidability instance for `fromRel.Adj`
PR #33856 Julian Berman: feat(GraphTheory): supports of top and bot graphs
PR #33865 Miyahara Kō: doc: capitalization
PR #34085 Iván Renison: feat(Combinatorics/SimpleGraph/Diam): add lemma `eccent_eq_one_iff`

PR #33835 Bolton Bailey: chore(Computability/Primrec): split file

PR #31579 Xavier Roblot: feat(Data/Nat/Digits): prove the bijection induced by `Nat.ofDigits` and use it to compute the sum of the sum of digits
PR #31637 Whysoserioushah: feat(Data/Matrix/Basis): add some lemmas
PR #32772 Thomas Browning: feat(Data/Set/Card): criterion for `s.ncard ≤ (f '' s).ncard + 1`
PR #32940 Jovan Gerbscheid: perf(to_fun): remove `ofNat(n)` in `Pi.ofNat_def`
PR #33074 euprunin: chore: golf using `grind`
PR #33115 Jonathan Reich: feat(Data/Matrix/Cartan): determinants and simply-laced properties
PR #33193 Yuval Filmus: feat(Powerset): Results related to image
PR #33339 Ruben Van de Velde: feat: small lemmas about LeftInverse and image/preimage
PR #33465 SnirBroshi: chore(Data/Finset/Insert): golf `eq_singleton_iff_nonempty_unique_mem` using grind
PR #33480 euprunin: chore(Data): golf proofs
PR #33521 Yaël Dillies: chore(Data/Finsupp): rename `finsuppProdEquiv` to `curryEquiv`
PR #33530 Violeta Hernández Palacios: feat: range of `Finsupp` is finite
PR #33538 Jonathan Reich: feat(Data/Matrix/Cartan): non-simply-laced theorems for F and G
PR #33547 Eric Wieser: feat: lemmas about `Matrix.single` and `diagonal` and `submatrix`
PR #33574 Kim Morrison: chore(Data): remove unnecessary @[expose] from public sections
PR #33653 Violeta Hernández Palacios: chore: deprecate duplicate results about `zsmul`
PR #33812 Yury G. Kudryashov: feat: define `List.offDiag`
PR #33902 Ruben Van de Velde: chore: golf Real.exists_floor
PR #33910 Yaël Dillies: feat(Data/List): `a :: l ~r l ++ [a]`
PR #33913 Yaël Dillies: feat(Data/Set/Pairwise): the `{f i}` are pairwise disjoint iff `f` is injective
PR #34004 Bhavik Mehta: feat(Data/Finset/Union): two easy lemmas relating union and biUnion

PR #33830 Seewoo Lee: feat(Manifold/MFDeriv): `MDifferentiable.pow` and variants
PR #33896 David Loeffler: refactor(Geometry/Manifold): split long file ChartedSpace.lean
PR #33923 Michael Rothgang: fix: example of GL(V) being a Lie group

PR #32676 Li Jiale: doc(Sphere.Power): add theorem to 1000.yaml and author credit
PR #33365 Zheng Chu: feat(Geometry/Euclidean/Angle/Oriented/Affine): Add oangle sign lemmas for two intersecting lines
PR #33383 wangying11123: feat(Geometry/Euclidean/Angle/Unoriented/Affine): Add Theorem about Sbtw.angle_eq and Wbtw.angle_eq
PR #33588 Jovan Gerbscheid: chore(Geometry/Euclidean/SignedDist): remove `privateInPublic`
PR #33861 Joseph Myers: feat(Geometry/Euclidean/SignedDist): `lineMap` lemmas

PR #32152 Lingyin Luo: feat(GroupTheory/SpecificGroups/Cyclic): generalize the proof of prime_card by not assuming Finite
PR #33483 Li Xuanji: chore: Fix Dihedral comments
PR #33823 SnirBroshi: chore(GroupTheory/GroupAction/Defs): golf `orbitRel.iseqv`

PR #33708 Michael Rothgang: chore: rename the `commandStart` linter to `whitespace`
PR #33827 Thomas R. Murrills: fix: restore `#lint` via Mathlib.Init
PR #33914 Anne Baanen: fix(Tactic/Linter): support Verso docstrings in header style linter

PR #26332 Alex Meiburg: feat(ModelTheory/Definability): TermDefinable functions
PR #33839 qawbecrdtey: chore(ModelTheory/Basic): fix comments

PR #30344 Louis Liu: feat(MeasureTheory/Integral): mean value theorem for integrals and average existence lemmas
PR #31444 Harald Husum: doc(Probability/Martingale/BorelCantelli): fix LaTeX typo
PR #31960 Yury G. Kudryashov: feat: a lower bound for the volume of a cone on the unit sphere
PR #32163 Yizheng Zhu: feat(MeasureTheory): interval integral is absolutely continuous
PR #32882 DavidLedvinka: feat(Probability): add `Adapted `
PR #33063 DavidLedvinka: chore(Probability): Rename Adapted to StronglyAdapted
PR #33278 Harald Husum: doc(MeasureTheory): remove stale paragraph
PR #33371 Kexing Ying: feat(Probability): Right continuous filtrations
PR #33513 Yury G. Kudryashov: feat(CircleIntegral): integral of a finite sum of functions
PR #33576 Kim Morrison: chore(MeasureTheory): remove unnecessary @[expose] from public sections
PR #33659 David Loeffler: feat(MeasureTheory/Group/Action): weaken MeasurableSMul to MeasurableConstSMul
PR #33670 Sebastien Gouezel: feat: more API for ae strongly measurable functions on compact sets
PR #33679 DavidLedvinka: feat(MeasureTheory): add formulas for the measures formed by a density with respect to counting or dirac measures.
PR #33710 David Loeffler: feat(MeasureTheory): more MeasurableSMul -> MeasurableConstSMul
PR #33725 Yuma Mizuno: chore(MeasureTheory): remove redundant `by_cases`
PR #33776 Moritz Doll: feat(MeasureTheory): every bounded continuous function is in `L∞`
PR #34030 Lua Viana Reis: feat(Integral/Bochnet/Set): add setIntegral_compl₀

PR #32795 Floris van Doorn: fix: restrict abv positivity extension to variable functions

PR #33711 Anne Baanen: chore(AlgebraicGeometry/ProjectiveSpectrum): delete unused code

PR #31133 Thomas R. Murrills: feat(Linter): combinators for linter option boilerplate

PR #25889 Aaron Liu: fix(Tactic/Widget/Conv): fix various issues
PR #32734 Anne Baanen: chore(Tactic): document remaining undocumented tactics
PR #32939 Jovan Gerbscheid: fix(to_additive): don't translate into non-existent names
PR #32956 damiano: fix: `simp_rw` does not hide goals
PR #33497 Jovan Gerbscheid: feat(to_dual): `to_dual none` to have the dual as an implementation detail
PR #33498 Jovan Gerbscheid: perf(translate): only run `check` after kernel check fails
PR #33500 Jovan Gerbscheid: doc(translate): improve discoverability of trace options
PR #33584 Kim Morrison: fix(Tactic/TacticAnalysis): analyze tactics inside `have ... := by ...`
PR #33589 Jovan Gerbscheid: chore(Lean/Meta/RefinedDiscrTree/Basic): remove `privateInPublic`
PR #33603 Jovan Gerbscheid: fix(translate): don't unfold aux lemmas, but translate them
PR #33632 Aaron Liu: fix(Tactic/WLOG): handle unused let variables
PR #33635 Aaron Liu: feat(Tactic/Set): use `binderIdent` instead of `ident`
PR #33666 Jovan Gerbscheid: chore(Tactic): remove duplicate instances
PR #33686 Aaron Liu: fix(Tactic/DepRewrite): unknown free variable on `rw!` at local hypothesis
PR #33701 Jovan Gerbscheid: chore(Tactic/Translate/ToDual): fix typo in `nameDict`
PR #33773 Jovan Gerbscheid: fix(to_dual none): don't allow attributes in `to_dual none`
PR #33994 Anne Baanen: doc(Tactic): improve `wlog` tactic docstring
PR #33995 Anne Baanen: doc(Tactic): improve `push`/`push_neg`/`pull`/`pull_neg` tactic docstring
PR #33996 Anne Baanen: doc(Tactic): improve `ring`/`ring1`/`ring_nf` tactic docstring
PR #33998 Anne Baanen: doc(Tactic): improve `fun_prop` tactic docstring

PR #33054 Michael Stoll: feat(NumberTheory/Height/Basic): first installment of heights
PR #33124 Riccardo Brasca: feat(RepresentationTheory/Homological/GroupCohomology/Hilbert90): add Hilbert 90 for cyclic groups
PR #33484 Salvatore Mercuri: feat: generalise `Ideal.absNorm_eq_pow_inertiaDeg`
PR #33524 Li Xuanji: fix: Rename constructors in Irrational.lean docstrings

PR #30378 Christopher Hoskin: refactor(Order/Hom/Lattice): Use default `initialize_simps_projections` configuration for `LatticeHom`.
PR #33211 Miyahara Kō: doc(Order/Filter/*): outdated documents
PR #33325 SnirBroshi: chore(Order/Defs/Unbundled): deprecate `IsSymm` in favor of core's `Std.Symm`
PR #33663 Yan Yablonovskiy: feat(Order): `OrderIso` involving `Prod` and `Lex`
PR #33685 SnirBroshi: chore(Order/Defs/Unbundled): deprecate `IsAntisymm` in favor of core's `Std.Antisymm`
PR #33717 SnirBroshi: chore(Order/Defs/Unbundled): deprecate `IsIrrefl` in favor of core's `Std.Irrefl`
PR #33755 SnirBroshi: chore(Order/Defs/Unbundled): deprecate `IsRefl` in favor of core's `Std.Refl`
PR #33760 Jovan Gerbscheid: feat(Order/Bounds/Basic): use `to_dual` - part 1
PR #33771 Aaron Liu: feat: prove `Prod.wellFoundedLT` directly
PR #33952 Violeta Hernández Palacios: chore(Order/FixedPoints): use `where` notation
PR #33953 Violeta Hernández Palacios: feat: IncompRel.ne
PR #34032 Bhavik Mehta: feat(Order/Filter/Extr): local minimum and local maximum implies const

PR #26483 metakunt: feat(RingTheory/RootsOfUnity/PrimitiveRoots): add primitiveRootsPowEquivOfCoprime
PR #27542 Christian Merten: feat(RingTheory/KrullDimension): dimension of polynomial ring
PR #27706 Xavier Roblot: feat(RingTheory/Localization/AtPrime): inertia degree and ramification index are preserved by localization
PR #30736 Junyan Xu: feat(RingTheory): Picard group of a domain is isomorphic to ClassGroup
PR #32027 Junyan Xu: feat(Counterexamples): invertible module not isomorphic to any ideal
PR #32643 Violeta Hernández Palacios: feat: cardinality of Hahn series inverse
PR #32665 Andrew Yang: feat(RingTheory): quasi-finite algebras
PR #32806 Andrew Yang: feat(RingTheory): base change of ideal with flat quotients
PR #32811 Andrew Yang: feat(RingTheory): predicate on satisfying Zariski's main theorem
PR #32823 Andrew Yang: feat(RingTheory): construct etale neighborhood that isolates point in fiber
PR #32837 Andrew Yang: feat(RingTheory): noetherian model for etale algebras
PR #32988 Whysoserioushah: feat(RingTheory/Morita/Matrix): more on morita equivalence between `R` and `Mn(R)`
PR #33040 Violeta Hernández Palacios: refactor: rename `≤ᵥ` to `vle` and `<ᵥ` to `vlt`
PR #33091 Wenrong Zou: feat(RingTheory/MvPowerSeries): (mv) PowerSeries version of `expand_char`
PR #33284 Harald Husum: doc(RingTheory): fix file refs
PR #33311 Yuval Filmus: feat(Polynomial/Chebyshev): calculate values of T and U at zero
PR #33324 Fabrizio Barroero: feat(RingTheory/DedekindDomain/AdicValuation): introduce `intAdicAbv`
PR #33326 Fabrizio Barroero: feat(RingTheory/DedekindDomain/GaussLemma): Gauss's Lemma for Dedekind Domains
PR #33361 sun123zxy: feat(RingTheory/Nakayama): refine Nakayama's lemma 00DV (8)
PR #33390 Blake Farman: feat(RingTheory/Ideal): generalize Submodule.colon to sets
PR #33398 Violeta Hernández Palacios: feat: `IsStrictOrderedRing (Lex R⟦Γ⟧)`
PR #33452 Yaël Dillies: chore(RingTheory/Bialgebra/MonoidAlgebra): use `to_additive`
PR #33473 Anirudh Vegesana: feat(RingTheory/Nilpotent/Exp): add isNilpotent_exp_sub_one
PR #33482 Yaël Dillies: feat(RingTheory/TensorProduct/MonoidAlgebra): additivise
PR #33488 Xavier Généreux: feat(Valuation/Basic): adjust Valuation.IsNontrivial lemmas for fields
PR #33489 Xavier Généreux: feat: simp lemmas PrimeSpectrum.asIdeal_bot/top
PR #33540 Yaël Dillies: feat(RingTheory): no extension is algebraic over the zero ring
PR #33553 Andrew Yang: feat(RingTheory): some base changes commute with integral closure
PR #33573 Kim Morrison: chore(RingTheory): remove unnecessary @[expose] from public sections
PR #33609 Xavier Généreux: refactor: Ideal.bot_prime as an instance
PR #33610 Xavier Généreux: feat(ValuationSubring): toSubring_top
PR #33614 Eric Wieser: chore: tidy results around `Module.Finite`
PR #33658 Violeta Hernández Palacios: refactor(RingTheory/Valuation/ValuativeRel/Basic): fix theorem names for multiplication
PR #33660 Violeta Hernández Palacios: chore(RingTheory/MvPowerSeries/Order): deprecate duplicate theorem
PR #33722 Andrew Yang: feat(RingTheory): Add `RingHom.QuasiFinite`
PR #33729 Harald Husum: chore(RingTheory): fix whitespace
PR #33770 Eric Wieser: chore(RingTheory/Morita/Matrix): remove uses of `default`
PR #33872 Wenrong Zou: feat(RingTheory/MvPowerSeries): some inequalities related to order
PR #33885 Wenrong Zou: feat(RingTheory/MvPowerSeries): some theorems about expand
PR #33906 Junyan Xu: feat(RingTheory/SimpleModule): Jacobson density theorem

PR #33298 Violeta Hernández Palacios: chore: mark `Ordinal.enumOrd` with `no_expose`
PR #33319 Violeta Hernández Palacios: refactor(SetTheory/Ordinal/Arithmetic): deprecate `boundedLimitRecOn`

PR #33837 Miyahara Kō: feat: `Tendsto (√·) atTop atTop`

PR #27261 Sebi-Kumar: feat(Topology): add definition for subpaths
PR #32660 Dagur Asgeirsson: feat(Topology): sandwich lemmas for profinite sets
PR #32674 Yongxi (Aaron) Lin: feat: a dense Gdelta subset of a Baire space is Baire.
PR #32764 Aaron Liu: feat(Topology/Separation): completely normal iff hereditarily normal
PR #33114 Yury G. Kudryashov: feat: define `Metric.Snowflaking`
PR #33128 Attila Gáspár: feat(Topology/UniformSpace): generalize `TotallyBounded` to filters
PR #33300 Yongxi (Aaron) Lin: feat: a finite space is Baire.
PR #33308 Lara Toledano: feat(Topology.GDelta.Basic): add helpers for IsMeagre
PR #33341 Monica Omar: chore(Topology/Algebra/Module/LinearMap): deprecate duplicate lemmas
PR #33374 Kexing Ying: feat: Simple lemmas about convergence in WithTop
PR #33414 Tian Chen: feat(Topology/Separation/NotNormal): generalize to non-separable spaces
PR #33422 Yury G. Kudryashov: feat(Homotopy/Lifting): add a lemma about `IsCoveringMapOn`
PR #33486 Attila Gáspár: chore(Topology/Order): generalize `IsCountablyGenerated atTop` instance to `SeparableSpace`
PR #33510 Yury G. Kudryashov: feat(Topology/Algebra/Module/Equiv): add 2 lemmas
PR #33512 Yury G. Kudryashov: feat(MetricSpace): add `eventually_ball_subset`
PR #33517 Yury G. Kudryashov: feat(MetricSpace/Algebra): prove uniform continuity of `(· • ·)`
PR #33525 Yury G. Kudryashov: feat(AddCircle/Defs): prove continuity of `toIocDiv` etc
PR #33564 Junyan Xu: feat(Analysis/Complex): exp is covering map
PR #33575 Kim Morrison: chore(Topology): remove unnecessary @[expose] from public sections
PR #33623 Jireh Loreaux: feat: add simp lemma `nhdsSet_eq_bot_iff`
PR #33624 Jireh Loreaux: feat: add `forall_is{Open,Closed}_iff`
PR #33625 Jireh Loreaux: feat: filter bases for `nhdsSet` of a compact set in locally compact (regular) spaces
PR #33626 Jireh Loreaux: feat: more API for upper hemicontinuous functions
PR #33678 Attila Gáspár: feat(Topology/Inseparable): condition for the compactness of a subset
PR #33682 Attila Gáspár: chore(Topology/Order/Lattice): tag continuity lemmas with `fun_prop`
PR #33720 Junyan Xu: feat(Topology): trivial lemmas
PR #33721 Junyan Xu: chore(Topology/Covering): adjust some statements
PR #33728 Harald Husum: chore(Topology): fix whitespace
PR #33750 Eric Wieser: fix: generalize ContinuousLinearMap.map_add₂ and friends
PR #33787 Lara Toledano: doc(Topology/Baire/BaireMeasurable): add naming convention for notation `residualEq`
PR #33824 Miyahara Kō: doc: update the doc of Bolzano-Weierstrass
PR #33920 Citronhat: feat(Topology): generalize tendsto_inv_iff from ℝ≥0∞ to ContinuousInv + InvolutiveInv
PR #33925 Harald Husum: doc(Topology): fix typos
PR #33959 Attila Gáspár: doc: fix typo
PR #33970 Floris van Doorn: doc: fix discrete_iff_cyclic
PR #34071 Bryan Wang Peng Jun: feat: ContinuousMonoidHom.toMonoidHom_injective

PR #29241 Yoh Tanimoto: feat(Analysis/InnerProductSpace/Orthogonal): add duplicates for `ClosedSubmodule`
PR #30881 Jasin: feat(RingTheory/PowerSeries/Schroder): Define the generating function for large Schroder number
PR #31220 François G. Dorais: chore: adaptations for batteries#1489
PR #31315 Jeremy Tan Jie Rui: feat: IMO 2010 Q5
PR #31653 Stefano Rocca: feat(MeasureTheory): Foelner filters
PR #31794 Thomas R. Murrills: feat: `unusedFintypeInType` linter
PR #31795 Thomas R. Murrills: feat: turn on `unusedFintypeInType` linter
PR #32648 Violeta Hernández Palacios: feat: subfield of Hahn series bounded by a cardinal
PR #32731 Sebastian Ullrich: chore: run the new `shake` tool
PR #32735 Joseph Hua: refactor: move `CategoryTheory.Category.Grpd` to `CategoryTheory.Groupoid.Grpd.Basic`
PR #32740 Lara Toledano: feat: add IsNowhereDense helpers
PR #32812 Harald Husum: doc(Geometry): fix typos
PR #33060 Xavier Généreux: feat: nontrivial instances for valuation with `ℤᵐ⁰` as codomain
PR #33061 edwin1729: refactor: generalise compact from CompleteLattice to PartialOrder
PR #33239 Jovan Gerbscheid: feat(to_dual): linter for redundant uses of `to_dual`/`to_additive`
PR #33290 euprunin: chore: golf using `grind` and `simp`
PR #33312 Yuval Filmus: feat(Polynomial/Chebyshev): formulas for iterated derivatives of T and U at 1
PR #33424 Bryan Gin-ge Chen: ci: run check-lean4checker on self-hosted runner
PR #33429 Jeremy Tan Jie Rui: chore: remove June 2025 deprecated declarations
PR #33442 Yury G. Kudryashov: feat(ToIntervalMod): add missing lemmas
PR #33445 Yury G. Kudryashov: feat(FundamentalGroupoid/InducedMaps): generalize to different universes
PR #33456 null: chore(deps): bump the actions-version-updates group across 2 directories with 6 updates
PR #33460 Sebastien Gouezel: chore: use a generic neighborhood instead of balls in theorems on parametric integrals
PR #33468 Andrew Yang: feat(RingTheory): polynomial is integral <-> coeffs are integral
PR #33474 Bryan Gin-ge Chen: ci: add tracing option to linting steps
PR #33503 SnirBroshi: chore(Order/Defs/Unbundled): deprecate `IsAsymm` in favor of core's `Std.Asymm`
PR #33516 Yaël Dillies: chore(Algebra/MonoidAlgebra/Basic): rename variables
PR #33528 mathlib4-update-dependencies-bot: chore: update Mathlib dependencies 2026-01-03
PR #33533 Rida Hamadani: doc(README): linter -> linters
PR #33534 mathlib4-update-dependencies-bot: chore: update Mathlib dependencies 2026-01-04
PR #33541 euprunin: chore: golf proofs
PR #33545 Jovan Gerbscheid: feat: rename `HasCompl` to `Compl`
PR #33546 Kim Morrison: fix(CI): prevent empty grep pattern from matching all lean-pr-testing branches
PR #33549 euprunin: chore: golf proofs
PR #33550 euprunin: chore: golf proofs
PR #33558 Yury G. Kudryashov: refactor(EMetricSpace): rename `EMetric.diam` -> `Metric.ediam`
PR #33559 euprunin: chore: golf proofs
PR #33566 mathlib4-update-dependencies-bot: chore: update Mathlib dependencies 2026-01-05
PR #33578 Kim Morrison: chore(NumberTheory): remove unnecessary @[expose] from public sections
PR #33579 Kim Morrison: chore(LinearAlgebra,Order): remove unnecessary @[expose] from public sections
PR #33580 Kim Morrison: chore(Probability,Geometry): remove unnecessary @[expose] from public sections
PR #33581 Kim Morrison: chore: remove unnecessary @[expose] from public sections
PR #33583 Kim Morrison: chore(Data/Option): deprecate `Option.iget`
PR #33591 Jovan Gerbscheid: chore: fix some `privateInPublic` proofs
PR #33593 Jovan Gerbscheid: chore(positivity): make tactic lemmas public
PR #33594 Salvatore Mercuri: feat: `HeightOneSpectrum.valuation` is rank one for number fields
PR #33596 euprunin: chore: golf proofs
PR #33598 Bryan Gin-ge Chen: ci: revert changes to wrapper script in #33474
PR #33600 euprunin: chore: golf proofs
PR #33605 Mac Malone: feat(Cache): environment-configurable URLs
PR #33616 euprunin: chore: golf proofs
PR #33628 Jireh Loreaux: feat: convenience lemmas for continuity of the continuous functional calculus in the operator variable
PR #33629 Harald Husum: chore: fix whitespace
PR #33646 Bryan Gin-ge Chen: ci: do not wrap linting step with log parsing script
PR #33647 Kim Morrison: chore(Cache): add README and rename USE_FRO_CACHE to MATHLIB_CACHE_USE_CLOUDFLARE
PR #33648 Kim Morrison: ci: add nanoda verification to daily workflow
PR #33651 Mac Malone: fix(Cache): print ProofWidgets build stdout on error
PR #33667 Jovan Gerbscheid: chore: remove some duplicate instances
PR #33681 François G. Dorais: chore: adaptations for batteries#1588
PR #33687 Ruben Van de Velde: chore: tidy various files
PR #33693 Yoh Tanimoto: feat(Mathlib/Analysis/Normed/Module): add instances of `CompleteSpace` for `Submodules` and `ClosedSubmodule`
PR #33694 Bryan Gin-ge Chen: ci(daily.yml): remove continue-on-error from check steps
PR #33695 mathlib4-update-dependencies-bot: chore: update Mathlib dependencies 2026-01-07
PR #33696 Kim Morrison: fix(ci): show helpful message when runLinter needs master merge
PR #33705 Michael Rothgang: chore: fix more spacing issues
PR #33706 Michael Rothgang: chore: fix more spacing issues
PR #33713 Johan Commelin: ci: add commit verification for transient commits
PR #33716 Michael Rothgang: chore: fix even more spacing issues
PR #33732 Harald Husum: style(misc): fix whitespace
PR #33733 mathlib4-update-dependencies-bot: chore: update Mathlib dependencies 2026-01-07
PR #33735 Mac Malone: fix(Cache): option order in usage & error messages
PR #33738 Bryan Gin-ge Chen: ci(daily.yml): get job status from API instead of via needs context
PR #33742 mathlib4-update-dependencies-bot: chore: update Mathlib dependencies 2026-01-08
PR #33743 Johan Commelin: ci: add automated commit verification
PR #33745 euprunin: chore: golf proofs
PR #33747 Harald Husum: chore: fix whitespace
PR #33754 euprunin: chore: golf proofs
PR #33759 Michael Rothgang: chore(Archive,Counterexamples): fix whitespace
PR #33762 Garmelon: chore: add radar benchmark suite
PR #33772 Yury G. Kudryashov: chore(*): rename `EMetric.infEdist` -> `Metric.infEDist` etc
PR #33777 Jovan Gerbscheid: feat(translate): linter for overwriting existing translations
PR #33783 Bryan Gin-ge Chen: ci: wrap linting with stdbuf -oL so log output appears immediately
PR #33789 Michael Rothgang: chore: annotate manual alignment
PR #33800 Bryan Gin-ge Chen: ci(lint_and_suggest.yml): rename job
PR #33816 Michael Rothgang: style: whitespace fixes
PR #33829 leanprover-community-bot-assistant: chore(scripts): update nolints.json
PR #33841 Sebastian Ullrich: ci(daily.yml): use upstreamed `leanchecker`
PR #33857 euprunin: chore: golf and reduce compilation time
PR #33868 Anne Baanen: chore: remove outdated `library_note2` usage
PR #33899 Michael Rothgang: style: fix whitespace
PR #33912 euprunin: chore: golf using `grind`, reduce compilation time and imports
PR #33922 Bryan Gin-ge Chen: ci: set timeout-minutes to 30 on flaky linting step
PR #33976 Michael Rothgang: chore: annotate locations using manual alignment
PR #33977 Michael Rothgang: style: fix whitespace
PR #33978 Michael Rothgang: style: be consistent about inserting spaces after { or before }
PR #33987 Jakub Nowak: doc(Tactic/Lift): Mention `norm_cast` in documentation of `lift`
PR #33988 leanprover-community-bot-assistant: chore: remove declarations deprecated between 2021-01-15 and 2025-07-15
PR #33999 Michael Rothgang: style: make fun_prop tests match the mathlib style guide better
PR #34003 Yury G. Kudryashov: chore(Algebra/ModEq): split file
PR #34011 Marcelo Lynch: ci: detect and kill stray runLinter processes before linting
PR #34021 damiano: chore: remove self-cancelling pairs
PR #34023 Jovan Gerbscheid: feat: `push` for `Set` membership
PR #34037 Yuval Filmus: doc(Chebyshev): update TODO
PR #34051 damiano: chore: more cancelling pairs
PR #34059 Marcelo Lynch: ci: Retry logic for linting step
PR #34087 Ruben Van de Velde: fix: add missing deprecations
PR #34089 leanprover-community-bot-assistant: chore(scripts): update nolints.json

* PRs not corresponding to a commit (merged before 2026-01-01, closed on 2026-01-01?)
  #31220
  #33352
  #33415
  #33429
  #33452
  #33453
  #33456
  #33457

* All commits are accounted for!

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[joneugster]

Mathlib has moved to PRs from forks. This PR is still from a branch of the main repository and will soon be closed! Please migrate the content to a fork and reopen a PR from there if you wish to do so. See Zulip topic for more instructions. Thank you for contributing to mathlib!

[mathlib-bors]

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.