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 14, 2025 at 11:13 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
9-2318
9 days ago
9-2318
9 days ago
16-68003
16 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
4-1602
4 days ago
4-1602
4 days ago
8-10695
8 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
2-54166
2 days ago
2-54166
2 days 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
2-7015
2 days ago
2-7015
2 days 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
1-66056
1 day ago
1-66056
1 day ago
1-74279
1 day
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
1-63526
1 day ago
1-63526
1 day ago
6-35060
6 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
1-52375
1 day ago
1-52375
1 day ago
2-65565
2 days
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
1-48993
1 day ago
1-48993
1 day ago
1-63671
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 maintainer-merge large-import 4/7 Mathlib/Tactic/TypeStar.lean 1 5 ['JovanGerb', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] dwrensha
assignee:dwrensha
1-48833
1 day ago
1-48833
1 day ago
12-17825
12 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
1-48162
1 day ago
6-3019
6 days ago
15-84731
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
1-21349
1 day ago
1-21349
1 day ago
2-57254
2 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
9-2318
9 days ago
9-2318
9 days ago
16-68003
16 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
4-1602
4 days ago
4-1602
4 days ago
8-10695
8 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
2-54166
2 days ago
2-54166
2 days 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
2-7015
2 days ago
2-7015
2 days 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
1-66056
1 day ago
1-66056
1 day ago
1-74279
1 day
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
1-63526
1 day ago
1-63526
1 day ago
6-35060
6 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
1-52375
1 day ago
1-52375
1 day ago
2-65565
2 days
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
1-48993
1 day ago
1-48993
1 day ago
1-63671
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 maintainer-merge large-import 4/7 Mathlib/Tactic/TypeStar.lean 1 5 ['JovanGerb', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] dwrensha
assignee:dwrensha
1-48833
1 day ago
1-48833
1 day ago
12-17825
12 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
1-48162
1 day ago
6-3019
6 days ago
15-84731
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
1-21349
1 day ago
1-21349
1 day ago
2-57254
2 days
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/) t-number-theory maintainer-merge large-import 224/5 Mathlib.lean,Mathlib/NumberTheory/ModularForms/EisensteinSeries/E2/Defs.lean,Mathlib/NumberTheory/ModularForms/EisensteinSeries/E2/Summable.lean,Mathlib/Topology/Algebra/InfiniteSum/ConditionalInt.lean 4 25 ['CBirkbeck', 'github-actions', 'loefflerd'] nobody
0-81719
22 hours ago
0-85993
23 hours ago
4-5716
4 days
32300 bjornsolheim
author:bjornsolheim
 feat(Geometry/Convex/Cone): define and characterize generating convex cone Define the notion of a generating convex cone. Prove some initial simple lemmas about generating cones. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) new-contributor maintainer-merge t-convex-geometry 90/0 Mathlib/Geometry/Convex/Cone/Basic.lean 1 17 ['bjornsolheim', 'github-actions', 'ocfnash'] nobody
0-81431
22 hours ago
0-81431
22 hours ago
11-80085
11 days
31505 dsfxcimk
author:dsfxcimk
 feat: Add some oangle theorems Add several theorems relating oriented angles and affine independence / collinearity, together with auxiliary lemmas about the equality and sign of oriented angles. Main additions `oangle_ne_zero_and_ne_pi_iff_not_collinear` – An oriented angle is neither `0` nor `π` if and only if the three points are not collinear. `affineIndependent_iff_of_oangle_eq` – If two oriented angles are equal, then the corresponding triples of points are affinely independent simultaneously. `not_collinear_iff_of_angle_eq` – If two oriented angles are equal, one triple is collinear if and only if the other is. `oangle_eq_or_eq_neg_of_angle_eq` – The oriented angles are equal or opposite if the unoriented angles are equal. `angle_eq_neg_of_two_zsmul_angle_eq` – If `2 • a = 2 • b` and the signs are opposite, then `a = b + π.` `two_zsmul_eq_iff_eq` – Characterizes equality of doubled angles when signs are equal. `oangle_sub_oangle_ne_pi_of_not_collinear` – If the signs of two oriented angles are equal and the points are not collinear, their difference is not `π`. t-euclidean-geometry new-contributor maintainer-merge 55/0 Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean,Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean 2 35 ['dsfxcimk', 'github-actions', 'jsm28'] nobody
