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: April 19, 2025 at 20:09 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
23988 RemyDegenne
author:RemyDegenne
 feat(MeasureTheory): `tendsto_iff_forall_integral_rclike_tendsto` Add variants of `tendsto_iff_forall_integral_tendsto` for finite measures and probability measures, where the integral is over functions with value in an RCLike type instead of Real. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-measure-probability ready-to-merge 52/0 Mathlib/Analysis/Complex/Basic.lean,Mathlib/Analysis/RCLike/Basic.lean,Mathlib/MeasureTheory/Measure/FiniteMeasure.lean,Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean 4 2 ['github-actions', 'sgouezel'] nobody
2-35779
2 days ago
2-36484
2 days ago
4-9076
4 days

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
23111 pechersky
author:pechersky
 feat(Topology/MetricSpace): pseudometrics as bundled functions Preparation for results using families of pseudometrics --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-topology 211/0 Mathlib.lean,Mathlib/Topology/MetricSpace/BundledFun.lean 2 35 ['YaelDillies', 'github-actions', 'pechersky', 'plp127'] nobody
29-24676
29 days ago
29-25838
29 days ago
30-64788
30 days
17802 vihdzp
author:vihdzp
 feat(SetTheory/Ordinal/Veblen): epsilon and gamma ordinals We define the epsilon function `ε_ o = veblen 1 o`, and the gamma function `Γ_ o` which enumerates the fixed points of `veblen · 0`. --- - [x] depends on: #17751 - [x] depends on: #18611 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-set-theory maintainer-merge 146/7 Mathlib/SetTheory/Ordinal/FixedPoint.lean,Mathlib/SetTheory/Ordinal/Veblen.lean 2 15 ['YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'vihdzp'] nobody
16-66354
16 days ago
16-66354
16 days ago
48-78740
48 days
21624 sinhp
author:sinhp
 feat(CategoryTheory): The (closed) monoidal structure on the product category of families of (closed) monoidal categories Given a family of closed monoidal categories, we show that the product of these categories is a closed monoidal category with the pointwise monoidal structure. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-category-theory awaiting-author 144/0 Mathlib.lean,Mathlib/CategoryTheory/Pi/Basic.lean,Mathlib/CategoryTheory/Pi/Monoidal.lean,Mathlib/CategoryTheory/Pi/MonoidalClosed.lean 4 19 ['TwoFX', 'YaelDillies', 'b-mehta', 'github-actions', 'jcommelin', 'sinhp'] nobody
11-40455
11 days ago
11-59288
11 days ago
54-54882
54 days
21539 Raph-DG
author:Raph-DG
 feat(LinearAlgebra): Symmetric Algebra Defined the universal property for the symmetric algebra of a module over a commutative ring, provided an explicit construction and proved that this satisfies the universal property. Also proved that the multivariate polynomial ring generated by a basis of a module satisfies the universal property of the symmetric algebra of that module. Co-authored-by: Zhixuan Dai <22300180006@m.fudan.edu.cn> Co-authored-by: Zhenyan Fu Co-authored-by: Yiming Fu Co-authored-by: Wang Jingting --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge new-contributor t-algebra
label:t-algebra$
 223/0 Mathlib.lean,Mathlib/Algebra/Symmetrized.lean,Mathlib/LinearAlgebra/SymmetricAlgebra/Basic.lean,Mathlib/LinearAlgebra/SymmetricAlgebra/MvPolynomial.lean 4 47 ['ADedecker', 'Raph-DG', 'YaelDillies', 'eric-wieser', 'github-actions', 'xyzw12345'] nobody
10-70482
10 days ago
11-42316
11 days ago
67-13911
67 days
22823 b-reinke
author:b-reinke
 feat(Algebra/Ring): associator of a non-associative ring If `R` is a non-associative ring, then `(x * y) * z - x * (y * z)` is called the `associator` of ring elements `x y z : R`. The associator vanishes exactly when `R` is associative. We prove variants of this statement also for the `AddMonoidHom` bundled version of the associator, as well as the bundled version of `mulLeft₃` and `mulRight₃`, the multiplications `(x * y) * z` and `x * (y * z)`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) large-import maintainer-merge new-contributor t-algebra
label:t-algebra$
 133/8 Mathlib.lean,Mathlib/Algebra/DirectSum/Ring.lean,Mathlib/Algebra/Ring/Associator.lean 3 46 ['Paul-Lez', 'YaelDillies', 'b-reinke', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant'] nobody
9-30228
9 days ago
9-37765
9 days ago
33-12713
33 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
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 8 ['FR-vdash-bot', 'github-actions', 'grunweg', 'leanprover-bot'] nobody
7-42433
7 days ago
7-42434
7 days ago
8-278
8 days
24069 jcommelin
author:jcommelin
 doc(Topology/CWComplex): cross-reference abstract and classical approaches * Add implementation notes to both Abstract/Basic.lean and Classical/Basic.lean explaining the relationship between the two approaches to CW complexes * Add TODO noting the missing connection between the approaches * Clarify that Abstract/Basic.lean uses a categorical approach while Classical/Basic.lean uses Whitehead's classical approach --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-topology 23/2 Mathlib/Topology/CWComplex/Abstract/Basic.lean,Mathlib/Topology/CWComplex/Classical/Basic.lean 2 3 ['github-actions', 'grunweg'] nobody
4-39623
4 days ago
4-39624
4 days ago
4-44596
4 days
23722 YaelDillies
author:YaelDillies
 feat(Bialgebra/MonoidAlgebra): `mapDomain` as a `BialgHom` From Toric Co-authored-by: Michał Mrugała --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) toric maintainer-merge t-algebra
label:t-algebra$
 64/16 Mathlib/RingTheory/Bialgebra/Hom.lean,Mathlib/RingTheory/Bialgebra/MonoidAlgebra.lean 2 9 ['YaelDillies', 'erdOne', 'eric-wieser', 'github-actions'] nobody
