Maintainers page: short tasks

Are you a maintainer with just a short amount of time? The following kinds of pull requests could be relevant for you.

If you realise you actually have a bit more time, you can also look at the page for reviewers, or look at the triage page!
This dashboard was last updated on: July 01, 2025 at 10:32 UTC

Stale ready-to-merge'd PRs

Number Author Title Description Labels +/- Modified files (first 100) 📝 💬 All users who commented or reviewed Assignee(s) Updated Last status change total time in review
26161 leanprover-community-mathlib4-bot
author:leanprover-community-mathlib4-bot
 chore: adaptations for nightly-2025-06-19 merge-conflict ready-to-merge 26/19 Mathlib/Algebra/CharP/Basic.lean,Mathlib/Algebra/CharP/Defs.lean,Mathlib/Algebra/Group/Basic.lean,lake-manifest.json,lean-toolchain 5 n/a ['YaelDillies', 'github-actions', 'kim-em', 'mathlib-bors'] nobody
11-39017
11 days ago
unknown
unknown

Stale maintainer-merge'd PRs

Number Author Title Description Labels +/- Modified files (first 100) 📝 💬 All users who commented or reviewed Assignee(s) Updated Last status change total time in review
25265 FMLJohn
author:FMLJohn
 feat(Order/SupClosed): `compl_image_latticeClosure` and `compl_image_latticeClosure_eq_of_compl_image_eq_self` The main results in this pull request are: 1. `compl_image_latticeClosure`: given any Boolean algebra `α` and `s : Set α`, `compl '' latticeClosure s` is the same as `latticeClosure (compl '' s)`; 2. `compl_image_latticeClosure_eq_of_compl_image_eq_self`: given any Boolean algebra `α` and `s : Set α` such that `compl '' s = s`, we have `compl '' latticeClosure s = latticeClosure s`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-order 59/1 Mathlib/Order/SupClosed.lean 1 8 ['FMLJohn', 'YaelDillies', 'github-actions'] bryangingechen
assignee:bryangingechen
25-74084
25 days ago
28-54056
28 days ago
32-63674
32 days
25089 Bergschaf
author:Bergschaf
 feat(Order/Sublocale): definition of sublocales There are several possible definition of sublocales. I used one from [nlab](https://ncatlab.org/nlab/show/sublocale) which states that a sublocale is a subset of a locale which is closed under all meets and for any ∈ S and x ∈ X, we have x ⇨ s ∈ S. This PR also includes an order isomorphism between (Nucleus)ᵒᵈ and Sublocale. --- I am open to better name suggestions for the order isomorphism. - [x] depends on: #24941 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-order 265/8 Mathlib.lean,Mathlib/Order/Hom/Lattice.lean,Mathlib/Order/Nucleus.lean,Mathlib/Order/Sublocale.lean,Mathlib/Order/Synonym.lean,docs/references.bib 6 71 ['Bergschaf', 'YaelDillies', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'xhalo32'] nobody
23-52890
23 days ago
23-52890
23 days ago
37-32312
37 days
25563 Komyyy
author:Komyyy
 chore: move `Topology.StoneCech` into `Topology.Compactification` (1/2) At present, the `Topology.Compactification` directory includes results on one-point compactifications, but results on Stone-Čech compactifications are currently located elsewhere. The removed file `Topology.Compactification` is deprecated in another PR (#25583) to leave a good git diff history. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) file-removed maintainer-merge t-topology 9/9 Mathlib.lean,Mathlib/Combinatorics/Hindman.lean,Mathlib/Topology/Category/CompHaus/Basic.lean,Mathlib/Topology/Category/CompHaus/Projective.lean,Mathlib/Topology/Category/Profinite/Projective.lean,Mathlib/Topology/Category/Stonean/Adjunctions.lean,Mathlib/Topology/Compactification/StoneCech.lean,Mathlib/Topology/ExtremallyDisconnected.lean,Mathlib/Topology/Maps/Proper/UniversallyClosed.lean,Mathlib/Topology/Separation/CompletelyRegular.lean 10 4 ['Komyyy', 'github-actions', 'grunweg'] nobody
23-7646
23 days ago
23-7646
23 days ago
23-69578
23 days
25600 Komyyy
author:Komyyy
 refactor: lemma expressing `ContinuousAt` using a punctured neighbourhood --- This lemma is used to prove that the Riemann zeta function is meromorphic in #25597. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-topology 4/0 Mathlib/Topology/ContinuousOn.lean 1 5 ['Komyyy', 'github-actions', 'grunweg'] nobody
22-44763
22 days ago
22-44763
22 days ago
22-56650
22 days
24669 qawbecrdtey
author:qawbecrdtey
 feat(Analysis/Normed/Operator/LinearIsometry): added definition `LinearIsometryEquiv.prodComm` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) This commit defines a `LinearIsometryEquiv`, and states some trivial theorems about it. ```lean def prodComm [Module R E₂] : E × E₂ ≃ₗᵢ[R] E₂ × E ``` maintainer-merge t-analysis awaiting-author 8/1 Mathlib/Analysis/Normed/Operator/LinearIsometry.lean 1 10 ['Ruben-VandeVelde', 'eric-wieser', 'faenuccio', 'github-actions', 'j-loreaux', 'jcommelin', 'qawbecrdtey'] faenuccio
assignee:faenuccio
21-20148
21 days ago
21-20148
21 days ago
32-83569
32 days
23849 chrisflav
author:chrisflav
 feat(Data/Set): add `Set.encard_iUnion` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) large-import t-data maintainer-merge 69/0 Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Data/Set/Card/Arithmetic.lean,Mathlib/Data/Set/Finite/Lattice.lean 3 25 ['YaelDillies', 'chrisflav', 'github-actions'] YaelDillies
assignee:YaelDillies
20-82611
20 days ago
20-82611
20 days ago
83-10001
83 days
25881 eric-wieser
author:eric-wieser
 chore: extract an auxiliary function from `congr()` The motivation here is to make it easier to review #25851. This code is moved (and unindented) without changes. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip maintainer-merge t-meta 72/61 Mathlib/Tactic/TermCongr.lean 1 5 ['eric-wieser', 'github-actions', 'grunweg', 'kmill'] nobody
16-46498
16 days ago
16-46498
16 days ago
0-3293
54 minutes
25172 eric-wieser
author:eric-wieser
 feat: restricting `Affine.Simplex` to an affine subspace that contains it Also removes a redundant `Nonempty` argument. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-euclidean-geometry 68/5 Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean,Mathlib/LinearAlgebra/AffineSpace/Independent.lean 2 11 ['eric-wieser', 'github-actions', 'jsm28', 'ocfnash'] nobody
4-51515
4 days ago
36-78106
1 month ago
37-32578
37 days
26405 euprunin
author:euprunin
 chore: golf using `omega` maintainer-merge 23/68 Mathlib/Algebra/Polynomial/Module/Basic.lean,Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean,Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean,Mathlib/Combinatorics/Enumerative/Composition.lean,Mathlib/Computability/DFA.lean,Mathlib/Control/Fix.lean,Mathlib/Data/Nat/Choose/Basic.lean,Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean,Mathlib/Geometry/Euclidean/Circumcenter.lean,Mathlib/GroupTheory/Coxeter/Length.lean,Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean,Mathlib/MeasureTheory/Function/ConditionalExpectation/Unique.lean,Mathlib/NumberTheory/Dioph.lean,Mathlib/Order/Partition/Equipartition.lean,Mathlib/SetTheory/Game/State.lean,Mathlib/Tactic/NormNum/LegendreSymbol.lean,Mathlib/Topology/EMetricSpace/BoundedVariation.lean 17 10 ['euprunin', 'github-actions', 'grunweg', 'leanprover-bot'] nobody
4-39067
4 days ago
4-39067
4 days ago
5-75936
5 days
26004 vasnesterov
author:vasnesterov
 feat(Algebra/Order/Floor): `⌊n * x⌋₊ / n = ⌊x⌋₊` Prove that `⌊n * x⌋₊ / n = ⌊x⌋₊` for natural `n`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-order t-algebra
label:t-algebra$
 39/9 Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean,Mathlib/Algebra/Order/Floor/Ring.lean,Mathlib/Algebra/Order/Floor/Semiring.lean,Mathlib/Data/EReal/Inv.lean 4 21 ['Ruben-VandeVelde', 'YaelDillies', 'b-mehta', 'eric-wieser', 'github-actions', 'vasnesterov'] nobody
