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 25, 2025 at 09:44 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
32835 vasnesterov
author:vasnesterov
 fix(Tactic/Order): equal but not syntactically equal types When collecting atoms, `order` relies only on syntactic equality of types. This PR replaces this with defeq check and adds a test that failed before. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) bug t-meta maintainer-merge 18/1 Mathlib/Tactic/Order/CollectFacts.lean,MathlibTest/order.lean 2 3 ['artie2000', 'github-actions', 'j-loreaux'] thorimur
assignee:thorimur
7-2331
7 days ago
7-50383
7 days ago
11-73556
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 63 ['YaelDillies', 'ctchou', 'github-actions', 'lambda-fairy', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'rudynicolop'] YaelDillies
assignee:YaelDillies
5-39377
5 days ago
6-19832
6 days ago
24-31734
24 days
31315 Parcly-Taxel
author:Parcly-Taxel
 feat: IMO 2010 Q5 See [#general > Panic in rw: Nat.pow exponent is too big @ 💬](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Panic.20in.20rw.3A.20Nat.2Epow.20exponent.20is.20too.20big/near/513294906) and leanprover/lean4#11713 for why 2010 and 11 are replaced with variables. maintainer-merge IMO 245/0 Archive.lean,Archive/Imo/Imo2010Q5.lean 2 6 ['Parcly-Taxel', 'github-actions', 'jsm28', 'nomeata'] jsm28
assignee:jsm28
3-31398
3 days ago
6-35684
6 days ago
28-32766
28 days
33156 JovanGerb
author:JovanGerb
 feat(AddRelatedDecl): define `optAttrArg` syntax and use it This PR gives a name to the often used `(attr := ...)` syntax, cleaning up the code --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-meta maintainer-merge 29/28 Mathlib/Order/Defs/Unbundled.lean,Mathlib/Tactic/CategoryTheory/Elementwise.lean,Mathlib/Tactic/CategoryTheory/Reassoc.lean,Mathlib/Tactic/CategoryTheory/ToApp.lean,Mathlib/Tactic/Simps/Basic.lean,Mathlib/Tactic/ToFun.lean,Mathlib/Util/AddRelatedDecl.lean 7 10 ['JovanGerb', 'github-actions', 'grunweg', 'mathlib4-merge-conflict-bot'] nobody
2-74149
2 days ago
2-74149
2 days ago
3-59629
3 days
31495 jsm28
author:jsm28
 feat(Geometry/Euclidean/Sphere/SecondInter): `secondInter` and sides of faces of a simplex Add lemmas that, if you take a simplex with one vertex on a sphere and the others on or inside it (typically, a triangle and its circumcircle), and take a line through the given vertex and a point in the interior of the simplex or the interior of the opposite face, the second intersection of that line with the sphere lies on the opposite side (from the vertex) of the face opposite that vertex. --- - [ ] depends on: #31451 - [ ] depends on: #31452 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-euclidean-geometry maintainer-merge 52/0 Mathlib/Geometry/Euclidean/Sphere/SecondInter.lean 1 5 ['JovanGerb', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] JovanGerb
assignee:JovanGerb
2-67383
2 days ago
2-67383
2 days ago
19-31216
19 days
31057 jsm28
author:jsm28
 feat(Geometry/Euclidean/Incenter): `reindex` lemmas Add lemmas about all the incenter/excenter-related definitions applied to a reindexed simplex. --- - [x] depends on: #31054 - [x] depends on: #31055 - [x] depends on: #31056 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-euclidean-geometry maintainer-merge 65/1 Mathlib/Geometry/Euclidean/Incenter.lean 1 5 ['JovanGerb', 'github-actions', 'jsm28', 'mathlib4-dependent-issues-bot'] JovanGerb
assignee:JovanGerb
2-64976
2 days ago
2-70213
2 days ago
27-1847
27 days
33160 joelriou
author:joelriou
 feat(CategoryTheory): adjunctions in Cat We show that adjunctions in the bicategory `Cat` correspond to adjunctions between functors in the usual categorical sense. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-category-theory maintainer-merge 110/0 Mathlib.lean,Mathlib/CategoryTheory/Bicategory/Adjunction/Basic.lean,Mathlib/CategoryTheory/Bicategory/Adjunction/Cat.lean 3 3 ['dagurtomas', 'github-actions'] nobody
2-39891
2 days ago
2-39891
2 days ago
3-56234
3 days
33202 joelriou
author:joelriou
 feat(Algebra/Homology): the spectral object with values in the homotopy category We define the precomposition of a spectral object (in a triangulated category) by an arbitrary functor. We also define the spectral object with values in the homotopy category that is indexed by the category of cochain complexes. It follows that to any functor `ι ⥤ CochainComplex C ℤ` (e.g. a filtered complex), there is an associated spectral object indexed by `ι` with values in the homotopy category of `C`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-category-theory maintainer-merge 129/6 Mathlib.lean,Mathlib/Algebra/Homology/HomotopyCategory/SpectralObject.lean,Mathlib/CategoryTheory/ComposableArrows/Basic.lean,Mathlib/CategoryTheory/ComposableArrows/One.lean,Mathlib/CategoryTheory/Triangulated/SpectralObject.lean 5 3 ['dagurtomas', 'github-actions', 'joelriou'] nobody
2-24662
2 days ago
2-24769
2 days ago
2-61359
2 days
30860 FormulaRabbit81
author:FormulaRabbit81
 feat(MeasureTheory): the space of probability measures on a compact space is compact --- - [x] depends on: #30845 - [x] depends on: #28061 - [x] depends on #31656 - [x] depends on #31964 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-measure-probability maintainer-merge 168/24 Mathlib/Algebra/Order/Module/PositiveLinearMap.lean,Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean,Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean,Mathlib/Topology/ContinuousMap/CompactlySupported.lean 4 44 ['FormulaRabbit81', 'YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'sgouezel'] nobody
1-7437
1 day ago
1-40825
1 day ago
5-45343
5 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
32835 vasnesterov
author:vasnesterov
 fix(Tactic/Order): equal but not syntactically equal types When collecting atoms, `order` relies only on syntactic equality of types. This PR replaces this with defeq check and adds a test that failed before. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) bug t-meta maintainer-merge 18/1 Mathlib/Tactic/Order/CollectFacts.lean,MathlibTest/order.lean 2 3 ['artie2000', 'github-actions', 'j-loreaux'] thorimur