4-17624
4 days ago
4-36528
4 days ago
13-36855
13 days
22576 Ruben-VandeVelde
author:Ruben-VandeVelde
 feat: more lemmas about alternatingGroup --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) cc @AntoineChambert-Loir (whose code this is) maintainer-merge t-algebra
label:t-algebra$
 55/0 Mathlib/GroupTheory/SpecificGroups/Alternating/Centralizer.lean 1 4 ['b-mehta', 'github-actions'] nobody
2-7159
2 days ago
2-9950
2 days ago
45-76763
45 days
23018 gio256
author:gio256
 feat: subscript and superscript delaborators We add the functions `delabSubscript` and `delabSuperscript` in the `Mathlib.Tactic` namespace. These delaborators are triggered only if the entirety of the provided expression can be subscripted (respectively, superscripted). The delaborators are not exhaustive, in that they will not successfully delaborate every expression that is valid in a subscript or superscript. We instead aim to make them overly conservative, so that any expression which is successfully delaborated must be subscriptable (or superscriptable). --- This PR is intended to serve as a predecessor to #20719. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) infinity-cosmos maintainer-merge t-meta 206/10 Mathlib/Util/Superscript.lean,MathlibTest/superscript.lean 2 36 ['eric-wieser', 'gio256', 'github-actions', 'joneugster'] nobody
2-4189
2 days ago
2-5399
2 days ago
31-7356
31 days
23530 YaelDillies
author:YaelDillies
 feat(.devcontainer): use prebuilt Docker image ... instead of building it every time we open a codespace. This makes opening a codespace much faster. The image can be found here: https://hub.docker.com/r/leanprovercommunity/gitpod4. I am the one maintaining it. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge CI 1/3 .devcontainer/devcontainer.json 1 3 ['github-actions', 'joneugster'] nobody
1-80523
1 day ago
1-80523
1 day ago
18-36235
18 days
23542 kbuzzard
author:kbuzzard
 chore(RingTheory/DedekindDomain/FiniteAdeleRing): refactor finite adeles Now we have a general theory of restricted products, we can refactor mathlib's finite adele file, removing the auxiliary results which are unused outside this file and replacing everything with much slicker proofs. Crucially, we also have a far more conceptual definition of the topology on the finite adele ring -- this is the big win. The motivation for this refactor is that the FLT project needs many more results about finite adeles (for example local compactness in the number field case) and this will be very easy to prove with this new definition (using `RestrictedProduct.locallyCompactSpace_of_addGroup`), whereas it took an entire project https://github.com/smmercuri/adele-ring_locally-compact with our current approach. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) The diff should not be taken too seriously: the file is rewritten from scratch and is a quarter the size. I have no idea what to do about deprecations here. I have removed several results (and two definitions) because we don't want them, they were just auxiliary results needed in the old proof of `IsTopologicalRing` and were not used anywhere else; after Anatole's complete rethink of the topology he gets this result for free so my proposal pretty clearly is just to nuke the old results and constructions, while keeping the key constructions (namely the structure of topological ring). The key deletions are `FiniteIntegralAdeles` (which we can still have as `∀ v : HeightOneSpectrum R, v.adicCompletionIntegers K`) and `ProdAdicCompletions` (an auxiliary construction, which we can still have as `∀ v : HeightOneSpectrum R, v.adicCompletion K`). These auxiliary definitions were also used a little in the FLT project; https://github.com/ImperialCollegeLondon/FLT/pull/399 is the accompanying PR which is waiting on this. maintainer-merge t-algebra t-number-theory
label:t-algebra$
 79/409 Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean,Mathlib/Topology/Algebra/RestrictedProduct.lean 2 21 ['ADedecker', 'Ruben-VandeVelde', 'github-actions', 'kbuzzard', 'loefflerd', 'mariainesdff', 'smmercuri'] nobody
1-19167
1 day ago
1-19168
1 day ago
18-24669
18 days
19315 quangvdao
author:quangvdao
 feat(Data/Finsupp/Fin): Add `Finsupp` operations on `Fin` tuple This PR adds more analogues of operations on `Fin` tuples to the `Finsupp` setting. Before, there were only `Finsupp.cons` and `Finsupp.tail`. Now there are also `Finsupp.snoc`, `Finsupp.insertNth`, `Finsupp.init`, and `Finsupp.removeNth`. These all come with supporting lemmas. I also removed the porting comment about `succAboveCases` in `Data/Fin/Basic`, and added a lemma about `succAbove` in `Data/Fin/Tuple/Basic`. --- - [x] depends on: #20361 - [x] depends on: #20771 - [x] depends on: #20770 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data maintainer-merge merge-conflict awaiting-author 193/16 Mathlib/Algebra/BigOperators/Fin.lean,Mathlib/Algebra/BigOperators/Finsupp.lean,Mathlib/Algebra/MvPolynomial/Equiv.lean,Mathlib/Data/Finsupp/Fin.lean,Mathlib/RingTheory/MvPolynomial/Homogeneous.lean,scripts/nolints_prime_decls.txt 6 44 ['YaelDillies', 'github-actions', 'j-loreaux', 'kbuzzard', 'mathlib4-dependent-issues-bot', 'quangvdao'] nobody
40-7030
1 month ago
40-7030
1 month ago
43-81255
43 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 12 ['YaelDillies', 'github-actions', 'vihdzp'] nobody
29-58563
29 days ago
29-58563
29 days ago
36-50134
36 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
23111 pechersky
author:pechersky
 feat(Topology/MetricSpace): pseudometrics as bundled functions Preparation for results using families of pseudometrics --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-topology 211/0 Mathlib.lean,Mathlib/Topology/MetricSpace/BundledFun.lean 2 35 ['YaelDillies', 'github-actions', 'pechersky', 'plp127'] nobody