4-12344
4 days ago
unknown
unknown
26426 Komyyy
author:Komyyy
 doc: remove `PartENat.card` in the module doc [`PartENat.card`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Deprecated/Cardinal/Finite.html#PartENat.card) is moved to the `Deprecated` directory and it's not in this file([`Mathlib.SetTheory.Cardinal.Finite`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/SetTheory/Cardinal/Finite.html)) anymore. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-set-theory maintainer-merge easy documentation 0/2 Mathlib/SetTheory/Cardinal/Finite.lean 1 2 ['github-actions', 'grunweg'] nobody
4-3984
4 days ago
4-3984
4 days ago
4-3997
4 days
26502 sgouezel
author:sgouezel
 feat: monotonicity of `lineMap` Also remove one assumption in `differentiableOn_integral_of_continuous`, and expand docstrings around this theorem. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-analysis 49/10 Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/FundThmCalculus.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/IntegrationByParts.lean,Mathlib/Topology/Algebra/ContinuousAffineMap.lean 4 6 ['eric-wieser', 'github-actions', 'grunweg', 'sgouezel'] nobody
1-80203
1 day ago
2-12994
2 days ago
2-18594
2 days
26166 joelriou
author:joelriou
 feat(AlgebraicTopology): application of the retract argument to model categories Basic consequences of the retract argument are obtained for model categories: cofibrations are exactly the morphisms that have the left lifting property with respect to trivial fibrations, etc. We deduce various properties of cofibrations, fibrations and weak equivalences in model categories (e.g. they are stable by composition). --- (I am sorry if this one is a little bit long. There are too many basic properties to state.) This PR continues the work from #20210. Original PR: https://github.com/leanprover-community/mathlib4/pull/20210 large-import maintainer-merge t-topology 450/4 Mathlib.lean,Mathlib/AlgebraicTopology/ModelCategory/Basic.lean,Mathlib/AlgebraicTopology/ModelCategory/Instances.lean 3 n/a ['github-actions', 'joelriou', 'robin-carlier'] robin-carlier
assignee:robin-carlier
1-15041
1 day ago
unknown
unknown
24361 Hagb
author:Hagb
 feat(Data/Finsupp/MonomialOrder): `0 ≤ a` where `a : m.syn` `simp` would be able to solve it. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data maintainer-merge new-contributor easy 3/0 Mathlib/Data/Finsupp/MonomialOrder.lean 1 2 ['Ruben-VandeVelde', 'github-actions'] nobody
1-8937
1 day ago
1-8937
1 day ago
67-9699
67 days
24582 pechersky
author:pechersky
 feat(GroupTheory/ArchimedeanDensely): Unique (ℤ ≃+o ℤ) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) - [x] depends on: #24580 maintainer-merge t-order t-algebra
label:t-algebra$
 44/0 Mathlib/Data/Int/Cast/Lemmas.lean,Mathlib/GroupTheory/ArchimedeanDensely.lean 2 6 ['Ruben-VandeVelde', 'eric-wieser', 'github-actions', 'mathlib4-dependent-issues-bot', 'pechersky'] nobody
1-5828
1 day ago
1-5828
1 day ago
36-80434
36 days
25758 YaelDillies
author:YaelDillies
 chore: shortcut instance `CompleteLattice α → PartialOrder α` This avoids using the path `CompleteLattice α → CompletePartialOrder α → PartialOrder α` that goes through `Order.CompletePartialOrder` and makes it appear used to our automation, such as `shake` or `#min_imports`. This is a followup to #25358. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-order 7/0 Mathlib/Order/CompleteLattice/Defs.lean 1 2 ['Ruben-VandeVelde', 'github-actions'] nobody
1-5719
1 day ago
1-5719
1 day ago
19-6207
19 days
25897 YaelDillies
author:YaelDillies
 feat: `ofNat(n) • a = ofNat(n) * a` From Toric --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) toric t-data maintainer-merge t-algebra
label:t-algebra$
 3/0 Mathlib/Data/Nat/Cast/Basic.lean 1 2 ['Ruben-VandeVelde', 'github-actions'] nobody
1-5598
1 day ago
1-5598
1 day ago
16-3108
16 days
26027 vasnesterov
author:vasnesterov
 feat(Topology): every compact metric space can be embedded into the Hilbert cube Prove `exists_closed_embedding_to_hilbert_cube`: every compact metric space can be embedded into the Hilbert cube. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-topology 58/1 Mathlib.lean,Mathlib/Topology/Compactness/HilbertCubeEmbedding.lean,Mathlib/Topology/MetricSpace/Bounded.lean 3 9 ['ADedecker', 'github-actions', 'jcommelin', 'vasnesterov'] nobody
1-2856
1 day ago
1-2856
1 day ago
13-71815
13 days
21751 vihdzp
author:vihdzp
 refactor(SetTheory/Ordinal/Arithmetic): rework `Ordinal.pred` API This PR does the following: - give a simpler definition of `Ordinal.pred` - replace `¬ ∃ a, o = succ a` and `∀ a, o ≠ succ a` by `IsSuccPrelimit o` throughout - improve theorem names --- There's a legitimate question of whether we even want `Ordinal.pred` (see [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Ordinal.2Epred)) but this should be a good change in the meanwhile regardless. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-set-theory maintainer-merge merge-conflict 102/67 Mathlib/SetTheory/Ordinal/Arithmetic.lean,Mathlib/SetTheory/Ordinal/Exponential.lean 2 13 ['YaelDillies', 'github-actions', 'grunweg', 'vihdzp'] nobody
55-45333
1 month ago
102-23960
3 months ago
36-50134
36 days
24965 erdOne
author:erdOne
 refactor: Make `IsLocalHom` take unbundled map --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-algebra merge-conflict awaiting-author
label:t-algebra$
 16/7 Mathlib/Algebra/Group/Units/Hom.lean,Mathlib/AlgebraicGeometry/Scheme.lean,Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean,Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean,Mathlib/Geometry/RingedSpace/OpenImmersion.lean 5 6 ['alreadydone', 'erdOne', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant'] nobody
28-28301
28 days ago
28-28302
28 days ago
10-26015
10 days
23961 FR-vdash-bot
author:FR-vdash-bot
 refactor: unbundle algebra from `ENormed*` Further speed up the search in the algebraic typeclass hierarchy by avoiding searching for `TopologicalSpace`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) slow-typeclass-synthesis maintainer-merge t-algebra t-analysis merge-conflict awaiting-author
label:t-algebra$
 32/25 Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/Analysis/Normed/Group/Continuity.lean,Mathlib/Analysis/NormedSpace/IndicatorFunction.lean,Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean 5 12 ['FR-vdash-bot', 'github-actions', 'grunweg', 'jcommelin', 'leanprover-bot', 'leanprover-community-bot-assistant'] nobody
24-12519
24 days ago
24-12519
24 days ago
17-72244
17 days

All maintainer merge'd PRs

Number Author Title Description Labels +/- Modified files (first 100) 📝 💬 All users who commented or reviewed Assignee(s) Updated Last status change total time in review
25265 FMLJohn
author:FMLJohn
 feat(Order/SupClosed): `compl_image_latticeClosure` and `compl_image_latticeClosure_eq_of_compl_image_eq_self` The main results in this pull request are: 1. `compl_image_latticeClosure`: given any Boolean algebra `α` and `s : Set α`, `compl '' latticeClosure s` is the same as `latticeClosure (compl '' s)`; 2. `compl_image_latticeClosure_eq_of_compl_image_eq_self`: given any Boolean algebra `α` and `s : Set α` such that `compl '' s = s`, we have `compl '' latticeClosure s = latticeClosure s`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-order 59/1 Mathlib/Order/SupClosed.lean 1 8 ['FMLJohn', 'YaelDillies', 'github-actions'] bryangingechen
assignee:bryangingechen
25-74084
25 days ago
28-54056
28 days ago
32-63674
32 days
25089 Bergschaf
author:Bergschaf
 feat(Order/Sublocale): definition of sublocales There are several possible definition of sublocales. I used one from [nlab](https://ncatlab.org/nlab/show/sublocale) which states that a sublocale is a subset of a locale which is closed under all meets and for any ∈ S and x ∈ X, we have x ⇨ s ∈ S. This PR also includes an order isomorphism between (Nucleus)ᵒᵈ and Sublocale. --- I am open to better name suggestions for the order isomorphism. - [x] depends on: #24941 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-order 265/8 Mathlib.lean,Mathlib/Order/Hom/Lattice.lean,Mathlib/Order/Nucleus.lean,Mathlib/Order/Sublocale.lean,Mathlib/Order/Synonym.lean,docs/references.bib 6 71 ['Bergschaf', 'YaelDillies', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'xhalo32'] nobody
23-52890
23 days ago
23-52890
23 days ago
37-32312
37 days
25563 Komyyy
author:Komyyy
 chore: move `Topology.StoneCech` into `Topology.Compactification` (1/2) At present, the `Topology.Compactification` directory includes results on one-point compactifications, but results on Stone-Čech compactifications are currently located elsewhere. The removed file `Topology.Compactification` is deprecated in another PR (#25583) to leave a good git diff history. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) file-removed maintainer-merge t-topology 9/9 Mathlib.lean,Mathlib/Combinatorics/Hindman.lean,Mathlib/Topology/Category/CompHaus/Basic.lean,Mathlib/Topology/Category/CompHaus/Projective.lean,Mathlib/Topology/Category/Profinite/Projective.lean,Mathlib/Topology/Category/Stonean/Adjunctions.lean,Mathlib/Topology/Compactification/StoneCech.lean,Mathlib/Topology/ExtremallyDisconnected.lean,Mathlib/Topology/Maps/Proper/UniversallyClosed.lean,Mathlib/Topology/Separation/CompletelyRegular.lean 10 4 ['Komyyy', 'github-actions', 'grunweg'] nobody
23-7646
23 days ago
23-7646
23 days ago
23-69578
23 days
25600 Komyyy
author:Komyyy
 refactor: lemma expressing `ContinuousAt` using a punctured neighbourhood --- This lemma is used to prove that the Riemann zeta function is meromorphic in #25597. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-topology 4/0 Mathlib/Topology/ContinuousOn.lean 1 5 ['Komyyy', 'github-actions', 'grunweg'] nobody
22-44763
22 days ago
22-44763
22 days ago
22-56650
22 days
24669 qawbecrdtey
author:qawbecrdtey
 feat(Analysis/Normed/Operator/LinearIsometry): added definition `LinearIsometryEquiv.prodComm` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) This commit defines a `LinearIsometryEquiv`, and states some trivial theorems about it. ```lean def prodComm [Module R E₂] : E × E₂ ≃ₗᵢ[R] E₂ × E ``` maintainer-merge t-analysis awaiting-author 8/1 Mathlib/Analysis/Normed/Operator/LinearIsometry.lean 1 10 ['Ruben-VandeVelde', 'eric-wieser', 'faenuccio', 'github-actions', 'j-loreaux', 'jcommelin', 'qawbecrdtey'] faenuccio
assignee:faenuccio
21-20148
21 days ago
21-20148
21 days ago
32-83569
32 days
23849 chrisflav
author:chrisflav
 feat(Data/Set): add `Set.encard_iUnion` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) large-import t-data maintainer-merge 69/0 Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Data/Set/Card/Arithmetic.lean,Mathlib/Data/Set/Finite/Lattice.lean 3 25 ['YaelDillies', 'chrisflav', 'github-actions'] YaelDillies