0-58161
16 hours ago
0-58161
16 hours ago
3-67985
3 days
32703 chrisflav
author:chrisflav
 chore(RingTheory): rename `RingHom.specComap` to `PrimeSpectrum.comap` and remove the old `PrimeSpectrum.comap`, which was `RingHom.specComap` bundled as a continuous map. Having both `RingHom.specComap` and `PrimeSpectrum.comap` leads to two ways of writing the same thing, with every lemma written before the topology-on-`PrimeSpectrum`-barrier stated in terms of `RingHom.specComap` and most lemmas after it stated in terms of `PrimeSpectrum.comap`. Since the bundled continuous map version is not useful, because the topology library rarely takes continuous maps as input, we remove the bundled version, but keep the name `PrimeSpectrum.comap` for the unbundled one. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-ring-theory 195/182 Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean,Mathlib/AlgebraicGeometry/IdealSheaf/Basic.lean,Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean,Mathlib/AlgebraicGeometry/Morphisms/UniversallyClosed.lean,Mathlib/AlgebraicGeometry/Scheme.lean,Mathlib/AlgebraicGeometry/Spec.lean,Mathlib/AlgebraicGeometry/StructureSheaf.lean,Mathlib/RingTheory/Flat/FaithfullyFlat/Algebra.lean,Mathlib/RingTheory/Ideal/GoingDown.lean,Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean,Mathlib/RingTheory/KrullDimension/Polynomial.lean,Mathlib/RingTheory/LocalRing/ResidueField/Fiber.lean,Mathlib/RingTheory/RingHom/FaithfullyFlat.lean,Mathlib/RingTheory/Spectrum/Maximal/Localization.lean,Mathlib/RingTheory/Spectrum/Prime/Chevalley.lean,Mathlib/RingTheory/Spectrum/Prime/ChevalleyComplexity.lean,Mathlib/RingTheory/Spectrum/Prime/ConstructibleSet.lean,Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean,Mathlib/RingTheory/Spectrum/Prime/Homeomorph.lean,Mathlib/RingTheory/Spectrum/Prime/Polynomial.lean,Mathlib/RingTheory/Spectrum/Prime/RingHom.lean,Mathlib/RingTheory/Spectrum/Prime/TensorProduct.lean,Mathlib/RingTheory/Spectrum/Prime/Topology.lean,docs/1000.yaml 24 9 ['chrisflav', 'erdOne', 'github-actions', 'leanprover-radar'] nobody
0-57507
15 hours ago
0-57507
15 hours ago
3-46438
3 days
32801 Hagb
author:Hagb
 feat(RingTheory/MvPolynomial/Ideal): `sPolynomial` preserves ideal membership It will be used by Buchberger's Criterion (in #29203). --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-ring-theory 10/0 Mathlib/RingTheory/MvPolynomial/Ideal.lean 1 2 ['erdOne', 'github-actions'] nobody
0-57284
15 hours ago
0-57284
15 hours ago
1-67211
1 day
32479 WenrongZou
author:WenrongZou
 feat(RingTheory/PowerSeries/Substitution): add `le_order_subst` I add a theorem saying multiplication of order less than the order of substitution. I tried to put at the file `PowerSeries.Order`, but it seems like in this file we already import `PowerSeries.Substitution`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) new-contributor maintainer-merge t-ring-theory 71/0 Mathlib/RingTheory/MvPowerSeries/Substitution.lean,Mathlib/RingTheory/PowerSeries/Order.lean,Mathlib/RingTheory/PowerSeries/Substitution.lean 3 22 ['AntoineChambert-Loir', 'WenrongZou', 'erdOne', 'github-actions'] chrisflav