29-24676
29 days ago
29-25838
29 days ago
30-64788
30 days
17802 vihdzp
author:vihdzp
 feat(SetTheory/Ordinal/Veblen): epsilon and gamma ordinals We define the epsilon function `ε_ o = veblen 1 o`, and the gamma function `Γ_ o` which enumerates the fixed points of `veblen · 0`. --- - [x] depends on: #17751 - [x] depends on: #18611 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-set-theory maintainer-merge 146/7 Mathlib/SetTheory/Ordinal/FixedPoint.lean,Mathlib/SetTheory/Ordinal/Veblen.lean 2 15 ['YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'vihdzp'] nobody
16-66354
16 days ago
16-66354
16 days ago
48-78740
48 days
21624 sinhp
author:sinhp
 feat(CategoryTheory): The (closed) monoidal structure on the product category of families of (closed) monoidal categories Given a family of closed monoidal categories, we show that the product of these categories is a closed monoidal category with the pointwise monoidal structure. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-category-theory awaiting-author 144/0 Mathlib.lean,Mathlib/CategoryTheory/Pi/Basic.lean,Mathlib/CategoryTheory/Pi/Monoidal.lean,Mathlib/CategoryTheory/Pi/MonoidalClosed.lean 4 19 ['TwoFX', 'YaelDillies', 'b-mehta', 'github-actions', 'jcommelin', 'sinhp'] nobody
11-40455
11 days ago
11-59288
11 days ago
54-54882
54 days
21539 Raph-DG
author:Raph-DG
 feat(LinearAlgebra): Symmetric Algebra Defined the universal property for the symmetric algebra of a module over a commutative ring, provided an explicit construction and proved that this satisfies the universal property. Also proved that the multivariate polynomial ring generated by a basis of a module satisfies the universal property of the symmetric algebra of that module. Co-authored-by: Zhixuan Dai <22300180006@m.fudan.edu.cn> Co-authored-by: Zhenyan Fu Co-authored-by: Yiming Fu Co-authored-by: Wang Jingting --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge new-contributor t-algebra
label:t-algebra$
 223/0 Mathlib.lean,Mathlib/Algebra/Symmetrized.lean,Mathlib/LinearAlgebra/SymmetricAlgebra/Basic.lean,Mathlib/LinearAlgebra/SymmetricAlgebra/MvPolynomial.lean 4 47 ['ADedecker', 'Raph-DG', 'YaelDillies', 'eric-wieser', 'github-actions', 'xyzw12345'] nobody
10-70482
10 days ago
11-42316
11 days ago
67-13911
67 days
22823 b-reinke
author:b-reinke
 feat(Algebra/Ring): associator of a non-associative ring If `R` is a non-associative ring, then `(x * y) * z - x * (y * z)` is called the `associator` of ring elements `x y z : R`. The associator vanishes exactly when `R` is associative. We prove variants of this statement also for the `AddMonoidHom` bundled version of the associator, as well as the bundled version of `mulLeft₃` and `mulRight₃`, the multiplications `(x * y) * z` and `x * (y * z)`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) large-import maintainer-merge new-contributor t-algebra
label:t-algebra$
 133/8 Mathlib.lean,Mathlib/Algebra/DirectSum/Ring.lean,Mathlib/Algebra/Ring/Associator.lean 3 46 ['Paul-Lez', 'YaelDillies', 'b-reinke', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant'] nobody
9-30228
9 days ago
9-37765
9 days ago
33-12713
33 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
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 8 ['FR-vdash-bot', 'github-actions', 'grunweg', 'leanprover-bot'] nobody
7-42433
7 days ago
7-42434
7 days ago
8-278
8 days
24069 jcommelin
author:jcommelin
 doc(Topology/CWComplex): cross-reference abstract and classical approaches * Add implementation notes to both Abstract/Basic.lean and Classical/Basic.lean explaining the relationship between the two approaches to CW complexes * Add TODO noting the missing connection between the approaches * Clarify that Abstract/Basic.lean uses a categorical approach while Classical/Basic.lean uses Whitehead's classical approach --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-topology 23/2 Mathlib/Topology/CWComplex/Abstract/Basic.lean,Mathlib/Topology/CWComplex/Classical/Basic.lean 2 3 ['github-actions', 'grunweg'] nobody
4-39623
4 days ago
4-39624
4 days ago
4-44596
4 days
23722 YaelDillies
author:YaelDillies
 feat(Bialgebra/MonoidAlgebra): `mapDomain` as a `BialgHom` From Toric Co-authored-by: Michał Mrugała --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) toric maintainer-merge t-algebra
label:t-algebra$
 64/16 Mathlib/RingTheory/Bialgebra/Hom.lean,Mathlib/RingTheory/Bialgebra/MonoidAlgebra.lean 2 9 ['YaelDillies', 'erdOne', 'eric-wieser', 'github-actions'] nobody
4-17624
4 days ago
4-36528
4 days ago
13-36855
13 days
22576 Ruben-VandeVelde
author:Ruben-VandeVelde
 feat: more lemmas about alternatingGroup --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) cc @AntoineChambert-Loir (whose code this is) maintainer-merge t-algebra
label:t-algebra$
 55/0 Mathlib/GroupTheory/SpecificGroups/Alternating/Centralizer.lean 1 4 ['b-mehta', 'github-actions'] nobody
2-7159
2 days ago
2-9950
2 days ago
45-76763
45 days
23018 gio256
author:gio256
 feat: subscript and superscript delaborators We add the functions `delabSubscript` and `delabSuperscript` in the `Mathlib.Tactic` namespace. These delaborators are triggered only if the entirety of the provided expression can be subscripted (respectively, superscripted). The delaborators are not exhaustive, in that they will not successfully delaborate every expression that is valid in a subscript or superscript. We instead aim to make them overly conservative, so that any expression which is successfully delaborated must be subscriptable (or superscriptable). --- This PR is intended to serve as a predecessor to #20719. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) infinity-cosmos maintainer-merge t-meta 206/10 Mathlib/Util/Superscript.lean,MathlibTest/superscript.lean 2 36 ['eric-wieser', 'gio256', 'github-actions', 'joneugster'] nobody