assignee:YaelDillies
20-82611
20 days ago
20-82611
20 days ago
83-10001
83 days
25881 eric-wieser
author:eric-wieser
 chore: extract an auxiliary function from `congr()` The motivation here is to make it easier to review #25851. This code is moved (and unindented) without changes. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip maintainer-merge t-meta 72/61 Mathlib/Tactic/TermCongr.lean 1 5 ['eric-wieser', 'github-actions', 'grunweg', 'kmill'] nobody
16-46498
16 days ago
16-46498
16 days ago
0-3293
54 minutes
25172 eric-wieser
author:eric-wieser
 feat: restricting `Affine.Simplex` to an affine subspace that contains it Also removes a redundant `Nonempty` argument. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-euclidean-geometry 68/5 Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean,Mathlib/LinearAlgebra/AffineSpace/Independent.lean 2 11 ['eric-wieser', 'github-actions', 'jsm28', 'ocfnash'] nobody
4-51515
4 days ago
36-78106
1 month ago
37-32578
37 days
26405 euprunin
author:euprunin
 chore: golf using `omega` maintainer-merge 23/68 Mathlib/Algebra/Polynomial/Module/Basic.lean,Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean,Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean,Mathlib/Combinatorics/Enumerative/Composition.lean,Mathlib/Computability/DFA.lean,Mathlib/Control/Fix.lean,Mathlib/Data/Nat/Choose/Basic.lean,Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean,Mathlib/Geometry/Euclidean/Circumcenter.lean,Mathlib/GroupTheory/Coxeter/Length.lean,Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean,Mathlib/MeasureTheory/Function/ConditionalExpectation/Unique.lean,Mathlib/NumberTheory/Dioph.lean,Mathlib/Order/Partition/Equipartition.lean,Mathlib/SetTheory/Game/State.lean,Mathlib/Tactic/NormNum/LegendreSymbol.lean,Mathlib/Topology/EMetricSpace/BoundedVariation.lean 17 10 ['euprunin', 'github-actions', 'grunweg', 'leanprover-bot'] nobody
4-39067
4 days ago
4-39067
4 days ago
5-75936
5 days
26004 vasnesterov
author:vasnesterov
 feat(Algebra/Order/Floor): `⌊n * x⌋₊ / n = ⌊x⌋₊` Prove that `⌊n * x⌋₊ / n = ⌊x⌋₊` for natural `n`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-order t-algebra
label:t-algebra$
 39/9 Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean,Mathlib/Algebra/Order/Floor/Ring.lean,Mathlib/Algebra/Order/Floor/Semiring.lean,Mathlib/Data/EReal/Inv.lean 4 21 ['Ruben-VandeVelde', 'YaelDillies', 'b-mehta', 'eric-wieser', 'github-actions', 'vasnesterov'] nobody
4-12344
4 days ago
unknown
unknown
26426 Komyyy
author:Komyyy
 doc: remove `PartENat.card` in the module doc [`PartENat.card`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Deprecated/Cardinal/Finite.html#PartENat.card) is moved to the `Deprecated` directory and it's not in this file([`Mathlib.SetTheory.Cardinal.Finite`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/SetTheory/Cardinal/Finite.html)) anymore. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-set-theory maintainer-merge easy documentation 0/2 Mathlib/SetTheory/Cardinal/Finite.lean 1 2 ['github-actions', 'grunweg'] nobody
4-3984
4 days ago
4-3984
4 days ago
4-3997
4 days
26502 sgouezel
author:sgouezel
 feat: monotonicity of `lineMap` Also remove one assumption in `differentiableOn_integral_of_continuous`, and expand docstrings around this theorem. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-analysis 49/10 Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/FundThmCalculus.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/IntegrationByParts.lean,Mathlib/Topology/Algebra/ContinuousAffineMap.lean 4 6 ['eric-wieser', 'github-actions', 'grunweg', 'sgouezel'] nobody
1-80203
1 day ago
2-12994
2 days ago
2-18594
2 days
26166 joelriou
author:joelriou
 feat(AlgebraicTopology): application of the retract argument to model categories Basic consequences of the retract argument are obtained for model categories: cofibrations are exactly the morphisms that have the left lifting property with respect to trivial fibrations, etc. We deduce various properties of cofibrations, fibrations and weak equivalences in model categories (e.g. they are stable by composition). --- (I am sorry if this one is a little bit long. There are too many basic properties to state.) This PR continues the work from #20210. Original PR: https://github.com/leanprover-community/mathlib4/pull/20210 large-import maintainer-merge t-topology 450/4 Mathlib.lean,Mathlib/AlgebraicTopology/ModelCategory/Basic.lean,Mathlib/AlgebraicTopology/ModelCategory/Instances.lean 3 n/a ['github-actions', 'joelriou', 'robin-carlier'] robin-carlier
assignee:robin-carlier
1-15041
1 day ago
unknown
unknown
24361 Hagb
author:Hagb
 feat(Data/Finsupp/MonomialOrder): `0 ≤ a` where `a : m.syn` `simp` would be able to solve it. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data maintainer-merge new-contributor easy 3/0 Mathlib/Data/Finsupp/MonomialOrder.lean 1 2 ['Ruben-VandeVelde', 'github-actions'] nobody
1-8937
1 day ago
1-8937
1 day ago
67-9699
67 days
24582 pechersky
author:pechersky
 feat(GroupTheory/ArchimedeanDensely): Unique (ℤ ≃+o ℤ) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) - [x] depends on: #24580 maintainer-merge t-order t-algebra
label:t-algebra$
 44/0 Mathlib/Data/Int/Cast/Lemmas.lean,Mathlib/GroupTheory/ArchimedeanDensely.lean 2 6 ['Ruben-VandeVelde', 'eric-wieser', 'github-actions', 'mathlib4-dependent-issues-bot', 'pechersky'] nobody
1-5828
1 day ago
1-5828
1 day ago
36-80434
36 days
25758 YaelDillies
author:YaelDillies
 chore: shortcut instance `CompleteLattice α → PartialOrder α` This avoids using the path `CompleteLattice α → CompletePartialOrder α → PartialOrder α` that goes through `Order.CompletePartialOrder` and makes it appear used to our automation, such as `shake` or `#min_imports`. This is a followup to #25358. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-order 7/0 Mathlib/Order/CompleteLattice/Defs.lean 1 2 ['Ruben-VandeVelde', 'github-actions'] nobody
1-5719
1 day ago
1-5719
1 day ago
19-6207
19 days
25897 YaelDillies
author:YaelDillies
 feat: `ofNat(n) • a = ofNat(n) * a` From Toric --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) toric t-data maintainer-merge t-algebra
label:t-algebra$
 3/0 Mathlib/Data/Nat/Cast/Basic.lean 1 2 ['Ruben-VandeVelde', 'github-actions'] nobody
1-5598
1 day ago
1-5598
1 day ago
16-3108
16 days
26027 vasnesterov
author:vasnesterov
 feat(Topology): every compact metric space can be embedded into the Hilbert cube Prove `exists_closed_embedding_to_hilbert_cube`: every compact metric space can be embedded into the Hilbert cube. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-topology 58/1 Mathlib.lean,Mathlib/Topology/Compactness/HilbertCubeEmbedding.lean,Mathlib/Topology/MetricSpace/Bounded.lean 3 9 ['ADedecker', 'github-actions', 'jcommelin', 'vasnesterov'] nobody
1-2856
1 day ago
1-2856
1 day ago
13-71815
13 days
26285 kckennylau
author:kckennylau
 feat(RingTheory): resultant of two polynomials Co-authored-by: Anne Baanen --- Split from #26283. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-algebra
