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: December 13, 2025 at 11:56 UTC

Stale ready-to-merge'd PRs

There are currently no stale PRs labelled auto-merge-after-CI or ready-to-merge. Congratulations!

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
30333 paulorauber
author:paulorauber
 feat(Probability): definition of trajMeasure A definition of `trajMeasure` and some basic lemmas. In the context of the Ionescu-Tulcea theorem, `trajMeasure μ₀ κ` corresponds to the distribution of the trajectory obtained by starting with the distribution `μ₀` and then iterating the kernels `κ`. Lemmas `partialTraj_compProd_kernel_eq_traj_map` and `traj_map_eq_kernel` are attributable to @EtienneC30 and some definitions borrow code from @RemyDegenne , who also improved the code considerably. Please let me know if you would like to be co-authors in this pull request. From the LeanBandits project. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-measure-probability new-contributor maintainer-merge 80/2 Mathlib/Order/Interval/Finset/Basic.lean,Mathlib/Order/Interval/Finset/Nat.lean,Mathlib/Probability/Kernel/IonescuTulcea/PartialTraj.lean,Mathlib/Probability/Kernel/IonescuTulcea/Traj.lean 4 28 ['EtienneC30', 'RemyDegenne', 'github-actions', 'mathlib4-merge-conflict-bot', 'paulorauber'] EtienneC30
assignee:EtienneC30
8-4935
8 days ago
8-4935
8 days ago
15-70621
15 days
32480 ADedecker
author:ADedecker
 feat: define `PolynormableSpace` A "polynormable space" is a TVS whose topology is induced by *some* family of seminorms. In the real or complex case this is just locally convex, but it makes sense (and will be used) for general nontrivially normed fields. The name is inspired by Bourbaki's "espace polynormé", although they only allow ultrametric seminorms over an ultrametric field. My motivation is the following: - first, I want to be able to state [WithSeminorms.banach_steinhaus](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/LocallyConvex/Barrelled.html#WithSeminorms.banach_steinhaus) without a choice of seminorm family. This is easy to do, and I have a PR on the way - the notion of bornological TVS makes sense over an arbitrary nontrivially normed field, and we have that any sequentially continuous linear map from a bornological TVS to a polynormable space is continuous. I see no reason to restrict to the real or complex case here. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-analysis maintainer-merge 51/0 Mathlib/Analysis/LocallyConvex/AbsConvexOpen.lean,Mathlib/Analysis/LocallyConvex/WithSeminorms.lean 2 7 ['ADedecker', 'github-actions', 'j-loreaux'] fpvandoorn
assignee:fpvandoorn
3-4219
3 days ago
3-4219
3 days ago
7-13313
7 days
32405 Shaddaaa
author:Shaddaaa
 feat(CategoryTheory/Sites): (Co)continuity of `Over.iteratedSliceEquiv` Show that the `Over.iteratedSliceEquiv` functor is continuous and cocontinuous. This contribution was created as part of the Heidelberg Lean workshop "Formalising algebraic geometry" in November 2025. Co-authored-by: Ben Eltschig @peabrainiac Co-authored-by: Andrew Yang @erdOne --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-author t-category-theory new-contributor maintainer-merge large-import 44/4 Mathlib/CategoryTheory/Sites/Equivalence.lean,Mathlib/CategoryTheory/Sites/Over.lean 2 28 ['Shaddaaa', 'dagurtomas', 'erdOne', 'github-actions', 'jcommelin', 'joelriou'] nobody
1-56783
1 day ago
1-56783
1 day ago
0-52480
14 hours
32652 BGuillemet
author:BGuillemet
 feat(CategoryTheory/Sites): add the Grothendieck topology generated by a precoverage Add the file `PrecoverageToGrothendieck.lean`, in which the Grothendieck topology generated by a precoverage is defined as `Precoverage.toGrothendieck`. This replace the previous `Precoverage.toGrothendieck`, which was defined only in the case of a precoverage having pullbacks and being stable under base change. The equivalence between the two constructions is `Precoverage.toGrothendieck_toCoverage`. Prove `Precoverage.isSheaf_toGrothendieck_iff`: given a precoverage `J`, a type-valued presheaf is a sheaf for `J.toGrothendieck` if and only if it is a sheaf for all the pullback sieves of the presieves in `J`. The proof is based on the previous proof of `isSheaf_coverage`, which is now a consequence of `Precoverage.isSheaf_toGrothendieck_iff`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-author t-category-theory maintainer-merge 236/106 Mathlib.lean,Mathlib/CategoryTheory/Sites/Coverage.lean,Mathlib/CategoryTheory/Sites/Over.lean,Mathlib/CategoryTheory/Sites/PrecoverageToGrothendieck.lean 4 22 ['BGuillemet', 'chrisflav', 'github-actions'] nobody
1-9632
1 day ago
1-9632
1 day ago
1-39387
1 day
31717 thorimur
author:thorimur
 chore: refactor `Type*` and `Sort*` to use `mkFreshLevelParam` Uses the API for creating new level parameters introduced in #30797. --- - [ ] depends on: #30797 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-meta large-import 4/7 Mathlib/Tactic/TypeStar.lean 1 3 ['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] dwrensha