assignee:chrisflav
0-56824
15 hours ago
0-57768
16 hours ago
7-48236
7 days
32789 harahu
author:harahu
 doc(RingTheory): 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-ring-theory 29/30 Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean,Mathlib/RingTheory/AdicCompletion/Basic.lean,Mathlib/RingTheory/AdicCompletion/RingHom.lean,Mathlib/RingTheory/Conductor.lean,Mathlib/RingTheory/Congruence/Hom.lean,Mathlib/RingTheory/DedekindDomain/Factorization.lean,Mathlib/RingTheory/DividedPowers/Basic.lean,Mathlib/RingTheory/Etale/StandardEtale.lean,Mathlib/RingTheory/Extension/Generators.lean,Mathlib/RingTheory/Extension/Presentation/Basic.lean,Mathlib/RingTheory/FiniteType.lean,Mathlib/RingTheory/Flat/Basic.lean,Mathlib/RingTheory/Ideal/Over.lean,Mathlib/RingTheory/Ideal/Quotient/Operations.lean,Mathlib/RingTheory/Localization/LocalizationLocalization.lean,Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean,Mathlib/RingTheory/MvPowerSeries/Trunc.lean,Mathlib/RingTheory/NonUnitalSubring/Basic.lean,Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean,Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean,Mathlib/RingTheory/SimpleRing/Congr.lean,Mathlib/RingTheory/Valuation/Basic.lean,Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean 23 4 ['erdOne', 'github-actions', 'harahu'] nobody
0-51603
14 hours ago
0-51603
14 hours ago
2-3782
2 days
32492 bjornsolheim
author:bjornsolheim
 feat(LinearAlgebra/TensorProduct): explicit tensor product decomposition in a finite basis * Given a finite basis `ℬ` for `M`, any tensor `x ∈ M ⊗ N` decomposes as `∑ᵢ ℬᵢ ⊗ₜ nᵢ` where the `N`-component `nᵢ` is obtained by applying `ℬ.coord i ⊗ id` to `x` and then identifying `R ⊗ N ≃ N` via `lid`. * Similarly for the right hand tensor product component version. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebra new-contributor
label:t-algebra$
 20/0 Mathlib/LinearAlgebra/TensorProduct/Basis.lean 1 16 ['bjornsolheim', 'erdOne', 'github-actions', 'robin-carlier', 'themathqueen'] erdOne
assignee:erdOne
0-59745
16 hours ago
1-47495
1 day ago
7-85414
7 days
32787 Hagb
author:Hagb
 feat(RingTheory/MvPolynomial/MonomialOrder): add several lemmas about `leadingTerm` and inequality on degree Some of them were abstracted from a proof of Buchberger's Criterion (#29203). --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-ring-theory 34/0 Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean 1 3 ['erdOne', 'github-actions'] nobody
0-48873
13 hours ago
0-48873
13 hours ago
2-5629
2 days
32640 vihdzp
author:vihdzp
 feat: cardinality of Hahn series This is a very preliminary development; most of the PR is really just lemmas about `HahnSeries.support`. This will be needed in the CGT repo, to define surreal Hahn series as the subfield of real, small Hahn series over their own order dual. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebra maintainer-merge t-ring-theory
label:t-algebra$
 148/35 Mathlib.lean,Mathlib/RingTheory/HahnSeries/Addition.lean,Mathlib/RingTheory/HahnSeries/Basic.lean,Mathlib/RingTheory/HahnSeries/Cardinal.lean,Mathlib/RingTheory/HahnSeries/Multiplication.lean,Mathlib/RingTheory/HahnSeries/Summable.lean 6 8 ['erdOne', 'github-actions', 'mathlib4-merge-conflict-bot', 'vihdzp', 'wwylele'] nobody
0-42504
11 hours ago
0-42504
11 hours ago
4-69865
4 days
32788 Hagb
author:Hagb
 feat(RingTheory/MvPolynomial/MonomialOrder): add some variants of `sPolynomial_mul_monomial` This commit adds a variant `sPolynomial_mul_monomial'`, using `m.degree (monomial d c * p)` instead of `d + m.degree p`, which are different in the edge case that one of `c` and `p` is 0. A pair of variants about `leadingTerm` instead of `monomial` are also added. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-ring-theory 30/0 Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean 1 3 ['erdOne', 'github-actions'] nobody