2-4189
2 days ago
2-5399
2 days ago
31-7356
31 days
23530 YaelDillies
author:YaelDillies
 feat(.devcontainer): use prebuilt Docker image ... instead of building it every time we open a codespace. This makes opening a codespace much faster. The image can be found here: https://hub.docker.com/r/leanprovercommunity/gitpod4. I am the one maintaining it. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge CI 1/3 .devcontainer/devcontainer.json 1 3 ['github-actions', 'joneugster'] nobody
1-80523
1 day ago
1-80523
1 day ago
18-36235
18 days
23542 kbuzzard
author:kbuzzard
 chore(RingTheory/DedekindDomain/FiniteAdeleRing): refactor finite adeles Now we have a general theory of restricted products, we can refactor mathlib's finite adele file, removing the auxiliary results which are unused outside this file and replacing everything with much slicker proofs. Crucially, we also have a far more conceptual definition of the topology on the finite adele ring -- this is the big win. The motivation for this refactor is that the FLT project needs many more results about finite adeles (for example local compactness in the number field case) and this will be very easy to prove with this new definition (using `RestrictedProduct.locallyCompactSpace_of_addGroup`), whereas it took an entire project https://github.com/smmercuri/adele-ring_locally-compact with our current approach. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) The diff should not be taken too seriously: the file is rewritten from scratch and is a quarter the size. I have no idea what to do about deprecations here. I have removed several results (and two definitions) because we don't want them, they were just auxiliary results needed in the old proof of `IsTopologicalRing` and were not used anywhere else; after Anatole's complete rethink of the topology he gets this result for free so my proposal pretty clearly is just to nuke the old results and constructions, while keeping the key constructions (namely the structure of topological ring). The key deletions are `FiniteIntegralAdeles` (which we can still have as `∀ v : HeightOneSpectrum R, v.adicCompletionIntegers K`) and `ProdAdicCompletions` (an auxiliary construction, which we can still have as `∀ v : HeightOneSpectrum R, v.adicCompletion K`). These auxiliary definitions were also used a little in the FLT project; https://github.com/ImperialCollegeLondon/FLT/pull/399 is the accompanying PR which is waiting on this. maintainer-merge t-algebra t-number-theory
label:t-algebra$
 79/409 Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean,Mathlib/Topology/Algebra/RestrictedProduct.lean 2 21 ['ADedecker', 'Ruben-VandeVelde', 'github-actions', 'kbuzzard', 'loefflerd', 'mariainesdff', 'smmercuri'] nobody
1-19167
1 day ago
1-19168
1 day ago
18-24669
18 days
23972 Paul-Lez
author:Paul-Lez
 feat(CategoryTheory/Monoidal/Mod_): add a class version of modules over monoid objects From Toric --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) toric maintainer-merge t-category-theory 73/3 Mathlib.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/Mod_.lean,Mathlib/CategoryTheory/Monoidal/Mod_.lean 3 25 ['Paul-Lez', 'YaelDillies', 'erdOne', 'github-actions'] nobody
0-80939
22 hours ago
1-75413
1 day ago
4-7398
4 days
22119 pimotte
author:pimotte
 feat(Combinatorics/SimpleGraph): part of Tutte's theorem Adds three key parts of the proof of Tutte's theorem, with some supporting lemma's: - necessity of the Tutte condition (`not_isTutteViolator`) - the fact that the empty set violates the Tutte condition if the number of vertices is odd (`IsTutteViolator.empty`) - the construction of a perfect matching in a graph that decomposes into cliques (`Subgraph.IsPerfectMatching.exists_of_isClique_supp`) Definitions added: `IsTutteViolator`. --- - [x] depends on: #22125 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) [Zulip thread on Tutte's](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Tutte's.20theorem) maintainer-merge t-combinatorics 195/11 Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/Represents.lean,Mathlib/Combinatorics/SimpleGraph/Matching.lean,Mathlib/Combinatorics/SimpleGraph/Tutte.lean,Mathlib/Combinatorics/SimpleGraph/UniversalVerts.lean,Mathlib/Data/Set/Card.lean 6 47 ['YaelDillies', 'b-mehta', 'github-actions', 'mathlib4-dependent-issues-bot', 'pimotte'] nobody
0-80277
22 hours ago
1-29042
1 day ago
23-70804
23 days
24185 urkud
author:urkud
 feat(Prod/Lex): prove `Prod.Lex.covBy_iff` Also - move the definitions of `CovBy` and `WCovBy` to `Defs/PartialOrder`; - rename instances to use `inst*`; - golf a proof using `aesop`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-order 77/66 Mathlib/Algebra/Module/LinearMap/Defs.lean,Mathlib/Algebra/Module/Submodule/Map.lean,Mathlib/Data/Fin/FlagRange.lean,Mathlib/Data/Prod/Lex.lean,Mathlib/Order/Cover.lean,Mathlib/Order/Defs/PartialOrder.lean 6 5 ['YaelDillies', 'github-actions'] nobody
0-67271
18 hours ago
0-67271
18 hours ago
0-71595
19 hours
23299 DavidLedvinka
author:DavidLedvinka
 feat(Analysis): add `mlconvolution` and `lconvolution`, Convolution with the Lebesgue integral Create LConvolution.lean which defines convolution using the Lebesgue integral. I plan to add more API but wanted to make sure the definition/notation are satisfactory. The main intended application of this is to prove that the pdf of a product (sum) of independent random variables is given by the convolution of their pdfs. maintainer-merge new-contributor t-measure-probability t-analysis 125/43 Mathlib.lean,Mathlib/Analysis/LConvolution.lean,Mathlib/MeasureTheory/Group/Convolution.lean,Mathlib/Tactic/ToAdditive/Frontend.lean 4 38 ['DavidLedvinka', 'EtienneC30', 'github-actions', 'leanprover-community-bot-assistant', 'urkud'] EtienneC30
assignee:EtienneC30
0-26259
7 hours ago
0-26889
7 hours ago
24-58289
24 days
23539 alreadydone
author:alreadydone
 feat(Algebra): transcendence degree is well-defined In **AlgebraicIndependent/TranscendenceBasis.lean**, we show: + The AlgebraicIndependent sets in a domain form a Matroid, which is used to show all transcendence bases have the same cardinality. Provide algebraic characterizations of the matroid notions `Indep`, `Base`, `cRank`, `Basis`, `closure`, `Flat`, and `Spanning`. + Transcendence bases are exactly algebraic independent families that are spanning (i.e. the whole algebra is algebraic over the algebra generated by the family). On the other hand, a spanning set in a domain contains a transcendence basis. + There always exists an transcendence basis between an arbitrary AlgebraicIndependent set and a spanning set in a domain. + `trdeg R S + trdeg S A = trdeg R A` in a domain, which depends on `AlgebraicIndependent/IsTranscendenceBasis.sumElim_comp`. + A finite AlgebraicIndependent family or spanning family in a domain that has the same cardinality as `trdeg` must be a transcendence basis. --- - [x] depends on: #20887 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-algebra
label:t-algebra$
 408/28 Mathlib/FieldTheory/IsAlgClosed/Classification.lean,Mathlib/FieldTheory/SeparableDegree.lean,Mathlib/RingTheory/AlgebraicIndependent/RankAndCardinality.lean,Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean 4 6 ['alreadydone', 'erdOne', 'github-actions', 'mathlib4-dependent-issues-bot'] nobody
0-21394
5 hours ago
0-21394
5 hours ago
13-1969
13 days
24194 Kiolt
author:Kiolt
 feat(AlgebraicGeometry): `ChosenFiniteProduct` over a general base From Toric --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) toric maintainer-merge t-algebraic-geometry 8/0 Mathlib/AlgebraicGeometry/Pullbacks.lean 1 3 ['erdOne', 'github-actions'] nobody