assignee:dwrensha
5-39327
5 days ago
8-65743
8 days ago
11-20443
11 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
30333 paulorauber
author:paulorauber
 feat(Probability): definition of trajMeasure A definition of `trajMeasure` and some basic lemmas. In the context of the Ionescu-Tulcea theorem, `trajMeasure μ₀ κ` corresponds to the distribution of the trajectory obtained by starting with the distribution `μ₀` and then iterating the kernels `κ`. Lemmas `partialTraj_compProd_kernel_eq_traj_map` and `traj_map_eq_kernel` are attributable to @EtienneC30 and some definitions borrow code from @RemyDegenne , who also improved the code considerably. Please let me know if you would like to be co-authors in this pull request. From the LeanBandits project. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-measure-probability new-contributor maintainer-merge 80/2 Mathlib/Order/Interval/Finset/Basic.lean,Mathlib/Order/Interval/Finset/Nat.lean,Mathlib/Probability/Kernel/IonescuTulcea/PartialTraj.lean,Mathlib/Probability/Kernel/IonescuTulcea/Traj.lean 4 28 ['EtienneC30', 'RemyDegenne', 'github-actions', 'mathlib4-merge-conflict-bot', 'paulorauber'] EtienneC30
assignee:EtienneC30
8-4935
8 days ago
8-4935
8 days ago
15-70621
15 days
32480 ADedecker
author:ADedecker
 feat: define `PolynormableSpace` A "polynormable space" is a TVS whose topology is induced by *some* family of seminorms. In the real or complex case this is just locally convex, but it makes sense (and will be used) for general nontrivially normed fields. The name is inspired by Bourbaki's "espace polynormé", although they only allow ultrametric seminorms over an ultrametric field. My motivation is the following: - first, I want to be able to state [WithSeminorms.banach_steinhaus](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/LocallyConvex/Barrelled.html#WithSeminorms.banach_steinhaus) without a choice of seminorm family. This is easy to do, and I have a PR on the way - the notion of bornological TVS makes sense over an arbitrary nontrivially normed field, and we have that any sequentially continuous linear map from a bornological TVS to a polynormable space is continuous. I see no reason to restrict to the real or complex case here. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-analysis maintainer-merge 51/0 Mathlib/Analysis/LocallyConvex/AbsConvexOpen.lean,Mathlib/Analysis/LocallyConvex/WithSeminorms.lean 2 7 ['ADedecker', 'github-actions', 'j-loreaux'] fpvandoorn
assignee:fpvandoorn
3-4219
3 days ago
3-4219
3 days ago
7-13313
7 days
32405 Shaddaaa
author:Shaddaaa
 feat(CategoryTheory/Sites): (Co)continuity of `Over.iteratedSliceEquiv` Show that the `Over.iteratedSliceEquiv` functor is continuous and cocontinuous. This contribution was created as part of the Heidelberg Lean workshop "Formalising algebraic geometry" in November 2025. Co-authored-by: Ben Eltschig @peabrainiac Co-authored-by: Andrew Yang @erdOne --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-author t-category-theory new-contributor maintainer-merge large-import 44/4 Mathlib/CategoryTheory/Sites/Equivalence.lean,Mathlib/CategoryTheory/Sites/Over.lean 2 28 ['Shaddaaa', 'dagurtomas', 'erdOne', 'github-actions', 'jcommelin', 'joelriou'] nobody
1-56783
1 day ago
1-56783
1 day ago
0-52480
14 hours
32652 BGuillemet
author:BGuillemet
 feat(CategoryTheory/Sites): add the Grothendieck topology generated by a precoverage Add the file `PrecoverageToGrothendieck.lean`, in which the Grothendieck topology generated by a precoverage is defined as `Precoverage.toGrothendieck`. This replace the previous `Precoverage.toGrothendieck`, which was defined only in the case of a precoverage having pullbacks and being stable under base change. The equivalence between the two constructions is `Precoverage.toGrothendieck_toCoverage`. Prove `Precoverage.isSheaf_toGrothendieck_iff`: given a precoverage `J`, a type-valued presheaf is a sheaf for `J.toGrothendieck` if and only if it is a sheaf for all the pullback sieves of the presieves in `J`. The proof is based on the previous proof of `isSheaf_coverage`, which is now a consequence of `Precoverage.isSheaf_toGrothendieck_iff`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-author t-category-theory maintainer-merge 236/106 Mathlib.lean,Mathlib/CategoryTheory/Sites/Coverage.lean,Mathlib/CategoryTheory/Sites/Over.lean,Mathlib/CategoryTheory/Sites/PrecoverageToGrothendieck.lean 4 22 ['BGuillemet', 'chrisflav', 'github-actions'] nobody