0-42409
11 hours ago
0-42409
11 hours ago
2-4740
2 days
32118 alreadydone
author:alreadydone
 feat(Algebra): prerequisites for #31919 + Extract a lemma `exists_aeval_invOf_eq_zero_of_ideal_map_adjoin_add_span_eq_top` that was used in the proof of [stacks#00IB](https://stacks.math.columbia.edu/tag/00IB) and are used to prove both parts of [stacks#090P](https://stacks.math.columbia.edu/tag/090P) + Add lemmas on units in a submonoid of a DivisionMonoid/Group(WithZero) + Add instances for `integralClosure` and API for integrally closed subrings + Add a lemma on `trailingCoeff` of polynomials + Fix a statement in `local_hom_TFAE` and rename to `isLocalHom_tfae` + Unify the instances `Algebra.ofSubsemiring` and `Algebra.ofSubring` + Move `NonUnitalSub(semi)ringClass` instance on `Ideal` to from Ideal/Operations to Defs + Upgrade `ValuationSubring.nonunits` from `Subsemigroup` to `NonUnitalSubring` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebra maintainer-merge t-ring-theory
label:t-algebra$
 161/39 Mathlib/Algebra/Algebra/Basic.lean,Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean,Mathlib/NumberTheory/Padics/PadicIntegers.lean,Mathlib/RingTheory/Ideal/Nonunits.lean,Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean,Mathlib/RingTheory/LocalRing/LocalSubring.lean,Mathlib/RingTheory/LocalRing/RingHom/Basic.lean,Mathlib/RingTheory/Polynomial/Basic.lean,Mathlib/RingTheory/Polynomial/Ideal.lean,Mathlib/RingTheory/Valuation/AlgebraInstances.lean,Mathlib/RingTheory/Valuation/Integers.lean,Mathlib/RingTheory/Valuation/ValuationSubring.lean 12 39 ['alreadydone', 'erdOne', 'github-actions', 'jcommelin', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'leanprover-radar'] mattrobball
assignee:mattrobball
0-42113
11 hours ago
0-42113
11 hours ago
10-46277
10 days
32360 YuvalFilmus
author:YuvalFilmus
 feat(Chebyshev): degree, leadingCoeff, eval_neg Calculated the degree and leading coefficients of Chebyshev T and U, as well as formulas for T(-x) and U(-x). --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) new-contributor maintainer-merge t-ring-theory 152/2 Mathlib/RingTheory/Polynomial/Chebyshev.lean 1 11 ['LLaurance', 'YuvalFilmus', 'erdOne', 'github-actions'] kbuzzard
assignee:kbuzzard
0-16652
4 hours ago
0-48570
13 hours ago
9-48995
9 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
189-55452
6 months ago
189-55453
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
49-52016
1 month ago
49-52273
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
21-81018
21 days ago
21-81018
21 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
17-11695
17 days ago
17-11695
17 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
3-53019
3 days ago
3-84485
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/) t-logic 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
1-15246
1 day ago
1-15246
1 day 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
388-82573
1 year ago
388-82573
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
233-37950
7 months ago
244-66580
8 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
162-26199
5 months ago
162-26199
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
26-45898
26 days ago
208-68457
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
25-62139
25 days ago
25-62140
25 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
25-61229
25 days ago
25-61230
25 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
24-71173
24 days ago
454-44898
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
162-25037
5 months ago
162-25038
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
102-40682
3 months ago
102-40683
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
59-17892
1 month ago
59-17893
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
40-27582
1 month ago
208-67532
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
31-28766
1 month ago
31-28766
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
25-12907
25 days ago
25-12908
25 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
22-70977
22 days ago
22-70978
22 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
406-63042
1 year ago
432-51564
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
222-45850
7 months ago
222-45855
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!