label:t-algebra$
 87/0 Mathlib.lean,Mathlib/RingTheory/Polynomial/Resultant/Basic.lean 2 20 ['MichaelStollBayreuth', 'YaelDillies', 'eric-wieser', 'github-actions', 'kckennylau'] nobody
0-80763
22 hours ago
0-82781
22 hours ago
8-28546
8 days
25945 adomani
author:adomani
 feat: the empty line in commands linter This linter flags empty lines within a command. It allows empty lines within doc-strings, module-docs and a couple of other "sensible" places. It also skips files that are likely to contain meta-code, since there the use of empty lines in definition is more widespread. This PR continues the work from #25236. large-import maintainer-merge 375/5 Mathlib.lean,Mathlib/CategoryTheory/Comma/StructuredArrow/CommaMap.lean,Mathlib/Init.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/EmptyLine.lean,MathlibTest/EmptyLine.lean 6 3 ['adomani', 'github-actions'] nobody
0-65499
18 hours ago
15-11716
15 days ago
15-11771
15 days
25491 tannerduve
author:tannerduve
 feat(Control/Monad/Free): define free monad, prove it lawful, and implement standard effects This PR introduces the `Free` monad. This implementation uses the "freer monad" approach as the traditional free monad (eg from [Haskell](https://hackage.haskell.org/package/free-5.2/docs/Control-Monad-Free.html)) is not safely definable in Lean due to termination checking (it's not strictly positive). The main contributions are: * Definition of the `Free` monad as an inductive type which generates a monad given any type constructor `F : Type -> Type`. * Functor and Monad instances for `Free F`, along with proofs of the `LawfulFunctor` and `LawfulMonad` laws. * Canonical instances of `Free` with standard effect signatures: * `FreeState s` for stateful computations, defined via a `StateF s` functor with `get` and `put` operations. * `FreeWriter w` for logging computations, defined via a `WriterF w` functor with a `tell` operation. * `FreeCont r` for continuation-passing computations, using the CPS functor `(α → r) → r`. In this construction, computations are represented as **trees of effects**. Each node (`liftBind`) represents a request to perform an effect, accompanied by a continuation specifying how the computation proceeds after the effect. The leaves (`pure`) represent completed computations with final results. A key insight is that `FreeM F` satisfies the **universal property of free monads**: for any monad `M` and effect handler `f : F → M`, there exists a unique way to interpret `FreeM F` computations in `M` that respects the effect semantics given by `f`. This unique interpreter is `mapM f`, which acts as the canonical **fold** for free monads. To execute or interpret these computations, we provide two approaches: 1. **Hand-written interpreters** (`FreeState.run`, `FreeWriter.run`, `FreeCont.run`) that directly pattern-match on the tree structure 2. **Canonical interpreters** (`FreeState.fold`, `FreeWriter.fold`, `FreeCont.fold`) derived from the universal property via `mapM` And then prove that these approaches are equivalent --- This PR adds new files and definitions; no breaking changes. **Tags:** free monad, freer monad, effect systems, state monad, writer monad, continuation monad, operational semantics, verified interpreters t-data maintainer-merge 717/0 Mathlib.lean,Mathlib/Control/Monad/Free.lean,MathlibTest/freemonad.lean,docs/references.bib 4 144 ['YaelDillies', 'copilot-pull-request-reviewer', 'eric-wieser', 'github-actions', 'plp127', 'quangvdao', 'tannerduve'] nobody
0-57355
15 hours ago
13-70072
13 days ago
24-2756
24 days
26543 vihdzp
author:vihdzp
 feat(SetTheory/ZFC/VonNeumann): von Neumann hierarchy of sets Ported from #17027. For extra discussion on this PR, see [Zulip](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2317027.20.2C.20.2326518.20von.20Neumann.20hierarchy/with/526389347). --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-set-theory maintainer-merge 133/0 Mathlib.lean,Mathlib/SetTheory/Ordinal/Basic.lean,Mathlib/SetTheory/ZFC/Basic.lean,Mathlib/SetTheory/ZFC/VonNeumann.lean 4 55 ['alreadydone', 'github-actions', 'kckennylau', 'vihdzp'] nobody
0-46465
12 hours ago
0-46706
12 hours ago
0-76246
21 hours
25872 101damnations
author:101damnations
 feat(RepresentationTheory/GroupCohomology): long exact sequences Given a commutative ring `k` and a group `G`, this PR shows that a short exact sequence of `k`-linear `G`-representations `0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0` induces a short exact sequence of complexes `0 ⟶ C(X₁) ⟶ C(X₂) ⟶ C(X₃) ⟶ 0`, where `C(Xᵢ)` is the complex of inhomogeneous cochains of `Xᵢ`, and hence `Hⁿ(C(Xᵢ))` is the `n`th group cohomology of `Xᵢ`. --- - [x] depends on: #25815 - [x] depends on: #25870 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) --- *This PR continues the work from #25311.* *Original PR: https://github.com/leanprover-community/mathlib4/pull/25311* maintainer-merge t-algebra
label:t-algebra$
 289/7 Mathlib.lean,Mathlib/Algebra/Homology/ConcreteCategory.lean,Mathlib/Algebra/Homology/HomologySequence.lean,Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean,Mathlib/LinearAlgebra/Pi.lean,Mathlib/RepresentationTheory/Homological/GroupCohomology/Basic.lean,Mathlib/RepresentationTheory/Homological/GroupCohomology/LongExactSequence.lean,Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean 8 9 ['101damnations', 'github-actions', 'kbuzzard', 'mathlib4-dependent-issues-bot'] nobody
0-38647
10 hours ago
1-44504
1 day ago
14-24901
14 days
26569 kim-em
author:kim-em
 feat: initial use of `@[grind]` in `Logic/Equiv` This PR begins using `grind` in `Logic/Equiv`. maintainer-merge 29/68 Mathlib/Data/Prod/PProd.lean,Mathlib/Logic/Equiv/Defs.lean,Mathlib/Logic/Equiv/Prod.lean,Mathlib/Logic/Function/Defs.lean 4 5 ['github-actions', 'grunweg', 'kim-em'] nobody
0-11193
3 hours ago
0-11193
3 hours ago
0-23910
6 hours
26566 BoltonBailey
author:BoltonBailey
 feat(Tactic/Common): register `grind` as `hint` tactic A short PR to register `grind` with the hint tactic. Reviewers, please let me know if something more involved needs to be done for this, I'm happy to work on that too if need be. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-meta 1/0 Mathlib/Tactic/Common.lean 1 2 ['github-actions', 'grunweg'] nobody
0-11160
3 hours ago
0-11160
3 hours ago
0-27511
7 hours
26572 kim-em
author:kim-em
 feat: use grind in Data/Option/NAry This PR shortens some easy proofs in `Data/Option/NAry` using `grind` (and a local `[grind cases Option]` attribute for case bashing). t-data maintainer-merge 32/37 Mathlib/Data/Option/NAry.lean 1 6 ['github-actions', 'grunweg', 'leanprover-bot'] nobody
0-9350
2 hours ago
0-11285
3 hours ago
0-23239
6 hours
26575 kim-em
author:kim-em
 feat: use grind in Data/Nat/Sqrt Not super-satisfying. There is still a lot of non-linear arithmetic in this file that we could eventually automate as well. maintainer-merge 24/43 Mathlib/Data/Nat/Sqrt.lean,Mathlib/InformationTheory/KullbackLeibler/Basic.lean 2 3 ['github-actions', 'grunweg'] nobody
0-8193
2 hours ago
0-8193
2 hours ago
0-18184
5 hours
26411 sgouezel
author:sgouezel
 feat: add `iInf` results on `ENNReal`, matching existing `iSup` ones --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data maintainer-merge 39/0 Mathlib/Data/ENNReal/Operations.lean 1 22 ['YaelDillies', 'github-actions', 'grunweg', 'sgouezel'] nobody
0-7679
2 hours ago
0-7679
2 hours ago
4-74863
4 days
26562 Ruben-VandeVelde
author:Ruben-VandeVelde
 chore: deprecate Mathlib.Algebra.Ring.Hom.Basic It was emptied in #25447. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) large-import maintainer-merge t-algebra
label:t-algebra$
 4/10 Mathlib/Algebra/Ring/Hom/Basic.lean 1 4 ['Ruben-VandeVelde', 'github-actions', 'grunweg'] nobody
0-6889
1 hour ago
0-6990
1 hour ago
0-46372
12 hours
26081 grunweg
author:grunweg
 fix/feat(migrate_to_fork.py): filter the automated summary comment as well [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Feedback.20on.20scripts.2Fmigrate_to_fork.2Epy/near/524149447) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge 2/1 scripts/migrate_to_fork.py 1 2 ['Ruben-VandeVelde', 'github-actions'] nobody
0-6119
1 hour ago
0-6119
1 hour ago
12-78038
12 days
26576 kim-em
author:kim-em
 feat: use grind in Data/Nat/Hyperoperations Some nice interactions between `grind`'s ring handling, case splitting, and instantiation. maintainer-merge 35/57 Mathlib/Algebra/Group/Even.lean,Mathlib/Data/Nat/Hyperoperation.lean 2 6 ['github-actions', 'grunweg', 'leanprover-bot'] nobody
0-5975
1 hour ago
0-8070
2 hours ago
0-12758
3 hours
25919 BoltonBailey
author:BoltonBailey
 doc: suggest !bench in `lake exe pole` This PR continues the work from #12561. Original PR: https://github.com/leanprover-community/mathlib4/pull/12561 maintainer-merge 2/1 LongestPole/Main.lean 1 3 ['BoltonBailey', 'Ruben-VandeVelde', 'github-actions'] nobody
0-5400
1 hour ago
0-5400
1 hour ago
15-67689
15 days
26570 winstonyin
author:winstonyin
 feat: version of `prod_range_induction` with weaker assumptions `prod_range_induction` currently requires ratios of adjacent terms to be checked for the entire sequence, but we only need to check terms up to `n`. I provide a parallel `prod_range_induction'` that relaxes this assumption. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-algebra
label:t-algebra$
 13/0 Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean 1 3 ['github-actions', 'grunweg'] grunweg
assignee:grunweg
0-5159
1 hour ago
0-8313
2 hours ago
0-23475
6 hours
26573 winstonyin
author:winstonyin
 chore: reorder arguments in `pathComponentIn` `pathComponentIn x F` and `connectedComponentIn F x` have opposite argument orders. I choose to reorder the arguments in `pathComponentIn` for no strong reason. Perhaps one can read, "the path component in F at x". --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-topology 24/24 Mathlib/Geometry/Manifold/ChartedSpace.lean,Mathlib/Topology/Connected/LocPathConnected.lean,Mathlib/Topology/Connected/PathConnected.lean 3 5 ['github-actions', 'grunweg', 'winstonyin'] grunweg
assignee:grunweg
0-3197
53 minutes ago
0-3197
53 minutes ago
0-3792
1 hour
26365 joelriou
author:joelriou
 feat(CategoryTheory/Localization): generalize results about adjunctions In this PR, results about adjunctions, localization of categories and calculus of fractions are slightly generalized. In particular, we show that under certain circumstances, adjoint functors are localization functors. (This shall be used in the proof of the fundamental lemma of homotopical algebra #26303.) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-category-theory 108/25 Mathlib/CategoryTheory/Localization/CalculusOfFractions/OfAdjunction.lean,Mathlib/CategoryTheory/Localization/Opposite.lean 2 7 ['github-actions', 'joelriou', 'robin-carlier'] robin-carlier
assignee:robin-carlier
0-1079
17 minutes ago
0-1291
21 minutes ago
6-66861
6 days
21751 vihdzp
author:vihdzp
 refactor(SetTheory/Ordinal/Arithmetic): rework `Ordinal.pred` API This PR does the following: - give a simpler definition of `Ordinal.pred` - replace `¬ ∃ a, o = succ a` and `∀ a, o ≠ succ a` by `IsSuccPrelimit o` throughout - improve theorem names --- There's a legitimate question of whether we even want `Ordinal.pred` (see [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Ordinal.2Epred)) but this should be a good change in the meanwhile regardless. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-set-theory maintainer-merge merge-conflict 102/67 Mathlib/SetTheory/Ordinal/Arithmetic.lean,Mathlib/SetTheory/Ordinal/Exponential.lean 2 13 ['YaelDillies', 'github-actions', 'grunweg', 'vihdzp'] nobody
55-45333
1 month ago
102-23960
3 months ago
36-50134
36 days
24965 erdOne
author:erdOne
 refactor: Make `IsLocalHom` take unbundled map --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-algebra merge-conflict awaiting-author
label:t-algebra$
 16/7 Mathlib/Algebra/Group/Units/Hom.lean,Mathlib/AlgebraicGeometry/Scheme.lean,Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean,Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean,Mathlib/Geometry/RingedSpace/OpenImmersion.lean 5 6 ['alreadydone', 'erdOne', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant'] nobody
28-28301
28 days ago
28-28302
28 days ago
10-26015
10 days
23961 FR-vdash-bot
author:FR-vdash-bot
 refactor: unbundle algebra from `ENormed*` Further speed up the search in the algebraic typeclass hierarchy by avoiding searching for `TopologicalSpace`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) slow-typeclass-synthesis maintainer-merge t-algebra t-analysis merge-conflict awaiting-author
label:t-algebra$
 32/25 Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/Analysis/Normed/Group/Continuity.lean,Mathlib/Analysis/NormedSpace/IndicatorFunction.lean,Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean 5 12 ['FR-vdash-bot', 'github-actions', 'grunweg', 'jcommelin', 'leanprover-bot', 'leanprover-community-bot-assistant'] nobody
24-12519
24 days ago
24-12519
24 days ago
17-72244
17 days

PRs blocked on a zulip discussion

Number Author Title Description Labels +/- Modified files (first 100) 📝 💬 All users who commented or reviewed Assignee(s) Updated Last status change total time in review
23866 kim-em
author:kim-em
 chore: remove `[AtLeastTwo n]` hypothesis from the `NatCast` to `OfNat` instance This PR observes that we can change ``` instance (priority := 100) instOfNatAtLeastTwo {n : ℕ} [NatCast R] [Nat.AtLeastTwo n] : OfNat R n ``` to ``` instance (priority := 100) instOfNatAtLeastTwo {n : ℕ} [NatCast R] : OfNat R n ``` with minimal fall-out. A follow-up PR #23867 then observes that we can remove nearly all the `[Nat.AtLeastTwo n]` hypotheses in Mathlib. This is slightly dangerous -- it does make it more likely that we'll generate non-defeq instances, but it appears to happen very rarely. However, it will make life slightly easier for something Leo and I are trying to do with `grind` and Grobner bases (we'd like to be able to assume types we consume have `[∀ n, OfNat α n]`, which is possible with this change, but not without...). Zulip thread: [#PR reviews > #23866 and #23867, removing most `[Nat.AtLeastTwo n]` @ 💬](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2323866.20and.20.2323867.2C.20removing.20most.20.60.5BNat.2EAtLeastTwo.20n.5D.60/near/511157297) awaiting-zulip 21/26 Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean,Mathlib/Data/Nat/Cast/Defs.lean,Mathlib/Data/Nat/Cast/Order/Basic.lean 3 3 ['eric-wieser', 'github-actions', 'urkud'] nobody
82-55963
2 months ago
82-56052
2 months ago
0-23929
6 hours
15649 TpmKranz
author:TpmKranz
 feat(Computability): introduce Generalised NFA as bridge to Regular Expression Lays the groundwork for a proof of equivalence of NFA and RE, w.r.t. described language. Actual connection to NFA comes later, after the groundwork for the opposite direction has been laid. Second chunk of #12648 --- - [x] depends on: #15647 [Data.FinEnum.Option unchanged since then] [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-computability new-contributor awaiting-author 298/0 Mathlib.lean,Mathlib/Computability/GNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/RegularExpressions.lean,docs/references.bib 5 6 ['github-actions', 'mathlib4-dependent-issues-bot', 'meithecatte', 'trivial1711'] nobody
56-43440
1 month ago
56-43449
1 month ago
23-54870
23 days
20648 anthonyde
author:anthonyde
 feat: formalize regular expression -> εNFA The file `Computability/RegularExpressionsToEpsilonNFA.lean` contains a formal definition of Thompson's method for constructing an `εNFA` from a `RegularExpression` and a proof of its correctness. --- - [x] depends on: #20644 - [x] depends on: #20645 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-computability new-contributor 490/0 Mathlib.lean,Mathlib/Computability/RegularExpressionsToEpsilonNFA.lean,docs/references.bib 3 5 ['github-actions', 'mathlib4-dependent-issues-bot', 'meithecatte', 'qawbecrdtey'] nobody
56-42751
1 month ago
56-43386
1 month ago
75-77754
75 days
17458 urkud
author:urkud
 refactor(Algebra/Group): make `IsUnit` a typeclass Also change some lemmas to assume `[IsUnit _]` instead of `[Invertible _]`. Motivated by potential non-defeq diamonds in #14986, see also [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Invertible.20and.20data) I no longer plan to merge this PR, but I'm going to cherry-pick some changes to a new PR before closing this one. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-algebra
label:t-algebra$
 82/72 Mathlib/Algebra/CharP/Invertible.lean,Mathlib/Algebra/Group/Invertible/Basic.lean,Mathlib/Algebra/Group/Units/Defs.lean,Mathlib/Algebra/GroupWithZero/Invertible.lean,Mathlib/Algebra/GroupWithZero/Units/Basic.lean,Mathlib/Algebra/Polynomial/Degree/Units.lean,Mathlib/Algebra/Polynomial/Splits.lean,Mathlib/Analysis/Convex/Segment.lean,Mathlib/Analysis/Normed/Affine/Isometry.lean,Mathlib/Analysis/Normed/Ring/Units.lean,Mathlib/CategoryTheory/Linear/Basic.lean,Mathlib/FieldTheory/Finite/Basic.lean,Mathlib/FieldTheory/Separable.lean,Mathlib/FieldTheory/SeparableDegree.lean,Mathlib/GroupTheory/Submonoid/Inverses.lean,Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean,Mathlib/LinearAlgebra/AffineSpace/Combination.lean,Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean,Mathlib/LinearAlgebra/CliffordAlgebra/Inversion.lean,Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean,Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean,Mathlib/NumberTheory/MulChar/Basic.lean,Mathlib/RingTheory/Localization/NumDen.lean,Mathlib/RingTheory/Polynomial/Content.lean,Mathlib/RingTheory/Polynomial/GaussLemma.lean,Mathlib/RingTheory/Valuation/Basic.lean 26 11 ['MichaelStollBayreuth', 'acmepjz', 'eric-wieser', 'github-actions', 'leanprover-bot', 'urkud'] nobody
43-29401
1 month ago
43-49828
1 month ago
0-66650
18 hours
20238 maemre
author:maemre
 feat(Computability/DFA): Closure of regular languages under some set operations This shows that regular languages are closed under complement and intersection by constructing DFAs for them. --- Closure under all other operations will be proved when someone adds the proof for DFA<->regular expression equivalence, so they are not part of this PR. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-computability new-contributor awaiting-author 159/0 Mathlib/Computability/DFA.lean,Mathlib/Computability/Language.lean 2 59 ['EtienneC30', 'YaelDillies', 'github-actions', 'maemre', 'meithecatte', 'urkud'] EtienneC30
assignee:EtienneC30
27-9211
27 days ago
56-43350
1 month ago
48-67492
48 days
23929 meithecatte
author:meithecatte
 feat(Computability/NFA): improve bound on pumping lemma --- - [x] depends on: #25321 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-computability new-contributor 101/10 Mathlib/Computability/EpsilonNFA.lean,Mathlib/Computability/NFA.lean 2 41 ['YaelDillies', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'meithecatte'] nobody
23-53002
23 days ago
23-53003
23 days ago
34-10595
34 days
25881 eric-wieser
author:eric-wieser
 chore: extract an auxiliary function from `congr()` The motivation here is to make it easier to review #25851. This code is moved (and unindented) without changes. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip maintainer-merge t-meta 72/61 Mathlib/Tactic/TermCongr.lean 1 5 ['eric-wieser', 'github-actions', 'grunweg', 'kmill'] nobody
16-46498
16 days ago
16-46498
16 days ago
0-3293
54 minutes
25218 kckennylau
author:kckennylau
 feat(AlgebraicGeometry): Tate normal form of elliptic curves --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip new-contributor t-algebraic-geometry 291/26 Mathlib.lean,Mathlib/AlgebraicGeometry/EllipticCurve/IsomOfJ.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Modular/TateNormalForm.lean,Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean,Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean 5 30 ['MichaelStollBayreuth', 'Multramate', 'acmepjz', 'github-actions', 'grunweg', 'kckennylau'] nobody
12-86226
12 days ago
28-84104
28 days ago
6-51040
6 days
11800 JADekker
author:JADekker
 feat : Define KappaLindelöf spaces Define KappaLindelöf spaces by following the first one-third of the API for Lindelöf spaces. The remainder will be added in a future PR. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-topology merge-conflict please-adopt 301/2 Mathlib.lean,Mathlib/Topology/Compactness/KappaLindelof.lean,Mathlib/Topology/Compactness/Lindelof.lean 3 38 ['ADedecker', 'JADekker', 'PatrickMassot', 'StevenClontz', 'adomani', 'github-actions', 'grunweg', 'kim-em', 'urkud'] nobody
288-20473
9 months ago
288-42448
9 months ago
119-10687
119 days
17518 grunweg
author:grunweg
 feat: lint on declarations mentioning `Invertible` or `Unique` Using the same infrastructure as for #10235. Depends on that PR to land first, and also (for the first lint) a zulip discussion if that change is desired/about the best way to enact it. --- - [ ] depends on: #10235 awaiting-zulip t-linter merge-conflict blocked-by-other-PR 149/7 Mathlib.lean,Mathlib/Algebra/MvPolynomial/PDeriv.lean,Mathlib/Computability/Halting.lean,Mathlib/Computability/TuringMachine.lean,Mathlib/Data/Fintype/Card.lean,Mathlib/GroupTheory/Perm/DomMulAct.lean,Mathlib/Logic/Basic.lean,Mathlib/Logic/Encodable/Basic.lean,Mathlib/NumberTheory/JacobiSum/Basic.lean,Mathlib/Order/Heyting/Regular.lean,Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/UnusedAssumptionInType.lean 13 3 ['github-actions', 'mathlib4-dependent-issues-bot', 'mergify'] nobody
240-60592
7 months ago
266-49114
8 months ago*
0-0
0 seconds*
17623 FR-vdash-bot
author:FR-vdash-bot
 feat(Algebra/Order/GroupWithZero/Unbundled): add some lemmas Some lemmas in `Algebra.Order.GroupWithZero.Unbundled` have incorrect or unsatisfactory names, or assumptions that can be omitted using `ZeroLEOneClass`. The lemmas added in this PR are versions of existing lemmas that use the correct or better name or `ZeroLEOneClass` to omit an assumption. The original lemmas will be deprecated in #17593. | New name | Old name | |-------------------------|-------------------------| | `mul_le_one_left₀` | `Left.mul_le_one_of_le_of_le` | | `mul_lt_one_of_le_of_lt_left₀` (`0 ≤ ·` version) / `mul_lt_one_of_le_of_lt_of_pos_left` | `Left.mul_lt_of_le_of_lt_one_of_pos` | | `mul_lt_one_of_lt_of_le_left₀` | `Left.mul_lt_of_lt_of_le_one_of_nonneg` | | `mul_le_one_right₀` | `Right.mul_le_one_of_le_of_le` | | `mul_lt_one_of_lt_of_le_right₀` (`0 ≤ ·` version) / `mul_lt_one_of_lt_of_le_of_pos_right` | `Right.mul_lt_one_of_lt_of_le_of_pos` | | `mul_lt_one_of_le_of_lt_right₀` | `Right.mul_lt_one_of_le_of_lt_of_nonneg` | The following lemmas use `ZeroLEOneClass`. | New name | Old name | |-------------------------|-------------------------| | `(Left.)one_le_mul₀` | `Left.one_le_mul_of_le_of_le` | | `Left.one_lt_mul_of_le_of_lt₀` | `Left.one_lt_mul_of_le_of_lt_of_pos` | | `Left.one_lt_mul_of_lt_of_le₀` | `Left.lt_mul_of_lt_of_one_le_of_nonneg` / `one_lt_mul_of_lt_of_le` (still there) | | `(Left.)one_lt_mul₀` | | | `Right.one_le_mul₀` | `Right.one_le_mul_of_le_of_le` | | `Right.one_lt_mul_of_lt_of_le₀` | `Right.one_lt_mul_of_lt_of_le_of_pos` | | `Right.one_lt_mul_of_le_of_lt₀` | `Right.one_lt_mul_of_le_of_lt_of_nonneg` / `one_lt_mul_of_le_of_lt` (still there) / `one_lt_mul` (still there) | | `Right.one_lt_mul₀` | `Right.one_lt_mul_of_lt_of_lt` | --- Split from #17593. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-order t-algebra merge-conflict
label:t-algebra$
 146/44 Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean 2 11 ['FR-vdash-bot', 'YaelDillies', 'github-actions', 'j-loreaux'] nobody
222-80123
7 months ago
222-80123
7 months ago
33-64877
33 days
8370 eric-wieser
author:eric-wieser
 refactor(Analysis/NormedSpace/Exponential): remove the `𝕂` argument from `exp` This argument is still needed for almost all the lemmas, which means it can longer be found by unification. We keep around `expSeries 𝕂 A`, as it's needed for talking about the radius of convergence over different base fields. This is a prerequisite for #8372, as we can't merge the functions until they have the same interface.\ Zulip thread: [#mathlib4 > Real.exp @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Real.2Eexp/near/401602245) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) This is started from the mathport output on https://github.com/leanprover-community/mathlib/pull/19244 awaiting-zulip t-analysis merge-conflict 432/387 Mathlib/Analysis/CStarAlgebra/Exponential.lean,Mathlib/Analysis/CStarAlgebra/Spectrum.lean,Mathlib/Analysis/Normed/Algebra/Exponential.lean,Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean,Mathlib/Analysis/Normed/Algebra/QuaternionExponential.lean,Mathlib/Analysis/Normed/Algebra/Spectrum.lean,Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean,Mathlib/Analysis/NormedSpace/DualNumber.lean,Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean,Mathlib/Analysis/SpecialFunctions/Exponential.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Series.lean 11 29 ['YaelDillies', 'eric-wieser', 'girving', 'github-actions', 'j-loreaux', 'kbuzzard', 'leanprover-community-bot-assistant', 'urkud'] nobody
67-35500
2 months ago
78-64130
2 months ago
29-60989
29 days
15654 TpmKranz
author:TpmKranz
 feat(Computability): language-preserving maps between NFA and RE Map REs to NFAs via Thompson's construction and NFAs to REs using GNFAs Last chunk of #12648 --- - [ ] depends on: #15651 - [ ] depends on: #15649 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-computability new-contributor merge-conflict blocked-by-other-PR 985/2 Mathlib.lean,Mathlib/Computability/GNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean,Mathlib/Computability/RegularExpressions.lean,Mathlib/Data/FinEnum/Option.lean,docs/references.bib 7 3 ['github-actions', 'leanprover-community-mathlib4-bot', 'meithecatte'] nobody
56-43400
1 month ago
56-43405
1 month ago
0-179
2 minutes
15651 TpmKranz
author:TpmKranz
 feat(Computability/NFA): operations for Thompson's construction Lays the groundwork for a proof of equivalence of RE and NFA, w.r.t. described language. Actual connection to REs comes later, after the groundwork for the opposite direction has been laid. Third chunk of #12648 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-computability new-contributor merge-conflict awaiting-author 307/5 Mathlib/Computability/NFA.lean 1 15 ['TpmKranz', 'YaelDillies', 'dupuisf', 'github-actions', 'leanprover-community-bot-assistant', 'meithecatte'] nobody
42-66006
1 month ago
42-66007
1 month ago
45-84611
45 days
22361 rudynicolop
author:rudynicolop
 feat(Computability/NFA): nfa closure properties Add the closure properties union, intersection and reversal for NFA. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-computability new-contributor merge-conflict awaiting-author 218/2 Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean 2 90 ['EtienneC30', 'b-mehta', 'github-actions', 'leanprover-community-bot-assistant', 'meithecatte', 'rudynicolop'] EtienneC30
assignee:EtienneC30
42-65080
1 month ago
42-65082
1 month ago
39-67601
39 days
24409 urkud
author:urkud
 chore(*): fix `nmem` vs `not_mem` names --- There are some missing/buggy deprecations, I'm going to fix them later today or tomorrow. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip tech debt merge-conflict delegated awaiting-author 317/176 Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Algebra/BigOperators/Group/Finset/Lemmas.lean,Mathlib/Algebra/Group/Indicator.lean,Mathlib/Algebra/Group/Support.lean,Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean,Mathlib/Algebra/Order/Group/Indicator.lean,Mathlib/Algebra/Polynomial/AlgebraMap.lean,Mathlib/Algebra/Polynomial/Degree/Operations.lean,Mathlib/Analysis/Calculus/BumpFunction/Basic.lean,Mathlib/Analysis/Calculus/DSlope.lean,Mathlib/Analysis/Calculus/Deriv/Basic.lean,Mathlib/Analysis/Calculus/Deriv/Support.lean,Mathlib/Analysis/Calculus/FDeriv/Basic.lean,Mathlib/Analysis/Calculus/Rademacher.lean,Mathlib/Analysis/Complex/RemovableSingularity.lean,Mathlib/Analysis/Convex/Cone/InnerDual.lean,Mathlib/Analysis/Convex/Cone/Proper.lean,Mathlib/Analysis/Convolution.lean,Mathlib/Analysis/Distribution/AEEqOfIntegralContDiff.lean,Mathlib/Data/LocallyFinsupp.lean,Mathlib/Data/Set/Basic.lean,Mathlib/Data/Set/Insert.lean,Mathlib/Dynamics/Ergodic/Conservative.lean,Mathlib/Dynamics/Ergodic/Ergodic.lean,Mathlib/Dynamics/Ergodic/Function.lean,Mathlib/Dynamics/PeriodicPts/Defs.lean,Mathlib/Geometry/Manifold/ContMDiff/Basic.lean,Mathlib/Geometry/Manifold/PartitionOfUnity.lean,Mathlib/GroupTheory/CosetCover.lean,Mathlib/LinearAlgebra/Dual/Lemmas.lean,Mathlib/LinearAlgebra/FreeModule/PID.lean,Mathlib/LinearAlgebra/PID.lean,Mathlib/LinearAlgebra/RootSystem/Base.lean,Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean,Mathlib/MeasureTheory/Function/ContinuousMapDense.lean,Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean,Mathlib/MeasureTheory/Function/L2Space.lean,Mathlib/MeasureTheory/Function/LocallyIntegrable.lean,Mathlib/MeasureTheory/Function/LpSpace/Indicator.lean,Mathlib/MeasureTheory/Integral/Average.lean,Mathlib/MeasureTheory/Integral/Bochner/Set.lean,Mathlib/MeasureTheory/Integral/Layercake.lean,Mathlib/MeasureTheory/Integral/Lebesgue/Add.lean,Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean,Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Basic.lean,Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Real.lean,Mathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean,Mathlib/MeasureTheory/Measure/AddContent.lean,Mathlib/MeasureTheory/Measure/DiracProba.lean,Mathlib/MeasureTheory/Measure/Haar/Unique.lean,Mathlib/MeasureTheory/Measure/Restrict.lean,Mathlib/MeasureTheory/Measure/WithDensity.lean,Mathlib/MeasureTheory/OuterMeasure/AE.lean,Mathlib/MeasureTheory/SetSemiring.lean,Mathlib/Order/Filter/AtTopBot/CountablyGenerated.lean,Mathlib/Order/Filter/Cocardinal.lean,Mathlib/Order/Filter/Cofinite.lean,Mathlib/Order/Filter/Tendsto.lean,Mathlib/Order/Filter/Ultrafilter/Basic.lean,Mathlib/Probability/Distributions/Uniform.lean,Mathlib/Probability/Kernel/Basic.lean,Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean,Mathlib/RingTheory/AdicCompletion/LocalRing.lean,Mathlib/RingTheory/Ideal/Maximal.lean,Mathlib/RingTheory/LaurentSeries.lean,Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean,Mathlib/RingTheory/MvPowerSeries/NoZeroDivisors.lean,Mathlib/RingTheory/Spectrum/Maximal/Localization.lean,Mathlib/RingTheory/Spectrum/Prime/RingHom.lean,Mathlib/RingTheory/Spectrum/Prime/Topology.lean,Mathlib/Topology/Algebra/InfiniteSum/Group.lean,Mathlib/Topology/Algebra/Module/Cardinality.lean,Mathlib/Topology/Algebra/Support.lean,Mathlib/Topology/Bases.lean,Mathlib/Topology/ContinuousMap/BoundedCompactlySupported.lean,Mathlib/Topology/Order/Basic.lean,Mathlib/Topology/UrysohnsLemma.lean 77 4 ['b-mehta', 'github-actions', 'jcommelin', 'leanprover-community-bot-assistant', 'mathlib-bors'] nobody
29-14578
29 days ago
29-14578
29 days ago
0-55045
15 hours
24396 JovanGerb
author:JovanGerb
 feat(Order/Defs): refactor in preparation of `to_dual` attribute When the `to_dual` attribute lands in Mathlib, we will tag many lemmas about order with this tag, which will automatically give us the dual statements. This PR prepares for this by - moving dual declarations closer together - replacing occurrences of `>` and `≥` with `<` and `≤` - consistently applying a new naming convention that helps us to name dual lemmas: we use the keywords `ge` and `gt` in place of `le` and `lt` to indicate that the same pair `a, b` in `a < b` is in the opposite order to the order in which it appeared the first time. - when we have to disambiguate the order of the argument to `<` or `≤`, we sometimes use `gt` or `ge` instead of `lt` or `le`. We also use this to get rid of many primed lemma names. This is a copy of #24376, but it doesn't remove the old lemma names, so doesn't require making changes in >500 files. deprecating these lemmas will be left to a future PR. [#mathlib4 > naming convention for ≤ and <](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/naming.20convention.20for.20.E2.89.A4.20and.20.3C) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-order merge-conflict 248/230 Mathlib/Algebra/Order/CauSeq/Basic.lean,Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean,Mathlib/Algebra/Polynomial/Degree/Domain.lean,Mathlib/Algebra/Tropical/Basic.lean,Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean,Mathlib/Computability/TuringMachine.lean,Mathlib/Data/Bool/Basic.lean,Mathlib/Data/Char.lean,Mathlib/Data/Complex/Order.lean,Mathlib/Data/ENat/Basic.lean,Mathlib/Data/Int/Order/Basic.lean,Mathlib/Data/Nat/Basic.lean,Mathlib/Data/Nat/Factorization/Defs.lean,Mathlib/Data/Nat/Find.lean,Mathlib/Data/Nat/PartENat.lean,Mathlib/Data/Num/Lemmas.lean,Mathlib/Data/Num/ZNum.lean,Mathlib/Data/PSigma/Order.lean,Mathlib/Data/Prod/Lex.lean,Mathlib/Data/Real/Basic.lean,Mathlib/Data/Setoid/Basic.lean,Mathlib/Data/Setoid/Partition.lean,Mathlib/Data/Sigma/Order.lean,Mathlib/Data/String/Basic.lean,Mathlib/Data/Sum/Order.lean,Mathlib/GroupTheory/MonoidLocalization/Order.lean,Mathlib/NumberTheory/Zsqrtd/Basic.lean,Mathlib/Order/Antisymmetrization.lean,Mathlib/Order/Basic.lean,Mathlib/Order/Booleanisation.lean,Mathlib/Order/Defs/LinearOrder.lean,Mathlib/Order/Defs/PartialOrder.lean,Mathlib/Order/RelClasses.lean,Mathlib/Order/WithBot.lean,Mathlib/Probability/Martingale/Upcrossing.lean,Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicity.lean,Mathlib/SetTheory/Game/Basic.lean,Mathlib/SetTheory/Ordinal/Basic.lean,Mathlib/SetTheory/Ordinal/Notation.lean,Mathlib/SetTheory/Surreal/Basic.lean,Mathlib/Tactic/Linarith/Frontend.lean,MathlibTest/linarith.lean 43 5 ['JovanGerb', 'bryangingechen', 'github-actions', 'leanprover-community-bot-assistant'] bryangingechen
assignee:bryangingechen
28-63080
28 days ago
28-63082
28 days ago
5-75236
5 days

PRs on the review queue labelled 'tech debt' or 'longest-pole'

Number Author Title Description Labels +/- Modified files (first 100) 📝 💬 All users who commented or reviewed Assignee(s) Updated Last status change total time in review
22603 pechersky
author:pechersky
 chore(Topology): rename pi family from π to X Only in files that mentioned such a family, via a script: ``` git grep -e "π : . → Type" --name-only | rg Topology | xargs -I{} sed -i -e 's/π/X/g' {} ``` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) tech debt t-topology 238/238 Mathlib/Topology/AlexandrovDiscrete.lean,Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean,Mathlib/Topology/Algebra/Module/Equiv.lean,Mathlib/Topology/Algebra/Order/LiminfLimsup.lean,Mathlib/Topology/Bases.lean,Mathlib/Topology/Bornology/Constructions.lean,Mathlib/Topology/Connected/Basic.lean,Mathlib/Topology/Connected/Clopen.lean,Mathlib/Topology/Connected/LocallyConnected.lean,Mathlib/Topology/Connected/TotallyDisconnected.lean,Mathlib/Topology/Constructions.lean,Mathlib/Topology/ContinuousOn.lean,Mathlib/Topology/EMetricSpace/Diam.lean,Mathlib/Topology/EMetricSpace/Pi.lean,Mathlib/Topology/ExtremallyDisconnected.lean,Mathlib/Topology/Inseparable.lean,Mathlib/Topology/MetricSpace/Basic.lean,Mathlib/Topology/MetricSpace/Infsep.lean,Mathlib/Topology/MetricSpace/ProperSpace.lean,Mathlib/Topology/MetricSpace/Pseudo/Pi.lean,Mathlib/Topology/Metrizable/Basic.lean,Mathlib/Topology/Order/Basic.lean,Mathlib/Topology/Separation/Hausdorff.lean,Mathlib/Topology/UniformSpace/Ascoli.lean 24 1 ['github-actions'] nobody
22-31809
22 days ago
22-31831
22 days ago
28-25445
28 days
25776 Parcly-Taxel
author:Parcly-Taxel
 chore: deprime `induction` in `Analysis` I think this is very marginally dependent on #25770. tech debt t-analysis 256/208 Mathlib/Analysis/Analytic/Composition.lean,Mathlib/Analysis/Analytic/Constructions.lean,Mathlib/Analysis/Analytic/Inverse.lean,Mathlib/Analysis/BoxIntegral/Basic.lean,Mathlib/Analysis/BoxIntegral/Box/SubboxInduction.lean,Mathlib/Analysis/BoxIntegral/Partition/Additive.lean,Mathlib/Analysis/BoxIntegral/Partition/Split.lean,Mathlib/Analysis/CStarAlgebra/Basic.lean,Mathlib/Analysis/CStarAlgebra/Multiplier.lean,Mathlib/Analysis/Calculus/ContDiff/Basic.lean,Mathlib/Analysis/Calculus/ContDiff/Bounds.lean,Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean,Mathlib/Analysis/Calculus/ContDiff/Operations.lean,Mathlib/Analysis/Calculus/Deriv/ZPow.lean,Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean,Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean,Mathlib/Analysis/Calculus/SmoothSeries.lean,Mathlib/Analysis/Convex/Combination.lean,Mathlib/Analysis/Convex/Radon.lean,Mathlib/Analysis/InnerProductSpace/Projection.lean,Mathlib/Analysis/Normed/Algebra/Exponential.lean,Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean,Mathlib/Analysis/Seminorm.lean,Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean,Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean,Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Deriv.lean,Mathlib/Analysis/SpecialFunctions/Integrals.lean,Mathlib/Analysis/SpecialFunctions/Log/Basic.lean,Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean,Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean,Mathlib/Analysis/SpecialFunctions/Pow/Real.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean 35 2 ['Parcly-Taxel', 'github-actions'] nobody
19-2134
19 days ago
19-2567
19 days ago
19-2611
19 days
25790 Parcly-Taxel
author:Parcly-Taxel
 chore: remove >6 month old material in `Deprecated` file-removed tech debt 0/250 Mathlib.lean,Mathlib/Deprecated/Cardinal/Continuum.lean,Mathlib/Deprecated/Cardinal/Finite.lean,Mathlib/Deprecated/Cardinal/PartENat.lean,Mathlib/Deprecated/Order.lean 5 1 ['github-actions'] nobody
19-810
19 days ago
19-909
19 days ago
19-897
19 days
25774 Parcly-Taxel
author:Parcly-Taxel
 chore: deprime `induction` in `AlgebraicTopology/CategoryTheory` Most replacements that are also in #23676 have been copied over, but some have been optimised further. tech debt 133/124 Mathlib/AlgebraicTopology/DoldKan/Decomposition.lean,Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean,Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean,Mathlib/AlgebraicTopology/DoldKan/Projections.lean,Mathlib/AlgebraicTopology/SimplexCategory/MorphismProperty.lean,Mathlib/AlgebraicTopology/SimplicialObject/Split.lean,Mathlib/AlgebraicTopology/SimplicialSet/Degenerate.lean,Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean,Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean,Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean,Mathlib/CategoryTheory/Abelian/GrothendieckCategory/Subobject.lean,Mathlib/CategoryTheory/Action/Concrete.lean,Mathlib/CategoryTheory/Action/Monoidal.lean,Mathlib/CategoryTheory/ComposableArrows.lean,Mathlib/CategoryTheory/Extensive.lean,Mathlib/CategoryTheory/Filtered/Basic.lean,Mathlib/CategoryTheory/Galois/Decomposition.lean,Mathlib/CategoryTheory/Galois/EssSurj.lean,Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean,Mathlib/CategoryTheory/Limits/Shapes/SequentialProduct.lean,Mathlib/CategoryTheory/Limits/Types/Colimits.lean,Mathlib/CategoryTheory/Limits/VanKampen.lean,Mathlib/CategoryTheory/Quotient.lean,Mathlib/CategoryTheory/Sites/Sheaf.lean,Mathlib/CategoryTheory/Subobject/Basic.lean,Mathlib/CategoryTheory/Subobject/FactorThru.lean,Mathlib/CategoryTheory/Subobject/Lattice.lean,Mathlib/CategoryTheory/Triangulated/TStructure/Basic.lean 28 3 ['Parcly-Taxel', 'eric-wieser', 'github-actions'] nobody
18-75179
18 days ago
19-3016
19 days ago
19-3001
19 days
25770 Parcly-Taxel
author:Parcly-Taxel
 chore: fix more induction/recursor branch names These were found using the regex `\| h. =>` and `def.*rec.*\(h. :`. tech debt 134/115 Mathlib/Analysis/Convolution.lean,Mathlib/Data/ENat/Basic.lean,Mathlib/Data/Fin/Tuple/Basic.lean,Mathlib/Data/Fin/Tuple/NatAntidiagonal.lean,Mathlib/Data/Nat/Factorization/Induction.lean,Mathlib/Data/Seq/Computation.lean,Mathlib/Data/Set/Card.lean,Mathlib/Data/WSeq/Basic.lean,Mathlib/FieldTheory/KummerExtension.lean,Mathlib/Logic/Function/Iterate.lean,Mathlib/NumberTheory/ArithmeticFunction.lean,Mathlib/NumberTheory/SumFourSquares.lean,Mathlib/NumberTheory/SumTwoSquares.lean,Mathlib/Order/SuccPred/Archimedean.lean,Mathlib/Order/Synonym.lean 15 10 ['Parcly-Taxel', 'eric-wieser', 'github-actions'] nobody
16-9995
16 days ago
19-4841
19 days ago
19-4826
19 days
25915 BoltonBailey
author:BoltonBailey
 chore(Algebra/Squarefree/Basic): fix erw This PR addresses an instance of the erw linter in Algebra/Squarefree/Basic. Original PR: https://github.com/leanprover-community/mathlib4/pull/25161 tech debt t-algebra easy
label:t-algebra$
 1/1 Mathlib/Algebra/Squarefree/Basic.lean 1 1 ['github-actions'] nobody
4-28312
4 days ago
8-50234
8 days ago
15-68298
15 days
26404 grunweg
author:grunweg
 chore: clean up and remove FunProp/Differentiable - one lemma in that file already exists, hence can be removed (We don't add a deprecation as I presume people will not have used it.) - move the three remaining lemmas in that file to their proper place, and use the now `fun_` naming convention (Omitting deprecations again.) - after this, `FunProp/Differentiable` is empty and need not be imported any more: add a module deprecation --- - [x] depends on: #26355 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) tech debt 23/49 Mathlib/Analysis/Calculus/FDeriv/Comp.lean,Mathlib/Tactic/FunProp/ContDiff.lean,Mathlib/Tactic/FunProp/Differentiable.lean,MathlibTest/fun_prop2.lean 4 3 ['github-actions', 'grunweg', 'mathlib4-dependent-issues-bot'] nobody
0-39614
11 hours ago
5-65380
5 days ago
5-65425
5 days