1-9632
1 day ago
1-9632
1 day ago
1-39387
1 day
32265 joelriou
author:joelriou
 feat(AlgebraicTopology): finite colimits of finite simplicial sets are finite From https://github.com/joelriou/topcat-model-category --- - [x] depends on: #32201 - [x] depends on: #32202 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-algebraic-topology 82/0 Mathlib.lean,Mathlib/AlgebraicTopology/SimplicialSet/Finite.lean,Mathlib/AlgebraicTopology/SimplicialSet/FiniteColimits.lean,Mathlib/CategoryTheory/FinCategory/Basic.lean 4 5 ['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'robin-carlier'] nobody
0-68673
19 hours ago
0-68673
19 hours ago
0-76897
21 hours
32562 YaelDillies
author:YaelDillies
 chore(Data/Finsupp): rename the `toFun` projection to `apply` in `simps` This is the standard name for fun-like types. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-data 20/37 Counterexamples/CliffordAlgebraNotInjective.lean,Mathlib/Algebra/Group/Finsupp.lean,Mathlib/Algebra/Polynomial/Derivative.lean,Mathlib/Data/Finsupp/Basic.lean,Mathlib/Data/Finsupp/Defs.lean,Mathlib/Data/Finsupp/Interval.lean,Mathlib/Data/Finsupp/Weight.lean,Mathlib/LinearAlgebra/Dual/Basis.lean,Mathlib/RingTheory/AlgebraTower.lean,Mathlib/RingTheory/Flat/EquationalCriterion.lean,Mathlib/RingTheory/HahnSeries/HEval.lean 11 4 ['JovanGerb', 'github-actions', 'mathlib4-merge-conflict-bot'] pechersky
assignee:pechersky
0-66143
18 hours ago
0-66143
18 hours ago
5-37677
5 days
32747 j-loreaux
author:j-loreaux
 feat: integer inequalities from multiples in a strict ordered ring These were useful during the review of #32259. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebra maintainer-merge
label:t-algebra$
 38/0 Mathlib.lean,Mathlib/Algebra/Order/Ring/Interval.lean 2 3 ['github-actions', 'jsm28'] nobody
0-54992
15 hours ago
0-54992
15 hours ago
1-68183
1 day
32237 joelriou
author:joelriou
 feat(AlgebraicTopology): binary products of standard simplices We start the study of nondegenerate simplices in `Δ[p] ⊗ Δ[q]`. In particular, we show that it is of dimension `≤ p + q`. From https://github.com/joelriou/topcat-model-category --- - [x] depends on: #32201 - [x] depends on: #32202 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-algebraic-topology 146/0 Mathlib.lean,Mathlib/AlgebraicTopology/SimplicialSet/Monoidal.lean,Mathlib/AlgebraicTopology/SimplicialSet/ProdStdSimplex.lean 3 12 ['github-actions', 'joelriou', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'robin-carlier'] nobody
0-51610
14 hours ago
0-51610
14 hours ago
0-66289
18 hours
31717 thorimur
author:thorimur
 chore: refactor `Type*` and `Sort*` to use `mkFreshLevelParam` Uses the API for creating new level parameters introduced in #30797. --- - [ ] depends on: #30797 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-meta large-import 4/7 Mathlib/Tactic/TypeStar.lean 1 3 ['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] dwrensha
assignee:dwrensha
5-39327
5 days ago
8-65743
8 days ago
11-20443
11 days
30872 rudynicolop
author:rudynicolop
 feat(Computability/NFA): NFA closure under concatenation This PR proves that regular languages are closed under concatenation via a direct construction on `NFA`s without `εNFA` nor ε-transitions. The main new definitions and results include: - `M1.concat M2`, the concatenation of `NFA`s `M1` and `M2`, a direct construction without ε-transitions. - Theorem `accepts_concat : (M1.concat M2).accepts = M1.accepts * M2.accepts`, showing the correctness of the construction. - Theorem `IsRegular.mul`, showing that regular languages are closed under concatenation. --- - [x] depends on: #31038 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) new-contributor t-computability maintainer-merge 104/7 Mathlib/Computability/NFA.lean 1 59 ['YaelDillies', 'ctchou', 'github-actions', 'lambda-fairy', 'mathlib4-dependent-issues-bot', 'rudynicolop'] YaelDillies
assignee:YaelDillies
0-50779
14 hours ago
5-5636
5 days ago
15-949
15 days
32754 felixpernegger
author:felixpernegger
 feat(Data/Set/Card): ncard of complement of set is Nat.card - ncard of set easy new-contributor maintainer-merge t-data 4/0 Mathlib/Data/Set/Card.lean 1 3 ['felixpernegger', 'github-actions', 'tb65536'] nobody
0-23966
6 hours ago
0-23966
6 hours ago
1-59872
1 day
32761 harahu
author:harahu
 doc(FieldTheory): fix typos Found and fixed by Codex. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebra maintainer-merge
label:t-algebra$
 17/17 Mathlib/FieldTheory/Finite/Extension.lean,Mathlib/FieldTheory/Finite/Trace.lean,Mathlib/FieldTheory/IsAlgClosed/Spectrum.lean,Mathlib/FieldTheory/IsPerfectClosure.lean,Mathlib/FieldTheory/Normal/Defs.lean 5 3 ['github-actions', 'tb65536', 'vihdzp'] nobody
