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 17, 2025 at 21:58 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
23641 eric-wieser
author:eric-wieser
 feat: generalize `TwoSidedIdeal.matricesOver` to `RingCon` This generalizes the result to non-associative rings, and most of results to non-unital rings. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) auto-merge-after-CI t-algebra
label:t-algebra$
 195/97 Mathlib/Data/Matrix/Basis.lean,Mathlib/LinearAlgebra/Matrix/Ideal.lean,Mathlib/RingTheory/Congruence/Defs.lean,Mathlib/RingTheory/SimpleRing/Matrix.lean,Mathlib/RingTheory/TwoSidedIdeal/Basic.lean 5 39 ['Whysoserioushah', 'alreadydone', 'eric-wieser', 'github-actions', 'j-loreaux', 'mathlib-bors', 'sgouezel'] nobody
4-78367
4 days ago
4-78416
4 days ago
5-1046
5 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
27-31258
27 days ago
27-32420
27 days ago
28-71368
28 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
14-72936
14 days ago
14-72936
14 days ago
46-85320
46 days
23558 JovanGerb
author:JovanGerb
 feat: don't delaborate to `⊔` or `⊓` if we have a `LinearOrder` This PR changes the `⊔` and `⊓` notations to only be used by the delaborator if the type in question is not a linear order. This was suggested here [#mathlib4 > max and min delaborators @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/max.20and.20min.20delaborators/near/500701449) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) large-import maintainer-merge t-order t-meta 124/8 Mathlib/Order/Notation.lean,MathlibTest/Delab/SupInf.lean 2 35 ['JovanGerb', 'eric-wieser', 'fpvandoorn', 'github-actions', 'kmill'] kmill
assignee:kmill
10-61551
10 days ago
11-29390
11 days ago
16-13543
16 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
9-47037
9 days ago
9-65870
9 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
8-77064
8 days ago
9-48898
9 days ago
65-20490
65 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
7-36810
7 days ago
7-44347
7 days ago
31-19292
31 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
5-49015
5 days ago
5-49016
5 days ago
6-6857
6 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
2-46205
2 days ago
2-46206
2 days ago
2-51175
2 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
2-24206
2 days ago
2-43110
2 days ago
11-43435
11 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 1 ['github-actions'] nobody
0-705
11 minutes ago
16-42832
16 days ago
16-42815
16 days
23549 bryangingechen
author:bryangingechen
 chore: make dependabot group updates into a single PR cf. docs at https://docs.github.com/en/code-security/dependabot/dependabot-version-updates/optimizing-pr-creation-version-updates --- It was a bit annoying to make a single bors batch for [#23544](https://github.com/leanprover-community/mathlib4/pull/23544) [#23543](https://github.com/leanprover-community/mathlib4/pull/23543) [#23541](https://github.com/leanprover-community/mathlib4/pull/23541) [#23540](https://github.com/leanprover-community/mathlib4/pull/23540). maintainer-merge CI 10/0 .github/dependabot.yml 1 1 ['github-actions'] nobody
0-468
7 minutes ago
16-27359
16 days ago
16-27343
16 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
38-13612
1 month ago
38-13612
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
27-65145
27 days ago
27-65145
27 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
27-31258
27 days ago
27-32420
27 days ago
28-71368
28 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
14-72936
14 days ago
14-72936
14 days ago
46-85320
46 days
23558 JovanGerb
author:JovanGerb
 feat: don't delaborate to `⊔` or `⊓` if we have a `LinearOrder` This PR changes the `⊔` and `⊓` notations to only be used by the delaborator if the type in question is not a linear order. This was suggested here [#mathlib4 > max and min delaborators @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/max.20and.20min.20delaborators/near/500701449) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) large-import maintainer-merge t-order t-meta 124/8 Mathlib/Order/Notation.lean,MathlibTest/Delab/SupInf.lean 2 35 ['JovanGerb', 'eric-wieser', 'fpvandoorn', 'github-actions', 'kmill'] kmill
assignee:kmill
10-61551
10 days ago
11-29390
11 days ago
16-13543
16 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
9-47037
9 days ago
9-65870
9 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
8-77064
8 days ago
9-48898
9 days ago
65-20490
65 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
7-36810
7 days ago
7-44347
7 days ago
31-19292
31 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
5-49015
5 days ago
5-49016
5 days ago
6-6857
6 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
2-46205
2 days ago
2-46206
2 days ago
2-51175
2 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
2-24206
2 days ago
2-43110
2 days ago
11-43435
11 days
24025 YaelDillies
author:YaelDillies
 feat: the index of the scaling of a subgroup From FLT --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) FLT maintainer-merge t-algebra
label:t-algebra$
 19/4 Mathlib/GroupTheory/Index.lean 1 2 ['Ruben-VandeVelde', 'github-actions'] nobody