0-20738
5 hours ago
0-21044
5 hours ago
0-26019
7 hours
22962 YaelDillies
author:YaelDillies
 feat: torsion-free *monoids* Behind this click-baity title, there is the fact that `Monoid.IsTorsionFree` is incorrect for torsion-free monoids. Indeed, if `n ≠ 0` then `∀ a : α, n • a = 0 → a = 0` is equivalent to `∀ a b : α, n • a = n • b → a = b` only if `α` is a group. If `α` is a monoid (possibly even cancellative!), then the `∀ a : α, n • a = 0 → a = 0` condition is quite weak. This PR introduces this new definition under the names `IsAddTorsionFree`/`IsMulTorsionFree`. Several things to note: * It is a class, while `Monoid.IsTorsionFree` is not. * It is outside of the `Monoid`/`AddMonoid` namespace. My thought is that people who care about torsion-free groups will prefer writing `IsAddTorsionFree G` over `Monoid.IsTorsionFree`. * I am making a new file. This is because the existing definitions talk about order of an element, which is a much more advanced notion than the new one I am offering. * I am not changing the existing definition in this PR. This will be done in a later PR. The new imports just come from making `#min_imports` and `mk_iff` available earlier. From Toric Co-authored-by: Patrick Luo --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) toric large-import maintainer-merge t-algebra
label:t-algebra$
 83/33 Mathlib.lean,Mathlib/Algebra/Group/Torsion.lean,Mathlib/Algebra/Order/Group/Basic.lean,Mathlib/Algebra/Order/Ring/Basic.lean,Mathlib/NumberTheory/Padics/MahlerBasis.lean,Mathlib/RingTheory/Binomial.lean 6 5 ['YaelDillies', 'erdOne', 'github-actions'] nobody
0-13651
3 hours ago
0-20517
5 hours ago
35-15323
35 days
23997 YaelDillies
author:YaelDillies
 feat: `ι →₀ R` is a finite `R`-module iff `ι` is finite --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-algebra
label:t-algebra$
 97/68 Mathlib/Data/Finsupp/Single.lean,Mathlib/Data/Matrix/Rank.lean,Mathlib/LinearAlgebra/Basis/Cardinality.lean,Mathlib/LinearAlgebra/Dimension/Finite.lean,Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean,Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean,Mathlib/LinearAlgebra/Finsupp/Supported.lean,Mathlib/LinearAlgebra/Finsupp/VectorSpace.lean,Mathlib/LinearAlgebra/StdBasis.lean,Mathlib/RingTheory/Finiteness/Cardinality.lean 10 n/a ['YaelDillies', 'alreadydone', 'eric-wieser', 'github-actions'] nobody
0-1309
21 minutes ago
unknown
unknown
19315 quangvdao
author:quangvdao
 feat(Data/Finsupp/Fin): Add `Finsupp` operations on `Fin` tuple This PR adds more analogues of operations on `Fin` tuples to the `Finsupp` setting. Before, there were only `Finsupp.cons` and `Finsupp.tail`. Now there are also `Finsupp.snoc`, `Finsupp.insertNth`, `Finsupp.init`, and `Finsupp.removeNth`. These all come with supporting lemmas. I also removed the porting comment about `succAboveCases` in `Data/Fin/Basic`, and added a lemma about `succAbove` in `Data/Fin/Tuple/Basic`. --- - [x] depends on: #20361 - [x] depends on: #20771 - [x] depends on: #20770 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data maintainer-merge merge-conflict awaiting-author 193/16 Mathlib/Algebra/BigOperators/Fin.lean,Mathlib/Algebra/BigOperators/Finsupp.lean,Mathlib/Algebra/MvPolynomial/Equiv.lean,Mathlib/Data/Finsupp/Fin.lean,Mathlib/RingTheory/MvPolynomial/Homogeneous.lean,scripts/nolints_prime_decls.txt 6 44 ['YaelDillies', 'github-actions', 'j-loreaux', 'kbuzzard', 'mathlib4-dependent-issues-bot', 'quangvdao'] nobody