0-23780
6 hours ago
0-23780
6 hours ago
1-47028
1 day
32781 harahu
author:harahu
 doc(GroupTheory): fix typos Typos found and fixed by Codex. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-group-theory 12/12 Mathlib/GroupTheory/DivisibleHull.lean,Mathlib/GroupTheory/HNNExtension.lean,Mathlib/GroupTheory/NoncommCoprod.lean,Mathlib/GroupTheory/PushoutI.lean,Mathlib/GroupTheory/SemidirectProduct.lean 5 2 ['github-actions', 'tb65536'] nobody
0-23421
6 hours ago
0-23421
6 hours ago
1-10233
1 day
32834 YaelDillies
author:YaelDillies
 chore(Algebra): move `CharZero.of_module` earlier This has nothing to do with `NoZeroSMulDivisors`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge 9/15 Mathlib/Algebra/Module/NatInt.lean,Mathlib/Algebra/NoZeroSMulDivisors/Basic.lean,Mathlib/NumberTheory/NumberField/Basic.lean 3 3 ['erdOne', 'github-actions'] nobody
0-4450
1 hour ago
0-4450
1 hour ago
0-6264
1 hour
32584 CBirkbeck
author:CBirkbeck
 feat(NumberTheory/EisensteinSeries/E2): Define the Eisenstein series E2 We define the Eisenstein series E2 and prove some basic results which will be needed in #32585 to prove how it transforms under the slash action of SL2. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-author t-number-theory maintainer-merge large-import 222/4 Mathlib.lean,Mathlib/NumberTheory/ModularForms/EisensteinSeries/E2/Defs.lean,Mathlib/NumberTheory/ModularForms/EisensteinSeries/E2/Summable.lean,Mathlib/Topology/Algebra/InfiniteSum/ConditionalInt.lean 4 24 ['CBirkbeck', 'github-actions', 'loefflerd'] nobody
0-68182
18 hours ago
0-68182
18 hours ago
3-6149
3 days

PRs blocked on a zulip discussion

Number Author Title Description Labels +/- Modified files (first 100) 📝 💬 All users who commented or reviewed Assignee(s) Updated Last status change total time in review
23929 meithecatte
author:meithecatte
 feat(Computability/NFA): improve bound on pumping lemma --- - [x] depends on: #25321 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) new-contributor t-computability awaiting-zulip 101/10 Mathlib/Computability/EpsilonNFA.lean,Mathlib/Computability/NFA.lean 2 41 ['YaelDillies', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'meithecatte'] nobody