assignee:thorimur
7-2331
7 days ago
7-50383
7 days ago
11-73556
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 63 ['YaelDillies', 'ctchou', 'github-actions', 'lambda-fairy', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'rudynicolop'] YaelDillies
assignee:YaelDillies
5-39377
5 days ago
6-19832
6 days ago
24-31734
24 days
31315 Parcly-Taxel
author:Parcly-Taxel
 feat: IMO 2010 Q5 See [#general > Panic in rw: Nat.pow exponent is too big @ 💬](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Panic.20in.20rw.3A.20Nat.2Epow.20exponent.20is.20too.20big/near/513294906) and leanprover/lean4#11713 for why 2010 and 11 are replaced with variables. maintainer-merge IMO 245/0 Archive.lean,Archive/Imo/Imo2010Q5.lean 2 6 ['Parcly-Taxel', 'github-actions', 'jsm28', 'nomeata'] jsm28
assignee:jsm28
3-31398
3 days ago
6-35684
6 days ago
28-32766
28 days
33156 JovanGerb
author:JovanGerb
 feat(AddRelatedDecl): define `optAttrArg` syntax and use it This PR gives a name to the often used `(attr := ...)` syntax, cleaning up the code --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-meta maintainer-merge 29/28 Mathlib/Order/Defs/Unbundled.lean,Mathlib/Tactic/CategoryTheory/Elementwise.lean,Mathlib/Tactic/CategoryTheory/Reassoc.lean,Mathlib/Tactic/CategoryTheory/ToApp.lean,Mathlib/Tactic/Simps/Basic.lean,Mathlib/Tactic/ToFun.lean,Mathlib/Util/AddRelatedDecl.lean 7 10 ['JovanGerb', 'github-actions', 'grunweg', 'mathlib4-merge-conflict-bot'] nobody
2-74149
2 days ago
2-74149
2 days ago
3-59629
3 days
31495 jsm28
author:jsm28
 feat(Geometry/Euclidean/Sphere/SecondInter): `secondInter` and sides of faces of a simplex Add lemmas that, if you take a simplex with one vertex on a sphere and the others on or inside it (typically, a triangle and its circumcircle), and take a line through the given vertex and a point in the interior of the simplex or the interior of the opposite face, the second intersection of that line with the sphere lies on the opposite side (from the vertex) of the face opposite that vertex. --- - [ ] depends on: #31451 - [ ] depends on: #31452 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-euclidean-geometry maintainer-merge 52/0 Mathlib/Geometry/Euclidean/Sphere/SecondInter.lean 1 5 ['JovanGerb', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] JovanGerb
assignee:JovanGerb
2-67383
2 days ago
2-67383
2 days ago
19-31216
19 days
31057 jsm28
author:jsm28
 feat(Geometry/Euclidean/Incenter): `reindex` lemmas Add lemmas about all the incenter/excenter-related definitions applied to a reindexed simplex. --- - [x] depends on: #31054 - [x] depends on: #31055 - [x] depends on: #31056 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-euclidean-geometry maintainer-merge 65/1 Mathlib/Geometry/Euclidean/Incenter.lean 1 5 ['JovanGerb', 'github-actions', 'jsm28', 'mathlib4-dependent-issues-bot'] JovanGerb
assignee:JovanGerb
2-64976
2 days ago
2-70213
2 days ago
27-1847
27 days
33160 joelriou
author:joelriou
 feat(CategoryTheory): adjunctions in Cat We show that adjunctions in the bicategory `Cat` correspond to adjunctions between functors in the usual categorical sense. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-category-theory maintainer-merge 110/0 Mathlib.lean,Mathlib/CategoryTheory/Bicategory/Adjunction/Basic.lean,Mathlib/CategoryTheory/Bicategory/Adjunction/Cat.lean 3 3 ['dagurtomas', 'github-actions'] nobody
2-39891
2 days ago
2-39891
2 days ago
3-56234
3 days
33202 joelriou
author:joelriou
 feat(Algebra/Homology): the spectral object with values in the homotopy category We define the precomposition of a spectral object (in a triangulated category) by an arbitrary functor. We also define the spectral object with values in the homotopy category that is indexed by the category of cochain complexes. It follows that to any functor `ι ⥤ CochainComplex C ℤ` (e.g. a filtered complex), there is an associated spectral object indexed by `ι` with values in the homotopy category of `C`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-category-theory maintainer-merge 129/6 Mathlib.lean,Mathlib/Algebra/Homology/HomotopyCategory/SpectralObject.lean,Mathlib/CategoryTheory/ComposableArrows/Basic.lean,Mathlib/CategoryTheory/ComposableArrows/One.lean,Mathlib/CategoryTheory/Triangulated/SpectralObject.lean 5 3 ['dagurtomas', 'github-actions', 'joelriou'] nobody
2-24662
2 days ago
2-24769
2 days ago
2-61359
2 days
30860 FormulaRabbit81
author:FormulaRabbit81
 feat(MeasureTheory): the space of probability measures on a compact space is compact --- - [x] depends on: #30845 - [x] depends on: #28061 - [x] depends on #31656 - [x] depends on #31964 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-measure-probability maintainer-merge 168/24 Mathlib/Algebra/Order/Module/PositiveLinearMap.lean,Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean,Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean,Mathlib/Topology/ContinuousMap/CompactlySupported.lean 4 44 ['FormulaRabbit81', 'YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'sgouezel'] nobody
1-7437
1 day ago
1-40825
1 day ago
5-45343
5 days
33138 gasparattila
author:gasparattila
 chore(MeasureTheory/Measure/Stieltjes): remove `backward.privateInPublic` In #32482, some definitions in this file were rewritten using private declarations. However, this made `StieltjesFunction.length` unusable, since its API uses private declarations even in statements. This PR fixes this by problem by specializing `length_eq` to `NoMinOrder` and adding a new lemma for the `OrderBot` case. The other lemmas involving the private declarations are made private, except for `length_subadditive_Icc_Ioo`, which is reverted to the previous statement. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-measure-probability maintainer-merge tech debt 35/30 Mathlib/MeasureTheory/Measure/Stieltjes.lean 1 6 ['github-actions', 'grunweg', 'sgouezel', 'vihdzp'] sgouezel
assignee:sgouezel
0-80875
22 hours ago
3-85132
3 days ago
4-44051
4 days
33179 joelriou
author:joelriou
 feat(CategoryTheory/Sites): relation between `IsPrestack` and the full faithfulness of `toDescentData` We show that a pseudofunctor `F` is a prestack iff the functors `F.toDescentData f` are fully faithful whenever `f` is a covering family. --- - [x] depends on: #30190 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-category-theory maintainer-merge 181/2 Mathlib/CategoryTheory/Functor/FullyFaithful.lean,Mathlib/CategoryTheory/Sites/Descent/DescentData.lean,Mathlib/CategoryTheory/Sites/Descent/IsPrestack.lean,Mathlib/CategoryTheory/Sites/IsSheafFor.lean,Mathlib/CategoryTheory/Sites/Over.lean 5 n/a ['dagurtomas', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] nobody
0-73169
20 hours ago
unknown
unknown
30436 wwylele
author:wwylele
 feat(Topology/InfiniteSum): tprod_one_{add/sub}_ordered This extends the existing `Finset.prod_one_sub_ordered` to infinite sum/product, and also adds the more natural `add` version. Together with some previous PRs about infinite sum/prod and powerseries, this is part of my effort of upstreaming useful stuff from https://github.com/wwylele/PentagonalNumberTheorem. It starts getting into niche lemma, so suggestions such that not wanting this in mathlib, or it should be stated in a different form, are all welcomed. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-topology maintainer-merge 42/0 Mathlib/Algebra/BigOperators/Ring/Finset.lean,Mathlib/Topology/Algebra/InfiniteSum/Ring.lean 2 12 ['JovanGerb', 'github-actions', 'grunweg', 'kckennylau', 'wwylele'] grunweg
assignee:grunweg
0-50716
14 hours ago
1-575
1 day ago
59-6075
59 days
32870 0xTerencePrime
author:0xTerencePrime
 feat(Combinatorics/SimpleGraph): define edge-connectivity ## Summary This PR introduces k-edge-connectivity definitions for SimpleGraph, addressing #31691. ## Main Changes - **New file:** `Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean` ### Definitions - `IsEdgeReachable k u v`: vertices remain reachable after removing < k edges - `IsEdgeConnected k`: graph is k-edge-connected ### Lemmas - Basic properties: `rfl`, `symm`, `trans`, `mono`, `zero` - `isEdgeReachable_one`: equivalence with standard `Reachable` - `isEdgeConnected_one`: equivalence with `Preconnected` - `isEdgeReachable_succ`: inductive characterization - `isEdgeConnected_succ`: inductive characterization for graphs - `isEdgeConnected_two`: equivalence with `Preconnected ∧ ¬∃ e, IsBridge e` ## Verification - [x] `lake build` passes - [x] `lake exe runLinter` passes Closes #31691 t-combinatorics new-contributor maintainer-merge 134/0 Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean 2 90 ['0xTerencePrime', 'SnirBroshi', 'YaelDillies', 'github-actions'] nobody
0-24853
6 hours ago
2-64194
2 days ago
8-84275
8 days
33266 vihdzp
author:vihdzp
 chore(Order/Synonym): use `to_dual` --- ...plus some trivial style improvements. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-order maintainer-merge 22/50 Mathlib/Order/Synonym.lean 1 4 ['JovanGerb', 'github-actions'] nobody
0-568
9 minutes ago
0-821
13 minutes ago
0-30182
8 hours

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
200-50156
6 months ago
200-50157
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
60-46720
1 month ago
60-46977
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
32-75722
1 month ago
32-75722
1 month 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
28-6399
28 days ago
28-6399
28 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
14-47723
14 days ago
14-79189
14 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 78/72 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,Mathlib/RingTheory/Congruence/Hom.lean 8 7 ['SnirBroshi', 'github-actions', 'mathlib4-merge-conflict-bot', 'thorimur', 'vihdzp'] thorimur
assignee:thorimur
5-39389
5 days ago
5-39406
5 days ago
8-76821
8 days
32389 LLaurance
author:LLaurance
 feat(Analysis): Trigonometric identities `sin` and `cos` of real and complex integer multiples of π/12 --- Resolves https://github.com/leanprover-community/mathlib4/pull/28630#discussion_r2307957255 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-author t-analysis awaiting-zulip 120/0 Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean 1 10 ['LLaurance', 'artie2000', 'github-actions', 'j-loreaux'] nobody
4-84591
4 days ago
4-84591
4 days ago
15-38599
15 days
32734 Vierkantor
author:Vierkantor
 chore(Tactic): document remaining undocumented tactics Write documentation for the few tactics in Mathlib that have no documentation at all. After this PR and a few related ones are merged, every tactic defined in Mathlib should now have a docstring or a `@[tactic_alt]` attribute. The documentation for `mem_tac` is pending a Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Proj.20as.20a.20scheme.3A.20.60mem_tac.60.20works.20accidentally.3F/with/563193768 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) documentation t-meta awaiting-zulip 37/0 Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean,Mathlib/Tactic/Conv.lean,Mathlib/Tactic/GCongr/Core.lean 3 1 ['github-actions'] nobody