40-7030
1 month ago
40-7030
1 month ago
43-81255
43 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 12 ['YaelDillies', 'github-actions', 'vihdzp'] nobody
29-58563
29 days ago
29-58563
29 days ago
36-50134
36 days

PRs from a fork of mathlib

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
23772 SEU-Prime
author:SEU-Prime
 Create Amice.lean i built amice equiv [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-number-theory WIP 283/0 Mathlib/NumberTheory/Padics/Amice.lean 1 n/a ['grunweg'] nobody
12-21732
12 days ago
unknown
unknown
23986 ShouxinZhang
author:ShouxinZhang
 feat(FieldTheory/RatFunc): add RatFunc.toFractionRingAlgEquiv --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) will-close-soon t-algebra
label:t-algebra$
 17/0 Mathlib/FieldTheory/RatFunc/Basic.lean 1 1 ['joneugster'] nobody
1-80914
1 day ago
1-80914
1 day ago
0-0
0 seconds
3610 TimothyGu
author:TimothyGu
 feat: derive Infinite automatically for inductive types Deals with recursive types, but not mutually recursive types or types with indices right now. See docstring for details. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-meta merge-conflict awaiting-author 517/0 Mathlib.lean,Mathlib/Tactic/DeriveInfinite.lean,test/DeriveInfinite.lean 3 11 ['TimothyGu', 'digama0', 'eric-wieser', 'grunweg', 'kim-em', 'kmill'] kmill
assignee:kmill
104-56544
3 months ago
104-56544
3 months ago
0-0
0 seconds

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
8047 faenuccio
author:faenuccio
 refactor(Util/Delaborators): remove `scoped` from delabPi' Following [this discussion](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Notation.20for.20Pi.20type) on Zulip, remove `scoped` from the delaborator of `Pi` so that in the infoview the `Pi` symbol appears again. awaiting-zulip t-meta 1/1 Mathlib/Util/Delaborators.lean 1 3 ['eric-wieser', 'github-actions', 'joneugster'] nobody
33-15568
1 month ago
33-15568
1 month ago
503-61537
503 days
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
10-4166
10 days ago
10-4255
10 days ago
0-23929
6 hours
24083 Parcly-Taxel
author:Parcly-Taxel
 feat: the `longFileHard` linter @kim-em [on Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/long.20files/near/510548946): > Yes, we don't have a sustainable mechanism that will prevent long files creeping back, unless when we reach "no long file", we turn it into an non-overridable error...! > > It would be great to have such a mechanism, of course, because I agree, of course, that this would be annoying to contributors (and doubly annoying to reviewers if they had to remind contributors not to "compress" things). awaiting-zulip t-linter 72/1 Mathlib/Tactic/Linter/Style.lean,MathlibTest/LongFile.lean,lakefile.lean 3 2 ['github-actions', 'grunweg'] nobody
4-14917
4 days ago
4-14917
4 days ago
0-5347
1 hour
19872 YaelDillies
author:YaelDillies
 chore(GroupTheory/Index): rename `relindex` to `relIndex` --- - [x] depends on: #24044 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) FLT awaiting-zulip t-algebra