188-58069
6 months ago
188-58070
6 months ago
34-10595
34 days
30902 adomani
author:adomani
 chore: longLine warnings happen starting at the 101st character Right now, the longLine linter warning spans the whole line. This PR changes the behaviour and the warning only covers the characters exceeding the 100 character limit. Previous discussion: [#general > error lens in lean4 @ 💬](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/error.20lens.20in.20lean4/near/547074537) Specific thread: [#mathlib4 > Restrict longLine warning to exceeding characters @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Restrict.20longLine.20warning.20to.20exceeding.20characters/near/547081669) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-linter awaiting-zulip 1/1 Mathlib/Tactic/Linter/Style.lean 1 1 ['github-actions'] nobody
48-54633
1 month ago
48-54890
1 month ago
0-132
2 minutes
28141 YaelDillies
author:YaelDillies
 chore: deprecate `BialgHom.coe_toLinearMap` `BialgHom.toLinearMap` is a fake projection. From Toric --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip toric t-ring-theory 5/11 Mathlib/RingTheory/Bialgebra/Hom.lean 1 16 ['YaelDillies', 'erdOne', 'eric-wieser', 'github-actions'] alreadydone
assignee:alreadydone
20-83635
20 days ago
20-83635
20 days ago
101-9047
101 days
30750 SnirBroshi
author:SnirBroshi
 feat(Data/Quot): `toSet` and `equivClassOf` Define `toSet` which gets the set corresponding to an element of a quotient, and `equivClassOf` which gets the equivalence class of an element under a quotient. --- I found these definitions helpful when working with quotients, specifically `ConnectedComponents` of a `TopologicalSpace`. Additionally, I need `equivSigmaToSet` (in `Data/Setoid/Basic`) to prove things about `SimpleGraph.ConnectedComponent`. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-author awaiting-zulip t-data 179/0 Mathlib/Data/Quot.lean,Mathlib/Data/Set/Image.lean,Mathlib/Data/SetLike/Basic.lean,Mathlib/Data/Setoid/Basic.lean 4 3 ['TwoFX', 'eric-wieser', 'github-actions'] TwoFX
assignee:TwoFX
16-14312
16 days ago
16-14312
16 days ago
36-69524
36 days
30668 astrainfinita
author:astrainfinita
 feat: `QuotType` This typeclass is primarily for use by type synonyms of `Quot` and `Quotient`. Using `QuotType` API for type synonyms of `Quot` and `Quotient` will avoid defeq abuse caused by directly using `Quot` and `Quotient` APIs. This PR also adds some typeclasses to support different ways to find the quotient map that should be used. See the documentation comments of these typeclasses for examples of usage. --- It's not a typical design to use these auxiliary typeclasses and term elaborators, but I haven't found a better way to support these notations. Some of the naming may need to be discussed. For example: - `⟦·⟧` is currently called `mkQ` in names. This distinguishes it from other `.mk`s and makes it possible to write the quotient map as `mkQ` `mkQ'` ~~`mkQ_ h`~~. But this will also require changing the old lemma names. - It would be helpful if the names of new type classes explained their functionality better. [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/migrate.20to.20.60QuotLike.60.20API) This PR continues the work from #16421. Original PR: https://github.com/leanprover-community/mathlib4/pull/16421 RFC awaiting-zulip t-data 629/0 Mathlib.lean,Mathlib/Data/QuotType.lean,MathlibTest/QuotType.lean 3 20 ['YaelDillies', 'astrainfinita', 'github-actions', 'mathlib4-merge-conflict-bot', 'plp127', 'vihdzp'] nobody
2-55636
2 days ago
3-702
3 days ago
0-81
1 minute
30526 SnirBroshi
author:SnirBroshi
 chore(Logic/Relation): use `Subrelation` to state theorems chore(Logic/Relation): replace every `∀ x y, r x y → r' x y` with `Subrelation r r'` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip 79/73 Mathlib/CategoryTheory/IsConnected.lean,Mathlib/CategoryTheory/Limits/Types/Coequalizers.lean,Mathlib/CategoryTheory/Limits/Types/Filtered.lean,Mathlib/Data/Setoid/Basic.lean,Mathlib/GroupTheory/FreeGroup/Basic.lean,Mathlib/Logic/Relation.lean,Mathlib/Order/Interval/Finset/Basic.lean 7 5 ['SnirBroshi', 'github-actions', 'mathlib4-merge-conflict-bot', 'thorimur', 'vihdzp'] thorimur
assignee:thorimur
25-73892
25 days ago
25-73912
25 days ago
8-76821
8 days
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/) merge-conflict t-algebra t-order awaiting-zulip
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
387-85190
1 year ago
387-85190
1 year 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 merge-conflict t-analysis awaiting-zulip 432/387 Mathlib/Analysis/CStarAlgebra/Exponential.lean,Mathlib/Analysis/CStarAlgebra/Spectrum.lean,Mathlib/Analysis/Normed/Algebra/Exponential.lean,Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean,Mathlib/Analysis/Normed/Algebra/QuaternionExponential.lean,Mathlib/Analysis/Normed/Algebra/Spectrum.lean,Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean,Mathlib/Analysis/NormedSpace/DualNumber.lean,Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean,Mathlib/Analysis/SpecialFunctions/Exponential.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Series.lean 11 29 ['YaelDillies', 'eric-wieser', 'girving', 'github-actions', 'j-loreaux', 'kbuzzard', 'leanprover-community-bot-assistant', 'urkud'] nobody
232-40567
7 months ago
243-69197
7 months ago
29-60989
29 days
17458 urkud
author:urkud
 refactor(Algebra/Group): make `IsUnit` a typeclass Also change some lemmas to assume `[IsUnit _]` instead of `[Invertible _]`. Motivated by potential non-defeq diamonds in #14986, see also [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Invertible.20and.20data) I no longer plan to merge this PR, but I'm going to cherry-pick some changes to a new PR before closing this one. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) merge-conflict t-algebra awaiting-zulip
label:t-algebra$
 82/72 Mathlib/Algebra/CharP/Invertible.lean,Mathlib/Algebra/Group/Invertible/Basic.lean,Mathlib/Algebra/Group/Units/Defs.lean,Mathlib/Algebra/GroupWithZero/Invertible.lean,Mathlib/Algebra/GroupWithZero/Units/Basic.lean,Mathlib/Algebra/Polynomial/Degree/Units.lean,Mathlib/Algebra/Polynomial/Splits.lean,Mathlib/Analysis/Convex/Segment.lean,Mathlib/Analysis/Normed/Affine/Isometry.lean,Mathlib/Analysis/Normed/Ring/Units.lean,Mathlib/CategoryTheory/Linear/Basic.lean,Mathlib/FieldTheory/Finite/Basic.lean,Mathlib/FieldTheory/Separable.lean,Mathlib/FieldTheory/SeparableDegree.lean,Mathlib/GroupTheory/Submonoid/Inverses.lean,Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean,Mathlib/LinearAlgebra/AffineSpace/Combination.lean,Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean,Mathlib/LinearAlgebra/CliffordAlgebra/Inversion.lean,Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean,Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean,Mathlib/NumberTheory/MulChar/Basic.lean,Mathlib/RingTheory/Localization/NumDen.lean,Mathlib/RingTheory/Polynomial/Content.lean,Mathlib/RingTheory/Polynomial/GaussLemma.lean,Mathlib/RingTheory/Valuation/Basic.lean 26 12 ['MichaelStollBayreuth', 'acmepjz', 'eric-wieser', 'github-actions', 'leanprover-bot', 'leanprover-community-bot-assistant', 'urkud'] nobody