2-42377
2 days ago
2-42377
2 days ago
11-27028
11 days
32608 PrParadoxy
author:PrParadoxy
 feat(LinearAlgebra/PiTensorProduct): API for PiTensorProducts indexed by sets This PR addresses a TODO item in LinearAlgebra/PiTensorProduct.lean: * API for the various ways `ι` can be split into subsets; connect this with the binary tensor product -- specifically by describing tensors of type `⨂ (i : S), s i`, for `S : Set ι`. Our primary motivation is to formalize the notion of "tensors with infinite index set, which are equal to a distinguished element on all but finitely many indices". This is a standard construction e.g. in the theory of "infinite tensor products" of unital algebras. Beyond that, the `Set` API is natural in contexts where the index type has an independent interpretation. An example is quantum physics, where `ι` ranges over distinguishable degrees of freedom, and where its is common practice to annotate objects by the set of indices they are defined on. This PR creates a directory LinearAlgebra/PiTensorProduct and starts the file Set.lean. --- - [x] depends on: #32598 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-author new-contributor awaiting-zulip 301/0 Mathlib.lean,Mathlib/LinearAlgebra/PiTensorProduct/Set.lean 2 15 ['PrParadoxy', 'dagurtomas', 'eric-wieser', 'github-actions', 'leanprover-radar', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] dagurtomas