0-28832
8 hours ago
0-28832
8 hours ago
3-48011
3 days
24037 YaelDillies
author:YaelDillies
 feat: `insert (b + 1) (Ioc a b) = Ioc a (b + 1)` And shorten recently introduced names for consistency --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-order 164/32 Mathlib/Algebra/Order/Interval/Finset/SuccPred.lean,Mathlib/Algebra/Order/Interval/Set/SuccPred.lean,Mathlib/Order/Interval/Finset/SuccPred.lean,Mathlib/Order/Interval/Set/SuccPred.lean 4 7 ['Ruben-VandeVelde', 'b-mehta', 'github-actions'] nobody
0-26078
7 hours ago
1-51488
1 day ago
3-12428
3 days
24134 sgouezel
author:sgouezel
 feat: drop measurability assumption in `norm_setIntegral_le_of_norm_le_const_ae'` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-measure-probability 46/47 Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean,Mathlib/Analysis/SpecialFunctions/MulExpNegMulSqIntegral.lean,Mathlib/MeasureTheory/Integral/Bochner/FundThmCalculus.lean,Mathlib/MeasureTheory/Integral/Bochner/Set.lean,Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean,Mathlib/MeasureTheory/Integral/TorusIntegral.lean,Mathlib/NumberTheory/Transcendental/Lindemann/AnalyticalPart.lean 8 3 ['Ruben-VandeVelde', 'github-actions', 'grunweg'] nobody
0-17520
4 hours ago
0-17521
4 hours ago
0-42960
11 hours
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
0-13741
3 hours ago
0-16532
4 hours ago
43-83342
43 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
0-10771
2 hours ago
0-11981
3 hours ago
29-13936
29 days
24146 urkud
author:urkud
 feat(BigOperators/Ring): add `Finset.prod_neg` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-algebra
label:t-algebra$
 4/1 Mathlib/Algebra/BigOperators/Ring/Finset.lean 1 5 ['YaelDillies', 'github-actions', 'urkud'] nobody
0-8411
2 hours ago
0-13512
3 hours ago
0-17028
4 hours
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 awaiting-author 196/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 44 ['YaelDillies', 'b-mehta', 'github-actions', 'mathlib4-dependent-issues-bot', 'pimotte'] nobody
0-6760
1 hour ago
0-6760
1 hour ago
22-41778
22 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 1 ['github-actions'] nobody
0-705
11 minutes ago
16-42832
16 days ago
16-42815
16 days
23549 bryangingechen
author:bryangingechen
 chore: make dependabot group updates into a single PR cf. docs at https://docs.github.com/en/code-security/dependabot/dependabot-version-updates/optimizing-pr-creation-version-updates --- It was a bit annoying to make a single bors batch for [#23544](https://github.com/leanprover-community/mathlib4/pull/23544) [#23543](https://github.com/leanprover-community/mathlib4/pull/23543) [#23541](https://github.com/leanprover-community/mathlib4/pull/23541) [#23540](https://github.com/leanprover-community/mathlib4/pull/23540). maintainer-merge CI 10/0 .github/dependabot.yml 1 1 ['github-actions'] nobody
0-468
7 minutes ago
16-27359
16 days ago
16-27343
16 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
38-13612
1 month ago
38-13612
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
27-65145
27 days ago
27-65145
27 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 2 ['grunweg'] nobody
10-28314
10 days ago
10-28314
10 days ago
0-0
0 seconds
23937 unknown
author:unknown
 feat(Algebra): vanishing of induced hom between ext unknown description t-algebra t-category-theory blocked-by-other-PR WIP
label:t-algebra$
 -1/-1 -1 n/a None nobody
1-36042
1 day 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
0-1096
18 minutes ago
0-3679
1 hour 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
102-63126
3 months ago
102-63126
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
31-22150
1 month ago
31-22150
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
8-10748
8 days ago
8-10837
8 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
2-21499
2 days ago
2-21499
2 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
1-49706
1 day ago
1-49706
1 day 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
0-74171
20 hours ago
0-74171
20 hours 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 1/1 Mathlib.lean,Mathlib/Algebra/Polynomial/OfFn.lean 2 3 ['github-actions', 'grunweg', 'riccardobrasca'] nobody
0-28911
8 hours ago
0-52470
14 hours ago
4-60671
4 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
213-61658
7 months ago
213-83633
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
166-15377
5 months ago
192-3899
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
153-39692
5 months ago
153-39692
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
148-34908
4 months ago
148-34908
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
4-18914
4 days ago
4-18915
4 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
12-75992
12 days ago
13-10634
13 days ago
13-10617
13 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
5-79007
5 days ago
13-16745
13 days ago
21-16118
21 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 7 ['Parcly-Taxel', 'YaelDillies', 'github-actions', 'grunweg'] nobody
0-69105
19 hours ago
1-72725
1 day ago
4-21432
4 days