161-28816
5 months ago
161-28816
5 months ago
0-66650
18 hours
15651 TpmKranz
author:TpmKranz
 feat(Computability/NFA): operations for Thompson's construction Lays the groundwork for a proof of equivalence of RE and NFA, w.r.t. described language. Actual connection to REs comes later, after the groundwork for the opposite direction has been laid. Third chunk of #12648 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-author merge-conflict new-contributor t-computability awaiting-zulip 307/5 Mathlib/Computability/NFA.lean 1 27 ['TpmKranz', 'YaelDillies', 'dupuisf', 'github-actions', 'leanprover-community-bot-assistant', 'meithecatte', 'rudynicolop'] nobody
25-48515
25 days ago
207-71074
6 months ago
45-84611
45 days
15649 TpmKranz
author:TpmKranz
 feat(Computability): introduce Generalised NFA as bridge to Regular Expression Lays the groundwork for a proof of equivalence of NFA and RE, w.r.t. described language. Actual connection to NFA comes later, after the groundwork for the opposite direction has been laid. Second chunk of #12648 --- - [x] depends on: #15647 [Data.FinEnum.Option unchanged since then] [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-author merge-conflict new-contributor t-computability awaiting-zulip 298/0 Mathlib.lean,Mathlib/Computability/GNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/RegularExpressions.lean,docs/references.bib 5 7 ['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'meithecatte', 'trivial1711'] nobody
24-64756
24 days ago
24-64757
24 days ago
23-54870
23 days
20238 maemre
author:maemre
 feat(Computability/DFA): Closure of regular languages under some set operations This shows that regular languages are closed under complement and intersection by constructing DFAs for them. --- Closure under all other operations will be proved when someone adds the proof for DFA<->regular expression equivalence, so they are not part of this PR. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-author merge-conflict new-contributor t-computability awaiting-zulip 159/0 Mathlib/Computability/DFA.lean,Mathlib/Computability/Language.lean 2 60 ['EtienneC30', 'YaelDillies', 'github-actions', 'maemre', 'mathlib4-merge-conflict-bot', 'meithecatte', 'urkud'] EtienneC30
assignee:EtienneC30
24-63846
24 days ago
24-63847
24 days ago
48-67492
48 days
11800 JADekker
author:JADekker
 feat: 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/) please-adopt merge-conflict t-topology awaiting-zulip 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
23-73790
23 days ago
453-47515
1 year ago
119-10687
119 days
25218 kckennylau
author:kckennylau
 feat(AlgebraicGeometry): Tate normal form of elliptic curves --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) merge-conflict t-algebraic-geometry new-contributor awaiting-zulip 291/26 Mathlib.lean,Mathlib/AlgebraicGeometry/EllipticCurve/IsomOfJ.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Modular/TateNormalForm.lean,Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean,Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean 5 31 ['MichaelStollBayreuth', 'Multramate', 'acmepjz', 'github-actions', 'grunweg', 'kckennylau', 'leanprover-community-bot-assistant'] nobody
161-27654
5 months ago
161-27655
5 months ago
6-51040
6 days
28803 astrainfinita
author:astrainfinita
 refactor: unbundle algebra from `ENormed*` Further speed up the search in the algebraic typeclass hierarchy by avoiding searching for `TopologicalSpace`. This PR continues the work from #23961. - Change `ESeminormed(Add)Monoid` and `ENormed(Add)Monoid` so they no longer carry algebraic data. - Deprecate `ESeminormed(Add)CommMonoid` and `ENormed(Add)CommMonoid` in favor of `ESeminormed(Add)Monoid` and `ENormed(Add)Monoid` with a commutative algebraic typeclass. |Old|New| |---|---| | `[ESeminormed(Add)(Comm)Monoid E]` | `[(Add)(Comm)Monoid E] [ESeminormed(Add)Monoid E]` | | `[ENormed(Add)(Comm)Monoid]` | `[(Add)(Comm)Monoid E] [ENormed(Add)Monoid]` | See [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2328803.20refactor.3A.20unbundle.20algebra.20from.20.60ENormed*.60/with/536024350) ------------ - [x] depends on: #28813 merge-conflict t-analysis t-algebra slow-typeclass-synthesis awaiting-zulip
