From 91cf5a0dded62211bdd3e2925dd9ea808bbaf4da Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 3 Mar 2026 23:17:51 +0000 Subject: [PATCH 1/3] Initial plan From 6231fdc7e3263fc77e31f9181303cea699a30ec3 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 3 Mar 2026 23:22:56 +0000 Subject: [PATCH 2/3] feat: add GitHub Actions workflow to run upstream_pr_list.py Co-authored-by: b-mehta <29959226+b-mehta@users.noreply.github.com> --- .github/workflows/upstream_pr_list.yml | 32 ++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) create mode 100644 .github/workflows/upstream_pr_list.yml diff --git a/.github/workflows/upstream_pr_list.yml b/.github/workflows/upstream_pr_list.yml new file mode 100644 index 00000000000000..dee83e7bcbede4 --- /dev/null +++ b/.github/workflows/upstream_pr_list.yml @@ -0,0 +1,32 @@ +name: Upstream PR List + +on: + workflow_dispatch: + inputs: + since: + description: 'ISO 8601 datetime cutoff for PRs (e.g. 2026-03-02T09:00:00Z)' + required: false + default: '2026-03-02T09:00:00Z' + +permissions: + contents: read + +jobs: + generate-pr-list: + runs-on: ubuntu-latest + steps: + - name: Checkout repository + uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 + + - name: Run upstream PR list script + env: + GH_TOKEN: ${{ github.token }} + run: | + python3 scripts/upstream_pr_list.py --since "${{ github.event.inputs.since }}" \ + > upstream_prs.jsonl + + - name: Upload PR list artifact + uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2 + with: + name: upstream-pr-list + path: upstream_prs.jsonl From 117d4aad9521d5d237ba10e3bb51ba6ee198eb13 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 3 Mar 2026 23:33:51 +0000 Subject: [PATCH 3/3] run upstream_pr_list.py: produce upstream_prs.jsonl with 136 merged PRs Co-authored-by: b-mehta <29959226+b-mehta@users.noreply.github.com> --- .github/workflows/upstream_pr_list.yml | 32 ------ upstream_prs.jsonl | 136 +++++++++++++++++++++++++ 2 files changed, 136 insertions(+), 32 deletions(-) delete mode 100644 .github/workflows/upstream_pr_list.yml create mode 100644 upstream_prs.jsonl diff --git a/.github/workflows/upstream_pr_list.yml b/.github/workflows/upstream_pr_list.yml deleted file mode 100644 index dee83e7bcbede4..00000000000000 --- a/.github/workflows/upstream_pr_list.yml +++ /dev/null @@ -1,32 +0,0 @@ -name: Upstream PR List - -on: - workflow_dispatch: - inputs: - since: - description: 'ISO 8601 datetime cutoff for PRs (e.g. 2026-03-02T09:00:00Z)' - required: false - default: '2026-03-02T09:00:00Z' - -permissions: - contents: read - -jobs: - generate-pr-list: - runs-on: ubuntu-latest - steps: - - name: Checkout repository - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 - - - name: Run upstream PR list script - env: - GH_TOKEN: ${{ github.token }} - run: | - python3 scripts/upstream_pr_list.py --since "${{ github.event.inputs.since }}" \ - > upstream_prs.jsonl - - - name: Upload PR list artifact - uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2 - with: - name: upstream-pr-list - path: upstream_prs.jsonl diff --git a/upstream_prs.jsonl b/upstream_prs.jsonl new file mode 100644 index 00000000000000..2e59889d5d7f5f --- /dev/null +++ b/upstream_prs.jsonl @@ -0,0 +1,136 @@ +{"number": 26292, "title": "[Merged by Bors] - feat(MeasureTheory): tightness of the range of a sequence", "author": "RemyDegenne", "created_at": "2025-06-23T08:33:50Z", "merged_at": "2026-03-02T19:02:00Z", "commenters": []} +{"number": 26303, "title": "[Merged by Bors] - feat(AlgebraicTopology): the fundamental lemma of homotopical algebra", "author": "joelriou", "created_at": "2025-06-23T14:11:15Z", "merged_at": "2026-03-03T18:35:36Z", "commenters": []} +{"number": 26588, "title": "[Merged by Bors] - feat(Algebra/GroupWithZero/WithZero): add the multiplicative embedding with zero from the range", "author": "faenuccio", "created_at": "2025-07-01T15:26:02Z", "merged_at": "2026-03-02T11:18:14Z", "commenters": []} +{"number": 26961, "title": "[Merged by Bors] - feat(RingTheory/PowerSeries/Substitution): add API", "author": "mariainesdff", "created_at": "2025-07-10T10:40:54Z", "merged_at": "2026-03-03T21:12:08Z", "commenters": []} +{"number": 30204, "title": "[Merged by Bors] - feat(Algebra/Category/Ring/EqualizerPushout): add effectiveEpi_of_faithfullyFlat in CommRingCat\u1d52\u1d56", "author": "yonggyuchoimath", "created_at": "2025-10-04T17:40:25Z", "merged_at": "2026-03-02T09:51:23Z", "commenters": []} +{"number": 30312, "title": "[Merged by Bors] - feat(RingTheory): define graded ring homomorphisms", "author": "kckennylau", "created_at": "2025-10-07T20:45:12Z", "merged_at": "2026-03-03T16:46:58Z", "commenters": []} +{"number": 30355, "title": "[Merged by Bors] - feat(Logic): graded functions", "author": "kckennylau", "created_at": "2025-10-09T01:03:15Z", "merged_at": "2026-03-02T12:12:03Z", "commenters": []} +{"number": 30811, "title": "[Merged by Bors] - feat(AlgebraicGeometry.EffectiveEpi): effective epimorphisms in schemes", "author": "yonggyuchoimath", "created_at": "2025-10-23T05:44:28Z", "merged_at": "2026-03-03T21:12:06Z", "commenters": []} +{"number": 31007, "title": "[Merged by Bors] - feat(RingTheory): generalise perfection to monoids", "author": "kckennylau", "created_at": "2025-10-28T13:55:27Z", "merged_at": "2026-03-03T16:04:21Z", "commenters": []} +{"number": 31132, "title": "[Merged by Bors] - feat(Algebra): saturation of a submonoid", "author": "kckennylau", "created_at": "2025-10-31T21:53:45Z", "merged_at": "2026-03-03T16:46:55Z", "commenters": []} +{"number": 31817, "title": "[Merged by Bors] - chore: remove extra monic hypotheses from divByMonic and modByMonic lemmas", "author": "kckennylau", "created_at": "2025-11-19T18:15:27Z", "merged_at": "2026-03-02T14:12:20Z", "commenters": []} +{"number": 33840, "title": "[Merged by Bors] - feat(SetTheory/Ordinal/CantorNormalForm): Evaluate a Finsupp as a CNF", "author": "vihdzp", "created_at": "2026-01-11T14:34:01Z", "merged_at": "2026-03-02T17:22:52Z", "commenters": []} +{"number": 34029, "title": "[Merged by Bors] - feat(Order/PartialSups): add exists_partialSups_eq", "author": "lua-vr", "created_at": "2026-01-16T03:05:03Z", "merged_at": "2026-03-03T21:12:03Z", "commenters": []} +{"number": 34049, "title": "[Merged by Bors] - refactor: use 1-field structure to define the `WithVal` type synonym", "author": "smmercuri", "created_at": "2026-01-16T14:53:19Z", "merged_at": "2026-03-02T11:18:11Z", "commenters": []} +{"number": 34189, "title": "[Merged by Bors] - feat(MeasureTheory/Measure): haarScalarFactor_map", "author": "bwangpj", "created_at": "2026-01-21T03:16:32Z", "merged_at": "2026-03-03T21:25:23Z", "commenters": []} +{"number": 34192, "title": "[Merged by Bors] - feat(MeasureTheory): mulEquivHaarChar_eq_one_of_compactSpace", "author": "bwangpj", "created_at": "2026-01-21T06:48:27Z", "merged_at": "2026-03-02T10:38:29Z", "commenters": []} +{"number": 34230, "title": "[Merged by Bors] - refactor: use 1-field structure to define the `WithAbs` type synonym", "author": "smmercuri", "created_at": "2026-01-21T19:52:32Z", "merged_at": "2026-03-02T17:22:49Z", "commenters": []} +{"number": 34267, "title": "[Merged by Bors] - feat(Topology/Algebra): Add API for Sheaves of abelian groups", "author": "Brian-Nugent", "created_at": "2026-01-22T18:45:27Z", "merged_at": "2026-03-02T10:51:28Z", "commenters": []} +{"number": 34611, "title": "[Merged by Bors] - feat: perfect subgroups", "author": "adomani", "created_at": "2026-01-30T13:01:10Z", "merged_at": "2026-03-02T11:18:09Z", "commenters": []} +{"number": 34658, "title": "[Merged by Bors] - feat(Algebra/Group/FiniteSupport): add HasFinite(Mul)Support and API", "author": "MichaelStollBayreuth", "created_at": "2026-01-31T18:38:45Z", "merged_at": "2026-03-03T18:35:34Z", "commenters": []} +{"number": 34877, "title": "[Merged by Bors] - refactor(RingTheory/Localization/Integral): Simplify `integerNormalization`", "author": "justus-springer", "created_at": "2026-02-05T16:31:49Z", "merged_at": "2026-03-02T23:42:37Z", "commenters": []} +{"number": 35005, "title": "[Merged by Bors] - chore(Algebra/Order/BigOperators): move lemmas which don't use addition out of Ring", "author": "b-mehta", "created_at": "2026-02-09T03:19:57Z", "merged_at": "2026-03-03T23:24:18Z", "commenters": []} +{"number": 35014, "title": "[Merged by Bors] - feat: Radon-Nikodym derivative of a composition-product", "author": "RemyDegenne", "created_at": "2026-02-09T10:41:10Z", "merged_at": "2026-03-02T11:18:07Z", "commenters": []} +{"number": 35015, "title": "[Merged by Bors] - feat: `rnDeriv` as ratio of densities wrt a dominating measure", "author": "RemyDegenne", "created_at": "2026-02-09T10:50:39Z", "merged_at": "2026-03-03T19:57:23Z", "commenters": []} +{"number": 35260, "title": "[Merged by Bors] - feat(Data/Fintype/Order): add API for ciSup with finite indexing type", "author": "MichaelStollBayreuth", "created_at": "2026-02-13T17:00:47Z", "merged_at": "2026-03-03T11:45:21Z", "commenters": []} +{"number": 35261, "title": "[Merged by Bors] - feat: `push` lemmas for `Filter.NeBot`", "author": "j-loreaux", "created_at": "2026-02-13T17:15:15Z", "merged_at": "2026-03-02T13:08:47Z", "commenters": []} +{"number": 35266, "title": "[Merged by Bors] - refactor: make `OrderIso.ofHomInv` take actual `OrderHom`s instead of using classes", "author": "j-loreaux", "created_at": "2026-02-13T17:32:43Z", "merged_at": "2026-03-02T12:12:01Z", "commenters": []} +{"number": 35269, "title": "[Merged by Bors] - refactor(Topology/Algebra/Module/LinearMap): adjust statement of `coe_mul` and `coe_pow`", "author": "tb65536", "created_at": "2026-02-13T18:29:14Z", "merged_at": "2026-03-03T16:30:31Z", "commenters": []} +{"number": 35301, "title": "[Merged by Bors] - feat: `klDiv` and scalar multiplication", "author": "RemyDegenne", "created_at": "2026-02-14T14:07:36Z", "merged_at": "2026-03-03T20:17:40Z", "commenters": []} +{"number": 35321, "title": "[Merged by Bors] - doc: capitalize the proper name Kan", "author": "harahu", "created_at": "2026-02-14T20:26:32Z", "merged_at": "2026-03-02T19:01:57Z", "commenters": []} +{"number": 35359, "title": "[Merged by Bors] - feat(Algebra/Homology/SpectralObject): kernel and cokernel of differentials", "author": "joelriou", "created_at": "2026-02-15T15:45:15Z", "merged_at": "2026-03-03T07:48:51Z", "commenters": []} +{"number": 35361, "title": "[Merged by Bors] - feat(Algebra/Homology/SpectralObject): cycles as cokernels and opcycles as kernels", "author": "joelriou", "created_at": "2026-02-15T15:52:26Z", "merged_at": "2026-03-03T10:51:19Z", "commenters": []} +{"number": 35362, "title": "[Merged by Bors] - feat(CategoryTheory/Triangulated/TStructure): more on `truncLT` and `truncGE`", "author": "joelriou", "created_at": "2026-02-15T16:04:57Z", "merged_at": "2026-03-02T15:40:16Z", "commenters": []} +{"number": 35363, "title": "[Merged by Bors] - feat(CategoryTheory/Triangulated/TStructure): properties of `truncLT` and `truncGE` which use the octahedron axiom", "author": "joelriou", "created_at": "2026-02-15T16:08:19Z", "merged_at": "2026-03-03T06:10:00Z", "commenters": []} +{"number": 35364, "title": "[Merged by Bors] - feat(CategoryTheory/Triangulated/TStructure): `truncLE` and `truncGT`", "author": "joelriou", "created_at": "2026-02-15T16:16:12Z", "merged_at": "2026-03-03T10:51:17Z", "commenters": []} +{"number": 35367, "title": "[Merged by Bors] - feat(CategoryTheory/Triangulated/TStucture): induced t-structures", "author": "joelriou", "created_at": "2026-02-15T16:27:00Z", "merged_at": "2026-03-03T17:27:42Z", "commenters": []} +{"number": 35372, "title": "[Merged by Bors] - feat(Algebra/Homology/SpectralObject): `SpectralSequenceDataCore`", "author": "joelriou", "created_at": "2026-02-15T17:07:28Z", "merged_at": "2026-03-03T16:04:18Z", "commenters": []} +{"number": 35437, "title": "[Merged by Bors] - chore(Topology): fix indentation in markdown lists", "author": "harahu", "created_at": "2026-02-17T10:43:32Z", "merged_at": "2026-03-02T17:22:47Z", "commenters": []} +{"number": 35496, "title": "[Merged by Bors] - feat(CategoryTheory/Triangulated): Rotated octahedron axiom", "author": "justus-springer", "created_at": "2026-02-18T15:53:34Z", "merged_at": "2026-03-02T10:08:34Z", "commenters": []} +{"number": 35497, "title": "[Merged by Bors] - feat(CategoryTheory/Triangulated): add extension_product", "author": "justus-springer", "created_at": "2026-02-18T15:59:35Z", "merged_at": "2026-03-02T13:08:44Z", "commenters": []} +{"number": 35515, "title": "[Merged by Bors] - feat(Topology/HomotopyGroup): Homeomorphism between GenLoop", "author": "WenrongZou", "created_at": "2026-02-19T01:03:58Z", "merged_at": "2026-03-03T05:11:35Z", "commenters": []} +{"number": 35544, "title": "[Merged by Bors] - feat(RingTheory): `I / I ^ 2` commutes with flat base change", "author": "chrisflav", "created_at": "2026-02-19T18:37:52Z", "merged_at": "2026-03-03T18:35:32Z", "commenters": []} +{"number": 35581, "title": "[Merged by Bors] - feat(RingTheory/MvPolynomial): MvPolynomial is isomorphic to the direct sum of its homogeneous submodules", "author": "mpenciak", "created_at": "2026-02-20T19:00:06Z", "merged_at": "2026-03-03T19:57:21Z", "commenters": []} +{"number": 35640, "title": "[Merged by Bors] - feat: Liouville Theorem for harmonic functions", "author": "kebekus", "created_at": "2026-02-22T09:11:10Z", "merged_at": "2026-03-02T20:45:34Z", "commenters": []} +{"number": 35699, "title": "[Merged by Bors] - chore(RingTheory/Etale/Kaehler): mention `FormallyEtale` in the names", "author": "chrisflav", "created_at": "2026-02-23T22:59:16Z", "merged_at": "2026-03-02T13:08:42Z", "commenters": []} +{"number": 35706, "title": "[Merged by Bors] - chore(Algebra/Group/Finsupp): fix argument names", "author": "vihdzp", "created_at": "2026-02-24T03:40:23Z", "merged_at": "2026-03-02T13:08:40Z", "commenters": []} +{"number": 35722, "title": "[Merged by Bors] - feat(CategoryTheory/Sites): the fiber functor associated to `Point.comap`", "author": "joelriou", "created_at": "2026-02-24T17:16:15Z", "merged_at": "2026-03-03T17:27:39Z", "commenters": []} +{"number": 35726, "title": "[Merged by Bors] - chore: golf using `simp`", "author": "euprunin", "created_at": "2026-02-24T18:27:12Z", "merged_at": "2026-03-02T17:22:45Z", "commenters": []} +{"number": 35727, "title": "[Merged by Bors] - chore(Analysis/Complex): simplify proof of `Complex.orderClosedTopology`", "author": "euprunin", "created_at": "2026-02-24T18:37:39Z", "merged_at": "2026-03-02T14:12:18Z", "commenters": []} +{"number": 35728, "title": "[Merged by Bors] - chore(SmoothSection): golf using custom elaborators", "author": "grunweg", "created_at": "2026-02-24T18:50:11Z", "merged_at": "2026-03-02T20:45:31Z", "commenters": []} +{"number": 35729, "title": "[Merged by Bors] - chore(Manifold/VectorBundle/LieBracket): golf using custom elaborators", "author": "grunweg", "created_at": "2026-02-24T18:50:38Z", "merged_at": "2026-03-02T19:01:54Z", "commenters": []} +{"number": 35730, "title": "[Merged by Bors] - chore(NumberTheory/ModularForms): golf using custom elaborators", "author": "grunweg", "created_at": "2026-02-24T18:51:57Z", "merged_at": "2026-03-02T23:42:35Z", "commenters": []} +{"number": 35736, "title": "[Merged by Bors] - chore(Mathlib/Topology/Algebra/Module/LinearMap.lean): automated extraction", "author": "mathlib-splicebot[bot]", "created_at": "2026-02-24T20:28:47Z", "merged_at": "2026-03-03T18:35:29Z", "commenters": []} +{"number": 35742, "title": "[Merged by Bors] - refactor: make `Order.pred_eq_sub_one` a simp lemma", "author": "vihdzp", "created_at": "2026-02-24T23:36:25Z", "merged_at": "2026-03-02T15:40:14Z", "commenters": []} +{"number": 35758, "title": "[Merged by Bors] - chore: use `to_dual` on `WellFoundedLT.toOrderBot`", "author": "vihdzp", "created_at": "2026-02-25T11:04:01Z", "merged_at": "2026-03-02T14:12:15Z", "commenters": []} +{"number": 35759, "title": "[Merged by Bors] - feat(CategoryTheory/Elements): functors to types are colimits of corepresentable functors", "author": "joelriou", "created_at": "2026-02-25T11:15:24Z", "merged_at": "2026-03-03T13:53:35Z", "commenters": []} +{"number": 35768, "title": "[Merged by Bors] - feat(RingTheory/DividedPowers/Basic): add lemmas", "author": "mariainesdff", "created_at": "2026-02-25T15:44:26Z", "merged_at": "2026-03-03T14:05:26Z", "commenters": []} +{"number": 35770, "title": "[Merged by Bors] - feat(RingTheory/Localization/FractionRing): add DecidableEq instance", "author": "mariainesdff", "created_at": "2026-02-25T16:03:40Z", "merged_at": "2026-03-02T12:11:58Z", "commenters": []} +{"number": 35782, "title": "[Merged by Bors] - feat(MeasureTheory): Add an AEMeasurable version of `Measure.map_add`", "author": "DavidLedvinka", "created_at": "2026-02-25T22:22:29Z", "merged_at": "2026-03-02T12:11:56Z", "commenters": []} +{"number": 35784, "title": "[Merged by Bors] - feat(MeasureTheory): Add `MeasurableSingletonClass` version of `Measure.map_dirac`", "author": "DavidLedvinka", "created_at": "2026-02-25T23:11:55Z", "merged_at": "2026-03-02T10:26:37Z", "commenters": []} +{"number": 35787, "title": "[Merged by Bors] - feat(Analysis/SchwartzSpace): post composition with continuous linear map", "author": "mcdoll", "created_at": "2026-02-25T23:41:35Z", "merged_at": "2026-03-02T23:55:25Z", "commenters": []} +{"number": 35806, "title": "[Merged by Bors] - feat(CategoryTheory/Monoidal/Limits): colimit of tensor products", "author": "joelriou", "created_at": "2026-02-26T10:35:53Z", "merged_at": "2026-03-03T01:27:43Z", "commenters": []} +{"number": 35809, "title": "[Merged by Bors] - refactor(Algebra/Algebra/Subalgebra/Operations): generalize `FixedPoints.subalgebra` to `Semiring` by introducing `FixedPoints.subsemiring`", "author": "tb65536", "created_at": "2026-02-26T12:50:26Z", "merged_at": "2026-03-03T23:24:15Z", "commenters": []} +{"number": 35810, "title": "[Merged by Bors] - feat(NumberTheory/ArithmeticFunction/Defs): define the Dirichlet inverse of an arithmetic function", "author": "tb65536", "created_at": "2026-02-26T13:13:18Z", "merged_at": "2026-03-02T20:45:29Z", "commenters": []} +{"number": 35814, "title": "[Merged by Bors] - chore(Tactic): rewrite `field`/`field_simp` tactic documentation", "author": "Vierkantor", "created_at": "2026-02-26T14:38:32Z", "merged_at": "2026-03-02T14:12:13Z", "commenters": []} +{"number": 35823, "title": "[Merged by Bors] - ci: Decouple workflow scripts into the mathlib-ci repository", "author": "marcelolynch", "created_at": "2026-02-26T18:02:17Z", "merged_at": "2026-03-02T17:22:41Z", "commenters": []} +{"number": 35824, "title": "[Merged by Bors] - refactor(GroupTheory/Nilpotent): add junk value to `Group.nilpotencyClass`", "author": "tb65536", "created_at": "2026-02-26T19:14:29Z", "merged_at": "2026-03-03T23:24:13Z", "commenters": []} +{"number": 35835, "title": "[Merged by Bors] - feat(MeasureTheory): add lemma for sum_smul_dirac_singleton", "author": "b-mehta", "created_at": "2026-02-27T01:38:16Z", "merged_at": "2026-03-02T10:26:34Z", "commenters": []} +{"number": 35837, "title": "[Merged by Bors] - feat(LinearAlgebra/AffineSpace): iff lemma about the inverse of a homothety", "author": "wwylele", "created_at": "2026-02-27T02:38:37Z", "merged_at": "2026-03-02T22:22:16Z", "commenters": []} +{"number": 35845, "title": "[Merged by Bors] - chore(AlgebraicGeometry): Remove TODO and fix documentation", "author": "Brian-Nugent", "created_at": "2026-02-27T05:29:06Z", "merged_at": "2026-03-02T15:40:11Z", "commenters": []} +{"number": 35855, "title": "[Merged by Bors] - chore(SetTheory/Ordinal/Basic): deprecate `Ordinal.induction` \u2192 `WellFoundedLT.induction`", "author": "vihdzp", "created_at": "2026-02-27T09:39:48Z", "merged_at": "2026-03-02T13:08:38Z", "commenters": []} +{"number": 35856, "title": "[Merged by Bors] - doc(misc): fix typos", "author": "harahu", "created_at": "2026-02-27T09:40:37Z", "merged_at": "2026-03-02T19:01:52Z", "commenters": []} +{"number": 35870, "title": "[Merged by Bors] - feat: weaken assumptions for integration by parts", "author": "fpvandoorn", "created_at": "2026-02-27T14:51:07Z", "merged_at": "2026-03-02T22:22:14Z", "commenters": []} +{"number": 35873, "title": "[Merged by Bors] - chore: delete deprecated modules to end August 2025", "author": "Parcly-Taxel", "created_at": "2026-02-27T18:32:52Z", "merged_at": "2026-03-02T15:40:08Z", "commenters": []} +{"number": 35875, "title": "[Merged by Bors] - fix(Translate): remap ConstantInfo.all during declaration translation", "author": "adamtopaz", "created_at": "2026-02-27T21:04:06Z", "merged_at": "2026-03-02T13:08:35Z", "commenters": []} +{"number": 35891, "title": "[Merged by Bors] - chore: move differential geometry elaborators tests into a separate directory", "author": "grunweg", "created_at": "2026-02-28T15:53:54Z", "merged_at": "2026-03-02T15:40:06Z", "commenters": []} +{"number": 35898, "title": "[Merged by Bors] - feat(Algebra/Star/StarProjection): add `IsStarProjection.map`", "author": "themathqueen", "created_at": "2026-02-28T21:51:17Z", "merged_at": "2026-03-02T19:01:50Z", "commenters": []} +{"number": 35901, "title": "[Merged by Bors] - feat(CategoryTheory/Sites): isomorphic hypercovers have equivalent sheaf conditions", "author": "chrisflav", "created_at": "2026-02-28T23:02:17Z", "merged_at": "2026-03-03T13:53:33Z", "commenters": []} +{"number": 35902, "title": "[Merged by Bors] - feat(CategoryTheory/Sites): homotopy equivalent hypercovers have equivalent sheaf conditions", "author": "chrisflav", "created_at": "2026-02-28T23:56:34Z", "merged_at": "2026-03-03T13:53:30Z", "commenters": []} +{"number": 35903, "title": "[Merged by Bors] - chore: make CompleteLattice helpers instance reducible", "author": "matthewjasper", "created_at": "2026-03-01T00:06:30Z", "merged_at": "2026-03-02T17:22:38Z", "commenters": []} +{"number": 35915, "title": "[Merged by Bors] - feat(AlgebraicGeometry): constant sheaf associated to a topological space", "author": "chrisflav", "created_at": "2026-03-01T12:10:38Z", "merged_at": "2026-03-02T12:11:54Z", "commenters": []} +{"number": 35918, "title": "[Merged by Bors] - feat(GroupTheory/Descent): add abstract descent theorem", "author": "MichaelStollBayreuth", "created_at": "2026-03-01T14:31:10Z", "merged_at": "2026-03-02T17:22:36Z", "commenters": []} +{"number": 35919, "title": "[Merged by Bors] - feat(NumberTheory/Height): formula for logHeight\u2081", "author": "MichaelStollBayreuth", "created_at": "2026-03-01T14:58:54Z", "merged_at": "2026-03-02T17:22:33Z", "commenters": []} +{"number": 35920, "title": "[Merged by Bors] - chore(CategoryTheory/Sites): generalize `Precoverage.toGrothendieck_le_iff_le_toPrecoverage`", "author": "chrisflav", "created_at": "2026-03-01T15:09:15Z", "merged_at": "2026-03-03T16:30:29Z", "commenters": []} +{"number": 35924, "title": "[Merged by Bors] - feat(NumberTheory/Height/NumberField): lemmas/positivity extension for `totalWeight`", "author": "MichaelStollBayreuth", "created_at": "2026-03-01T16:30:20Z", "merged_at": "2026-03-03T18:35:27Z", "commenters": []} +{"number": 35926, "title": "[Merged by Bors] - chore(ENNReal/Inv): lemma variants for `norm_cast`", "author": "hrmacbeth", "created_at": "2026-03-01T17:53:44Z", "merged_at": "2026-03-03T20:17:38Z", "commenters": []} +{"number": 35929, "title": "[Merged by Bors] - feat(Algebra/Homology): the mapping cocone", "author": "joelriou", "created_at": "2026-03-01T19:20:57Z", "merged_at": "2026-03-03T01:14:21Z", "commenters": []} +{"number": 35930, "title": "[Merged by Bors] - feat(CategoryTheory/Abelian): lemmas for diagram chasing in short complexes", "author": "joelriou", "created_at": "2026-03-01T19:28:12Z", "merged_at": "2026-03-02T13:08:33Z", "commenters": []} +{"number": 35931, "title": "[Merged by Bors] - feat(Algebra/Homology): lemmas for diagram chasing in homological complexes", "author": "joelriou", "created_at": "2026-03-01T19:30:41Z", "merged_at": "2026-03-03T16:30:26Z", "commenters": []} +{"number": 35932, "title": "[Merged by Bors] - chore(CategoryTheory): improve Factorisation", "author": "joelriou", "created_at": "2026-03-01T19:35:21Z", "merged_at": "2026-03-02T12:11:52Z", "commenters": []} +{"number": 35934, "title": "[Merged by Bors] - feat(Algebra/Homology): more lemmas for the biproduct of complexes", "author": "joelriou", "created_at": "2026-03-01T19:39:15Z", "merged_at": "2026-03-02T14:12:09Z", "commenters": []} +{"number": 35935, "title": "[Merged by Bors] - feat(Algebra/Homology): limits of degreewise eventually constant projective systems", "author": "joelriou", "created_at": "2026-03-01T19:42:24Z", "merged_at": "2026-03-02T13:08:31Z", "commenters": []} +{"number": 35936, "title": "[Merged by Bors] - feat(Algebra/Homology): lemmas and instances for truncation of cochain complexes", "author": "joelriou", "created_at": "2026-03-01T19:45:48Z", "merged_at": "2026-03-02T23:42:32Z", "commenters": []} +{"number": 35937, "title": "[Merged by Bors] - feat(CategoryTheory/Shift): naturality lemmas for ShiftedHom.map", "author": "joelriou", "created_at": "2026-03-01T19:48:09Z", "merged_at": "2026-03-02T12:11:49Z", "commenters": []} +{"number": 35938, "title": "[Merged by Bors] - feat(Algebra/Homology): compatibilities for homology functors", "author": "joelriou", "created_at": "2026-03-01T19:57:40Z", "merged_at": "2026-03-02T23:42:30Z", "commenters": []} +{"number": 35949, "title": "[Merged by Bors] - chore(Mathlib/CategoryTheory/Sites): more API for `Presieve.map`", "author": "mathlib-splicebot[bot]", "created_at": "2026-03-02T01:38:17Z", "merged_at": "2026-03-03T14:20:49Z", "commenters": []} +{"number": 35952, "title": "[Merged by Bors] - chore: add/remove `set_option backward` after moving to `v4.29.0-rc3`", "author": "kim-em", "created_at": "2026-03-02T04:09:08Z", "merged_at": "2026-03-03T00:44:29Z", "commenters": []} +{"number": 35959, "title": "[Merged by Bors] - chore: fix defeq abuse in Boolean Algebra instance on Set alpha", "author": "sgouezel", "created_at": "2026-03-02T08:02:34Z", "merged_at": "2026-03-02T22:22:12Z", "commenters": []} +{"number": 35967, "title": "[Merged by Bors] - feat(CategoryTheory/Monoidal/Grp_): `Grp` has terminal objects", "author": "tb65536", "created_at": "2026-03-02T10:58:47Z", "merged_at": "2026-03-02T13:08:29Z", "commenters": []} +{"number": 35968, "title": "[Merged by Bors] - feat: characteristic function of a sum of independent variables", "author": "EtienneC30", "created_at": "2026-03-02T11:12:49Z", "merged_at": "2026-03-02T13:08:27Z", "commenters": []} +{"number": 35969, "title": "[Merged by Bors] - feat(GroupTheory): explicit isomorphism between infinite cyclic groups and Z", "author": "erdOne", "created_at": "2026-03-02T11:12:56Z", "merged_at": "2026-03-02T19:01:48Z", "commenters": []} +{"number": 35972, "title": "[Merged by Bors] - chore: fix naming in `WithVal`", "author": "smmercuri", "created_at": "2026-03-02T12:08:48Z", "merged_at": "2026-03-02T20:45:26Z", "commenters": []} +{"number": 35973, "title": "[Merged by Bors] - feat(Algebra/Polynomial/BigOperators): A lemma about degrees of sums", "author": "justus-springer", "created_at": "2026-03-02T12:31:08Z", "merged_at": "2026-03-03T21:12:00Z", "commenters": []} +{"number": 35975, "title": "[Merged by Bors] - feat: inv_bijective", "author": "Ruben-VandeVelde", "created_at": "2026-03-02T12:45:00Z", "merged_at": "2026-03-03T10:35:25Z", "commenters": []} +{"number": 35978, "title": "[Merged by Bors] - chore(Topology/FiberBundle/Trivialisation): more simp lemmas", "author": "grunweg", "created_at": "2026-03-02T13:31:16Z", "merged_at": "2026-03-03T10:35:23Z", "commenters": []} +{"number": 35980, "title": "[Merged by Bors] - feat: covering numbers and isometries", "author": "RemyDegenne", "created_at": "2026-03-02T13:52:59Z", "merged_at": "2026-03-03T14:05:23Z", "commenters": []} +{"number": 35981, "title": "[Merged by Bors] - chore(RepresentationTheory/Basic): generalise to Semiring", "author": "Whysoserioushah", "created_at": "2026-03-02T13:59:51Z", "merged_at": "2026-03-02T17:22:30Z", "commenters": []} +{"number": 35982, "title": "[Merged by Bors] - feat(CategoryTheory/Monoidal/Grp_): zero morphisms in `Grp C`", "author": "tb65536", "created_at": "2026-03-02T14:06:14Z", "merged_at": "2026-03-02T17:22:28Z", "commenters": []} +{"number": 35983, "title": "[Merged by Bors] - refactor(Topology/Sheaves/LocallySurjective): change `isLocallySurjective_iff`", "author": "smorel394", "created_at": "2026-03-02T14:21:27Z", "merged_at": "2026-03-02T15:40:03Z", "commenters": []} +{"number": 35990, "title": "[Merged by Bors] - fix: `linarith` `splitNe` skips hypotheses without `LinearOrder`", "author": "emmanuel-ferdman", "created_at": "2026-03-02T16:28:16Z", "merged_at": "2026-03-02T23:42:28Z", "commenters": []} +{"number": 35992, "title": "[Merged by Bors] - feat(Analysis/CStarAlgebra/Basic): `\u2016e\u2016 \u2264 1` for star projections", "author": "themathqueen", "created_at": "2026-03-02T17:27:49Z", "merged_at": "2026-03-03T13:53:28Z", "commenters": []} +{"number": 35995, "title": "[Merged by Bors] - chore: Make {Preorder,PartialOrder}.mk abbrevs", "author": "matthewjasper", "created_at": "2026-03-02T18:29:12Z", "merged_at": "2026-03-02T20:45:24Z", "commenters": []} +{"number": 35996, "title": "[Merged by Bors] - feat(CategoryTheory/Monoidal/Limits): generalise universes and explicit limits for limits of monoid objects", "author": "b-mehta", "created_at": "2026-03-02T18:29:52Z", "merged_at": "2026-03-03T16:04:15Z", "commenters": []} +{"number": 35999, "title": "[Merged by Bors] - fix(scripts): fix a link to radar", "author": "harahu", "created_at": "2026-03-02T19:25:50Z", "merged_at": "2026-03-03T06:20:12Z", "commenters": []} +{"number": 36002, "title": "[Merged by Bors] - feat(CategoryTheory/Monoidal/Grp_): a monoid object with invertible homs is a group object", "author": "tb65536", "created_at": "2026-03-02T21:49:32Z", "merged_at": "2026-03-03T18:35:24Z", "commenters": []} +{"number": 36004, "title": "[Merged by Bors] - feat(CategoryTheory/Limits/Preserves/FunctorCategory): add `ReflectsLimitsOfShape` instance for `whiskeringRight`", "author": "tb65536", "created_at": "2026-03-02T21:57:13Z", "merged_at": "2026-03-03T10:51:14Z", "commenters": []} +{"number": 36021, "title": "[Merged by Bors] - chore: remove `set_option backward.isDefEq.respectTransparency false`", "author": "kim-em", "created_at": "2026-03-03T02:50:01Z", "merged_at": "2026-03-03T05:58:32Z", "commenters": []} +{"number": 36025, "title": "[Merged by Bors] - feat: taylor expansion of the characteristic function", "author": "EtienneC30", "created_at": "2026-03-03T08:58:13Z", "merged_at": "2026-03-03T17:27:36Z", "commenters": []} +{"number": 36026, "title": "[Merged by Bors] - chore: rename theorems to comply with mathlib standards", "author": "kebekus", "created_at": "2026-03-03T08:59:16Z", "merged_at": "2026-03-03T09:40:19Z", "commenters": []} +{"number": 36027, "title": "[Merged by Bors] - feat: monotonicity of norm integrability", "author": "EtienneC30", "created_at": "2026-03-03T09:05:21Z", "merged_at": "2026-03-03T09:28:47Z", "commenters": []} +{"number": 36028, "title": "[Merged by Bors] - feat: iterated Fr\u00e9chet derivative of a composition with scalar multiplication", "author": "EtienneC30", "created_at": "2026-03-03T09:13:50Z", "merged_at": "2026-03-03T10:35:21Z", "commenters": []} +{"number": 36034, "title": "[Merged by Bors] - chore: add missing fast_instance on instances on the subtype of nonnegative elements", "author": "sgouezel", "created_at": "2026-03-03T09:56:48Z", "merged_at": "2026-03-03T13:53:26Z", "commenters": []} +{"number": 36035, "title": "[Merged by Bors] - feat: taylor expansion within `univ`", "author": "EtienneC30", "created_at": "2026-03-03T10:00:54Z", "merged_at": "2026-03-03T10:51:12Z", "commenters": []} +{"number": 36039, "title": "[Merged by Bors] - feat: variance of a sum with respect to the product measure", "author": "EtienneC30", "created_at": "2026-03-03T10:31:54Z", "merged_at": "2026-03-03T10:51:09Z", "commenters": []} +{"number": 36044, "title": "[Merged by Bors] - chore(RingTheory): reorganize imports around locality properties of finiteness", "author": "chrisflav", "created_at": "2026-03-03T11:07:42Z", "merged_at": "2026-03-03T15:09:37Z", "commenters": []} +{"number": 36046, "title": "[Merged by Bors] - refactor(Topology/Category/TopCat/Opens): split off part of `IsOpenMap.functor`", "author": "smorel394", "created_at": "2026-03-03T11:13:38Z", "merged_at": "2026-03-03T12:51:46Z", "commenters": []} +{"number": 36047, "title": "[Merged by Bors] - chore(RepresentationTheory/Intertwining): Generalise and add lemmas", "author": "Whysoserioushah", "created_at": "2026-03-03T11:14:01Z", "merged_at": "2026-03-03T14:20:46Z", "commenters": []} +{"number": 36049, "title": "[Merged by Bors] - feat: generalize Liouville's theorem for harmonic functions", "author": "kebekus", "created_at": "2026-03-03T11:39:00Z", "merged_at": "2026-03-03T16:30:23Z", "commenters": []} +{"number": 36052, "title": "[Merged by Bors] - feat(Algebra/Homology): bounded below cochain complexes", "author": "joelriou", "created_at": "2026-03-03T12:13:08Z", "merged_at": "2026-03-03T17:54:05Z", "commenters": []} +{"number": 36057, "title": "[Merged by Bors] - feat(Topology/Sheaves/Presheaf): pullback of a presheaf by an open map", "author": "smorel394", "created_at": "2026-03-03T13:52:40Z", "merged_at": "2026-03-03T16:04:12Z", "commenters": []} +{"number": 36058, "title": "[Merged by Bors] - feat: more versions of the characteristic function of a sum", "author": "EtienneC30", "created_at": "2026-03-03T14:03:34Z", "merged_at": "2026-03-03T17:54:03Z", "commenters": []} +{"number": 36061, "title": "[Merged by Bors] - feat(CategoryTheory/Sites): topology on `Over X` is subcanonical if the topology on the base is subcanonical", "author": "chrisflav", "created_at": "2026-03-03T14:53:55Z", "merged_at": "2026-03-03T16:04:09Z", "commenters": []} +{"number": 36071, "title": "[Merged by Bors] - feat(Topology/Sheaves/Functors): pullback of a sheaf by an open embedding", "author": "smorel394", "created_at": "2026-03-03T16:46:18Z", "merged_at": "2026-03-03T19:57:18Z", "commenters": []} +{"number": 36074, "title": "[Merged by Bors] - refactor(Topology/Sheaves): harmonize names", "author": "smorel394", "created_at": "2026-03-03T17:15:52Z", "merged_at": "2026-03-03T20:17:35Z", "commenters": []} +{"number": 36076, "title": "[Merged by Bors] - feat: deprecate file", "author": "EtienneC30", "created_at": "2026-03-03T17:38:34Z", "merged_at": "2026-03-03T23:24:11Z", "commenters": []} +{"number": 36085, "title": "[Merged by Bors] - chore: remove superfluous usage of `simpa using by ...`", "author": "tb65536", "created_at": "2026-03-03T21:44:22Z", "merged_at": "2026-03-03T22:44:58Z", "commenters": []}