label:t-algebra$
 214/137 Mathlib/FieldTheory/Relrank.lean,Mathlib/GroupTheory/Commensurable.lean,Mathlib/GroupTheory/CosetCover.lean,Mathlib/GroupTheory/GroupAction/Blocks.lean,Mathlib/GroupTheory/Index.lean,Mathlib/GroupTheory/IndexNormal.lean,Mathlib/GroupTheory/PGroup.lean,Mathlib/GroupTheory/Schreier.lean,Mathlib/GroupTheory/SchurZassenhaus.lean,Mathlib/GroupTheory/Sylow.lean,Mathlib/GroupTheory/Transfer.lean,Mathlib/LinearAlgebra/FreeModule/Finite/CardQuotient.lean,Mathlib/RingTheory/Ideal/Quotient/Index.lean 13 18 ['Ruben-VandeVelde', 'TwoFX', 'YaelDillies', 'alreadydone', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant', 'loefflerd', 'madvorak', 'mathlib4-dependent-issues-bot', 'tb65536'] nobody
3-43124
3 days ago
3-43124
3 days ago
114-79171
114 days
23721 YaelDillies
author:YaelDillies
 chore: rename `AlgebraCat` to `Alg` and its friends too. The new names: * are shorter * match `Grp`, `CommGrp` * are what people would write on paper The existing name is too much of a mouthful to be usefully included in declaration names. For example, [`BialgebraCat.hasForgetToAlgebra`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Category/BialgebraCat/Basic.html#BialgebraCat.hasForgetToAlgebra) wasn't named `BialgebraCat.hasForgetToAlgebraCat`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-algebra awaiting-author
label:t-algebra$
 433/433 Mathlib.lean,Mathlib/Algebra/Algebra/Defs.lean,Mathlib/Algebra/BrauerGroup/Defs.lean,Mathlib/Algebra/Category/Alg/Basic.lean,Mathlib/Algebra/Category/Alg/Limits.lean,Mathlib/Algebra/Category/Alg/Monoidal.lean,Mathlib/Algebra/Category/Alg/Symmetric.lean,Mathlib/Algebra/Category/AlgebraCat/Symmetric.lean,Mathlib/Algebra/Category/Bialg/Basic.lean,Mathlib/Algebra/Category/Bialg/Monoidal.lean,Mathlib/Algebra/Category/Coalg/Basic.lean,Mathlib/Algebra/Category/Coalg/ComonEquivalence.lean,Mathlib/Algebra/Category/Coalg/Monoidal.lean,Mathlib/Algebra/Category/HopfAlg/Basic.lean,Mathlib/Algebra/Category/HopfAlg/Monoidal.lean,Mathlib/Algebra/Category/Ring/Under/Basic.lean,Mathlib/CategoryTheory/Monoidal/Hopf_.lean,Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean,Mathlib/CategoryTheory/Monoidal/Internal/Module.lean,Mathlib/CategoryTheory/Monoidal/Mon_.lean,Mathlib/LinearAlgebra/CliffordAlgebra/CategoryTheory.lean,Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Monoidal.lean,Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat/Symmetric.lean,Mathlib/RingTheory/Coalgebra/TensorProduct.lean,Mathlib/RingTheory/HopfAlgebra/Basic.lean,MathlibTest/CategoryTheory/ConcreteCategory/Alg.lean,docs/overview.yaml 27 8 ['YaelDillies', 'b-mehta', 'erdOne', 'github-actions', 'leanprover-community-bot-assistant', 'urkud'] nobody
2-67589
2 days ago
2-67589
2 days ago
10-35940
10 days
23974 fbarroero
author:fbarroero
 fix: change file name for consistency We change the name of the file `Mathlib.Algebra.Polynomial.ofFn` to `Mathlib.Algebra.Polynomial.OfFn` for consistency. For instance, the file containing `List.ofFn` is called `Init.Data.List.OfFn`. Zulip discussion [here](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2323974.20Change.20file.20name.20to.20CamelCase/with/512739476) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip easy 2/2 Mathlib.lean,Mathlib/Algebra/Polynomial/OfFn.lean,Mathlib/LinearAlgebra/RootSystem/Finite/G2.lean 3 3 ['github-actions', 'grunweg', 'riccardobrasca'] nobody
0-32743
9 hours ago
2-45888
2 days ago
4-60671
4 days
24178 wswartworth
author:wswartworth
 feat: sort eigenvalues in Analysis.InnerProductSpace.Spectrum Spectrum.eigenvalues and Spectrum.eigenvectorBasis now give the eigenvalues and eigenvectors in increasing order of eigenvalues, which clears a prior TODO. The new theorem eigenvalues_monotone allows the monotonicity to be used downstream. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip new-contributor t-analysis 39/19 Mathlib/Analysis/InnerProductSpace/Spectrum.lean 1 3 ['github-actions', 'j-loreaux', 'wswartworth'] nobody
0-21063
5 hours ago
0-21063
5 hours ago
0-48679
13 hours
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
215-55076
7 months ago
215-77051
7 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
168-8795
5 months ago
193-83717
6 months ago*
0-0
0 seconds*
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) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-algebra merge-conflict
label:t-algebra$
 107/114 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/Definitions.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/Fintype.lean,Mathlib/RingTheory/Localization/NumDen.lean,Mathlib/RingTheory/Polynomial/Content.lean,Mathlib/RingTheory/Polynomial/GaussLemma.lean,Mathlib/RingTheory/Valuation/Basic.lean 27 11 ['MichaelStollBayreuth', 'acmepjz', 'eric-wieser', 'github-actions', 'leanprover-bot', 'urkud'] nobody
155-33110
5 months ago
155-33110
5 months ago
0-66650
18 hours
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
150-28326
4 months ago
150-28326
4 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 28 ['YaelDillies', 'eric-wieser', 'girving', 'github-actions', 'j-loreaux', 'kbuzzard', 'leanprover-community-bot-assistant', 'urkud'] nobody
6-12332
6 days ago
6-12333
6 days ago
29-60989
29 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
23676 Parcly-Taxel
author:Parcly-Taxel
 chore: deprime `induction'` for localizations and quotients All these removed instances of `induction'` generate only one subgoal. In some cases `obtain` can be used. The relevant instances were identified by adding the following to `Mathlib.Tactic.Cases` ```diff diff --git a/Mathlib/Tactic/Cases.lean b/Mathlib/Tactic/Cases.lean index 4a60db6c551..08c06520879 100644 --- a/Mathlib/Tactic/Cases.lean +++ b/Mathlib/Tactic/Cases.lean @@ -122,6 +122,16 @@ elab (name := induction') "induction' " tgts:(Parser.Tactic.elimTarget,+) g.assign result.elimApp let subgoals ← ElimApp.evalNames elimInfo result.alts withArg (generalized := fvarIds) (toClear := targetFVarIds) (toTag := toTag) + let body ← inferType targets[0]! + let names : Array Format := if withArg.1.getArgs.size > 1 then + (withArg.1.getArgs[1]!).getArgs.map Syntax.prettyPrint else Array.empty + let gens : Array Format := if genArg.1.getArgs.size > 1 then + (genArg.1.getArgs[1]!).getArgs.map Syntax.prettyPrint else Array.empty + let inductor : Format := if usingArg.1.getArgs.size > 1 then + Syntax.prettyPrint usingArg.1.getArgs[1]! else "~" + if subgoals.toList.length ≤ 1 then + logInfoAt tgts m!"{body.getAppFn.setPPExplicit true} {inductor} {gens} {names} \ + {subgoals.toList.length}" setGoals <| (subgoals ++ result.others).toList ++ gs /-- The `cases'` tactic is similar to the `cases` tactic in Lean 4 core, but the syntax for giving ``` and then examining [the output](https://github.com/leanprover-community/mathlib4/actions/runs/14270845291/job/40003467676). tech debt 87/108 Mathlib/Algebra/Module/LocalizedModule/Basic.lean,Mathlib/Algebra/Pointwise/Stabilizer.lean,Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean,Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean,Mathlib/CategoryTheory/Action/Concrete.lean,Mathlib/CategoryTheory/Galois/EssSurj.lean,Mathlib/CategoryTheory/Limits/Types/Colimits.lean,Mathlib/CategoryTheory/Subobject/Basic.lean,Mathlib/CategoryTheory/Subobject/FactorThru.lean,Mathlib/CategoryTheory/Subobject/Lattice.lean,Mathlib/Data/Finset/NoncommProd.lean,Mathlib/Data/Finsupp/BigOperators.lean,Mathlib/Data/Fintype/Quotient.lean,Mathlib/Data/List/Cycle.lean,Mathlib/Data/Nat/ChineseRemainder.lean,Mathlib/Data/Setoid/Partition.lean,Mathlib/FieldTheory/RatFunc/Basic.lean,Mathlib/GroupTheory/GroupAction/Quotient.lean,Mathlib/GroupTheory/OreLocalization/Basic.lean,Mathlib/GroupTheory/Perm/Cycle/Concrete.lean,Mathlib/GroupTheory/Perm/Sign.lean,Mathlib/GroupTheory/Torsion.lean,Mathlib/RingTheory/OreLocalization/Basic.lean,Mathlib/RingTheory/OreLocalization/Ring.lean,Mathlib/SetTheory/Surreal/Basic.lean 25 7 ['Parcly-Taxel', 'apnelson1', 'eric-wieser', 'github-actions'] nobody
14-69410
14 days ago
15-4052
15 days ago
15-4037
15 days
23324 Parcly-Taxel
author:Parcly-Taxel
 chore: deprime `induction'` with 5+ variables, part 3 Based on a comment by @apnelson1 on [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/The.20plan.20to.20remove.20induction'/near/508274747). The relevant instances were identified by adding the following to `Mathlib.Tactic.Cases` ```diff diff --git a/Mathlib/Tactic/Cases.lean b/Mathlib/Tactic/Cases.lean index 4a60db6c551..29ec70424c7 100644 --- a/Mathlib/Tactic/Cases.lean +++ b/Mathlib/Tactic/Cases.lean @@ -122,6 +122,16 @@ elab (name := induction') "induction' " tgts:(Parser.Tactic.elimTarget,+) g.assign result.elimApp let subgoals ← ElimApp.evalNames elimInfo result.alts withArg (generalized := fvarIds) (toClear := targetFVarIds) (toTag := toTag) + let body ← inferType targets[0]! + let names : Array Format := if withArg.1.getArgs.size > 1 then + (withArg.1.getArgs[1]!).getArgs.map Syntax.prettyPrint else Array.empty + let gens : Array Format := if genArg.1.getArgs.size > 1 then + (genArg.1.getArgs[1]!).getArgs.map Syntax.prettyPrint else Array.empty + let inductor : Format := if usingArg.1.getArgs.size > 1 then + Syntax.prettyPrint usingArg.1.getArgs[1]! else "~" + if 5 ≤ names.size then + logInfoAt tgts m!"{body.getAppFn.setPPExplicit true} {inductor} {gens} {names} \ + {subgoals.toList.length}" setGoals <| (subgoals ++ result.others).toList ++ gs /-- The `cases'` tactic is similar to the `cases` tactic in Lean 4 core, but the syntax for giving ``` and then examining [the output](https://github.com/leanprover-community/mathlib4/actions/runs/14085064444/job/39446843657). tech debt 168/119 Mathlib/Probability/Kernel/Defs.lean,Mathlib/Probability/Moments/Basic.lean,Mathlib/RingTheory/EssentialFiniteness.lean,Mathlib/RingTheory/FiniteType.lean,Mathlib/RingTheory/Flat/Equalizer.lean,Mathlib/RingTheory/IsTensorProduct.lean,Mathlib/RingTheory/Kaehler/JacobiZariski.lean,Mathlib/RingTheory/Kaehler/Polynomial.lean,Mathlib/RingTheory/Multiplicity.lean,Mathlib/RingTheory/Nakayama.lean,Mathlib/RingTheory/Polynomial/Ideal.lean,Mathlib/RingTheory/PowerSeries/Order.lean,Mathlib/RingTheory/Presentation.lean,Mathlib/RingTheory/Smooth/StandardSmooth.lean,Mathlib/RingTheory/TensorProduct/MvPolynomial.lean,Mathlib/RingTheory/Unramified/Finite.lean,Mathlib/SetTheory/Lists.lean,Mathlib/SetTheory/Ordinal/FixedPoint.lean,Mathlib/SetTheory/Ordinal/Notation.lean,Mathlib/SetTheory/Ordinal/Principal.lean,Mathlib/SetTheory/PGame/Algebra.lean,Mathlib/SetTheory/PGame/Order.lean 22 12 ['Parcly-Taxel', 'apnelson1', 'eric-wieser', 'github-actions'] nobody
7-72425
7 days ago
15-10163
15 days ago
23-9538
23 days
16408 Parcly-Taxel
author:Parcly-Taxel
 chore: deprecate `Order.Nat` * Move the two `Nat` instances and `bot_eq_zero` to `Order.BoundedOrder.Basic`. We also remove the TODO relating to #13092, as it was tried and it was agreed not to be a good idea. * Move the other two lemmas in `Order.Nat` to `Data.Nat.Find`. tech debt 35/54 Mathlib/Algebra/IsPrimePow.lean,Mathlib/Data/Finset/Grade.lean,Mathlib/Data/Finset/Lattice/Fold.lean,Mathlib/Data/Nat/Basic.lean,Mathlib/Data/Nat/Cast/SetInterval.lean,Mathlib/Data/Nat/Find.lean,Mathlib/Data/Nat/SuccPred.lean,Mathlib/Data/Rat/Cast/Defs.lean,Mathlib/Order/BoundedOrder/Basic.lean,Mathlib/Order/Filter/AtTopBot/Basic.lean,Mathlib/Order/Nat.lean,Mathlib/RingTheory/Multiplicity.lean,Mathlib/SetTheory/Cardinal/Order.lean 13 8 ['Parcly-Taxel', 'YaelDillies', 'github-actions', 'grunweg'] nobody
1-40062
1 day ago
3-66143
3 days ago
6-14852
6 days