label:t-algebra$
 80/63 Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/Analysis/Normed/Group/Continuity.lean,Mathlib/Analysis/Normed/Group/InfiniteSum.lean,Mathlib/Analysis/NormedSpace/IndicatorFunction.lean,Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean,Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean,Mathlib/MeasureTheory/Function/L1Space/Integrable.lean,Mathlib/MeasureTheory/Function/LocallyIntegrable.lean,Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean,Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean,Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean,Mathlib/MeasureTheory/Integral/IntegrableOn.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean 14 28 ['astrainfinita', 'bryangingechen', 'github-actions', 'grunweg', 'kbuzzard', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib-bors', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'sgouezel'] grunweg
assignee:grunweg
101-43299
3 months ago
101-43300
3 months ago
0-20585
5 hours
28925 grunweg
author:grunweg
 chore: remove `linear_combination'` tactic When `linear_combination` was refactored in #15899, the old code was kept as the `linear_combination'` tactic, for easier migration. The consensus of the zulip discussion ([#mathlib4 > Narrowing the scope of `linear_combination` @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Narrowing.20the.20scope.20of.20.60linear_combination.60/near/470237816)) was to wait, and "revisit this once people have experienced the various tactics in practice". One year later, the old tactic has almost no uses: it is unused in mathlib; [searching on github](https://github.com/search?q=linear_combination%27%20path%3A*.lean&type=code) yields 37 hits --- all of which are in various forks of mathlib. Thus, removing this tactic seems appropriate. --- Do not merge before the zulip discussion has concluded! [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) merge-conflict awaiting-zulip file-removed 0/564 Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/LinearCombination'.lean,Mathlib/Tactic/Linter/UnusedTactic.lean,MathlibTest/linear_combination'.lean 5 4 ['euprunin', 'github-actions', 'grunweg', 'mathlib4-merge-conflict-bot'] nobody
58-20509
1 month ago
58-20510
1 month ago
0-1
1 second
22361 rudynicolop
author:rudynicolop
 feat(Computability/NFA): nfa closure properties Add the closure properties union, intersection and reversal for NFA. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-author merge-conflict new-contributor t-computability awaiting-zulip 218/2 Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean 2 91 ['EtienneC30', 'b-mehta', 'ctchou', 'github-actions', 'leanprover-community-bot-assistant', 'meithecatte', 'rudynicolop'] EtienneC30
assignee:EtienneC30
39-30199
1 month ago
207-70149
6 months ago
39-67601
39 days
30150 imbrem
author:imbrem
 feat(CategoryTheory/Monoidal): to_additive for MonoidalCategory Add `AddMonoidalCategory`, the additive version of `MonoidalCategory`. To get this to work, I needed to _remove_ the `to_additive` attributes in `Discrete.lean`, since existing code relies on the `AddMonoid M → MonoidalCategory M` instance. For now, we simply implement the additive variants by hand instead. --- As discussed in #28718; I added an `AddMonoidalCategory` struct and tagged `MonoidalCategory` with `to_additive`, along with the lemmas in `Category.lean`. I think this is the right approach, since under this framework the "correct" additive version of `Discrete.lean` would be mapping an `AddMonoid` to an `AddMonoidalCategory`. Next steps would be to: - Make `monoidal_coherence` and `coherence` support `AddMonoidalCategory` - Add `CocartesianMonoidalCategory` extending `AddMonoidalCategory` [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) merge-conflict t-meta t-category-theory new-contributor awaiting-zulip large-import 444/125 Mathlib/CategoryTheory/Monoidal/Category.lean,Mathlib/CategoryTheory/Monoidal/Discrete.lean,Mathlib/Tactic/ToAdditive/GuessName.lean 3 22 ['JovanGerb', 'YaelDillies', 'github-actions', 'imbrem', 'mathlib4-merge-conflict-bot'] nobody
30-31383
1 month ago
30-31383
1 month ago
1-18384
1 day
20648 anthonyde
author:anthonyde
 feat: formalize regular expression -> εNFA The file `Computability/RegularExpressionsToEpsilonNFA.lean` contains a formal definition of Thompson's method for constructing an `εNFA` from a `RegularExpression` and a proof of its correctness. --- - [x] depends on: #20644 - [x] depends on: #20645 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) merge-conflict new-contributor t-computability awaiting-zulip 490/0 Mathlib.lean,Mathlib/Computability/RegularExpressionsToEpsilonNFA.lean,docs/references.bib 3 7 ['anthonyde', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'meithecatte', 'qawbecrdtey'] nobody
24-15524
24 days ago
24-15525
24 days ago
75-77754
75 days
24614 JovanGerb
author:JovanGerb
 chore: rename field `inf` to `min` in `Lattice` As suggested by @eric-wieser, this PR renames the `sup` and `inf` fields in `Lattice` to `max` and `min`. This means that we now can extend `Lattice` and `LinearOrder` simultaneously without ending up with duplicate fields. This should be implemented in a future PR for existing classes like `CompleteLinearOrder`. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60sup.60.2F.60inf.60.20or.20.60max.60.2F.60min.60.20for.20set.20interval.20lemmas.3F) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) merge-conflict t-order awaiting-zulip 175/181 Mathlib/Algebra/Field/Subfield/Basic.lean,Mathlib/Algebra/Group/Subgroup/Lattice.lean,Mathlib/Algebra/Group/Submonoid/Basic.lean,Mathlib/Algebra/Group/Subsemigroup/Basic.lean,Mathlib/Algebra/Lie/Subalgebra.lean,Mathlib/Algebra/Module/Submodule/Lattice.lean,Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/Kleene.lean,Mathlib/Algebra/Order/Ring/Idempotent.lean,Mathlib/Algebra/Ring/Subring/Basic.lean,Mathlib/Algebra/Ring/Subsemiring/Basic.lean,Mathlib/Algebra/Tropical/Lattice.lean,Mathlib/AlgebraicGeometry/IdealSheaf/Basic.lean,Mathlib/Analysis/BoxIntegral/Box/Basic.lean,Mathlib/Analysis/BoxIntegral/Partition/Basic.lean,Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean,Mathlib/Analysis/Normed/Group/Seminorm.lean,Mathlib/Analysis/NormedSpace/ENormedSpace.lean,Mathlib/Analysis/NormedSpace/MStructure.lean,Mathlib/Analysis/Seminorm.lean,Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean,Mathlib/CategoryTheory/Sites/Coverage.lean,Mathlib/CategoryTheory/Sites/Grothendieck.lean,Mathlib/CategoryTheory/Sites/Pretopology.lean,Mathlib/CategoryTheory/Sites/Sieves.lean,Mathlib/CategoryTheory/Subobject/Lattice.lean,Mathlib/CategoryTheory/Subpresheaf/Basic.lean,Mathlib/Computability/Reduce.lean,Mathlib/Data/DFinsupp/Order.lean,Mathlib/Data/Finset/Lattice/Basic.lean,Mathlib/Data/Multiset/UnionInter.lean,Mathlib/Data/Nat/PartENat.lean,Mathlib/Data/PEquiv.lean,Mathlib/Data/Real/Basic.lean,Mathlib/Data/Semiquot.lean,Mathlib/Data/Set/Basic.lean,Mathlib/Data/Setoid/Basic.lean,Mathlib/Data/Sum/Lattice.lean,Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean,Mathlib/Geometry/Manifold/ChartedSpace.lean,Mathlib/GroupTheory/Congruence/Defs.lean,Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean,Mathlib/LinearAlgebra/LinearPMap.lean,Mathlib/MeasureTheory/Function/AEEqFun.lean,Mathlib/MeasureTheory/Function/SimpleFunc.lean,Mathlib/ModelTheory/Substructures.lean,Mathlib/Order/BooleanSubalgebra.lean,Mathlib/Order/Booleanisation.lean,Mathlib/Order/CompleteLattice/Defs.lean,Mathlib/Order/Concept.lean,Mathlib/Order/ConditionallyCompleteLattice/Defs.lean,Mathlib/Order/Copy.lean,Mathlib/Order/Filter/Basic.lean,Mathlib/Order/Filter/Germ/Basic.lean,Mathlib/Order/FixedPoints.lean,Mathlib/Order/GaloisConnection/Basic.lean,Mathlib/Order/Heyting/Basic.lean,Mathlib/Order/Hom/Order.lean,Mathlib/Order/Ideal.lean,Mathlib/Order/Interval/Basic.lean,Mathlib/Order/Lattice.lean,Mathlib/Order/Partition/Finpartition.lean,Mathlib/Order/Preorder/Finsupp.lean,Mathlib/Order/PropInstances.lean,Mathlib/Order/Sublattice.lean,Mathlib/Order/WithBot.lean,Mathlib/Probability/Process/Filtration.lean,Mathlib/RingTheory/Congruence/Basic.lean,Mathlib/RingTheory/Finiteness/Basic.lean,Mathlib/RingTheory/Finiteness/Small.lean,Mathlib/RingTheory/NonUnitalSubring/Basic.lean,Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean,Mathlib/RingTheory/TwoSidedIdeal/Lattice.lean,Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean,Mathlib/RingTheory/Valuation/ValuationSubring.lean,Mathlib/Topology/Algebra/Group/GroupTopology.lean,Mathlib/Topology/Algebra/Module/ClosedSubmodule.lean,Mathlib/Topology/Category/TopCat/OpenNhds.lean,Mathlib/Topology/LocallyFinsupp.lean,Mathlib/Topology/MetricSpace/BundledFun.lean,Mathlib/Topology/UniformSpace/Basic.lean 81 18 ['JovanGerb', 'bryangingechen', 'eric-wieser', 'github-actions', 'j-loreaux', 'leanprover-bot', 'leanprover-community-bot-assistant', 'leanprover-community-mathlib4-bot', 'mathlib4-merge-conflict-bot'] Vierkantor
assignee:Vierkantor
21-73594
21 days ago
21-73595
21 days ago
24-8021
24 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 blocked-by-other-PR merge-conflict t-linter awaiting-zulip 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
405-65659
1 year ago
431-54181
1 year ago*
0-0
0 seconds*
15654 TpmKranz
author:TpmKranz
 feat(Computability): language-preserving maps between NFA and RE Map REs to NFAs via Thompson's construction and NFAs to REs using GNFAs Last chunk of #12648 --- - [ ] depends on: #15651 - [ ] depends on: #15649 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) blocked-by-other-PR merge-conflict new-contributor t-computability awaiting-zulip 985/2 Mathlib.lean,Mathlib/Computability/GNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean,Mathlib/Computability/RegularExpressions.lean,Mathlib/Data/FinEnum/Option.lean,docs/references.bib 7 3 ['github-actions', 'leanprover-community-mathlib4-bot', 'meithecatte'] nobody
221-48467
7 months ago
221-48472
7 months ago
0-179
2 minutes

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

There are currently no PRs on the review queue which are labelled 'tech debt' or 'longest-pole. Congratulations!