assignee:dagurtomas
2-38239
2 days ago
2-59196
2 days ago
10-66980
10 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
399-77277
1 year ago
399-77277
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
244-32654
8 months ago
255-61284
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
173-20903
5 months ago
173-20903
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
37-40602
1 month ago
219-63161
7 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
36-56843
1 month ago
36-56844
1 month 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
36-55933
1 month ago
36-55934
1 month 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
35-65877
1 month ago
465-39602
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
173-19741
5 months ago
173-19742
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
113-35386
3 months ago
113-35387
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
70-12596
2 months ago
70-12597
2 months 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
51-22286
1 month ago
219-62236
7 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
42-23470
1 month ago
42-23470
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
36-7611
1 month ago
36-7612
1 month 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
33-65681
1 month ago
33-65682
1 month 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
417-57746
1 year ago
443-46268
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
233-40554
7 months ago
233-40559
7 months ago
0-179
2 minutes

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

Number Author Title Description Labels +/- Modified files (first 100) 📝 💬 All users who commented or reviewed Assignee(s) Updated Last status change total time in review
33138 gasparattila
author:gasparattila
 chore(MeasureTheory/Measure/Stieltjes): remove `backward.privateInPublic` In #32482, some definitions in this file were rewritten using private declarations. However, this made `StieltjesFunction.length` unusable, since its API uses private declarations even in statements. This PR fixes this by problem by specializing `length_eq` to `NoMinOrder` and adding a new lemma for the `OrderBot` case. The other lemmas involving the private declarations are made private, except for `length_subadditive_Icc_Ioo`, which is reverted to the previous statement. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-measure-probability maintainer-merge tech debt 35/30 Mathlib/MeasureTheory/Measure/Stieltjes.lean 1 6 ['github-actions', 'grunweg', 'sgouezel', 'vihdzp'] sgouezel
assignee:sgouezel
0-80875
22 hours ago
3-85132
3 days ago
4-44051
4 days