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: October 04, 2025 at 03:29 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
25945 adomani
author:adomani
 feat: the empty line in commands linter This linter flags empty lines within a command. It allows empty lines within doc-strings, module-docs and a couple of other "sensible" places. It also skips files that are likely to contain meta-code, since there the use of empty lines in definition is more widespread. This PR continues the work from #25236. large-import t-linter maintainer-merge awaiting-author 375/7 Mathlib.lean,Mathlib/Analysis/Meromorphic/FactorizedRational.lean,Mathlib/CategoryTheory/Comma/StructuredArrow/CommaMap.lean,Mathlib/Init.lean,Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/EmptyLine.lean,MathlibTest/EmptyLine.lean 8 12 ['adomani', 'bryangingechen', 'eric-wieser', 'github-actions'] bryangingechen
assignee:bryangingechen
67-46739
2 months ago
67-46739
2 months ago
42-26074
42 days
24669 qawbecrdtey
author:qawbecrdtey
 feat(Analysis/Normed/Operator/LinearIsometry): added definition `LinearIsometryEquiv.prodComm` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) This commit defines a `LinearIsometryEquiv`, and states some trivial theorems about it. ```lean def prodComm [Module R E₂] : E × E₂ ≃ₗᵢ[R] E₂ × E ``` maintainer-merge t-analysis awaiting-author 8/1 Mathlib/Analysis/Normed/Operator/LinearIsometry.lean 1 12 ['Ruben-VandeVelde', 'eric-wieser', 'faenuccio', 'github-actions', 'j-loreaux', 'jcommelin', 'qawbecrdtey'] faenuccio
assignee:faenuccio
26-6941
26 days ago
115-81173
3 months ago
32-83569
32 days
27292 gasparattila
author:gasparattila
 feat: asymptotic cone of a set This PR defines the asymptotic cone of a set in a normed affine space and proves its main properties. This is partial progress towards showing that an unbounded finite-dimensional convex set contains a ray. --- - [x] depends on: #27221 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge new-contributor t-analysis 466/0 Mathlib.lean,Mathlib/Analysis/Normed/Affine/AsymptoticCone.lean,Mathlib/Order/Filter/Map.lean,Mathlib/Topology/Algebra/AsymptoticCone.lean 4 45 ['AntoineChambert-Loir', 'YaelDillies', 'gasparattila', 'github-actions', 'mathlib4-dependent-issues-bot'] YaelDillies
assignee:YaelDillies
16-76847
16 days ago
59-38740
1 month ago
73-56272
73 days
26660 strihanje01
author:strihanje01
 feat(Combinatorics/Additive/VerySmallDoubling): weak non-commutative Kneser's theorem add theorem about the structure of a doubling smaller than the golden ratio --- - [x] depends on: #28653 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) large-import maintainer-merge new-contributor t-combinatorics 215/41 Mathlib/Algebra/Group/Action/Pointwise/Finset.lean,Mathlib/Combinatorics/Additive/VerySmallDoubling.lean 2 79 ['YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'strihanje01'] YaelDillies
assignee:YaelDillies
10-51418
10 days ago
10-84067
10 days ago
52-26043
52 days
28295 artie2000
author:artie2000
 feat(Algebra/Order/Ring/Ordering): basic results about ring (pre)orderings * Basic automation for membership of ring orderings * Alternative constructors for ring preorderings and ring orderings * Basic results about ring preorderings and their supports, including the special case over a field --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) - [x] depends on: #27282 maintainer-merge t-algebra
label:t-algebra$
 203/0 Mathlib.lean,Mathlib/Algebra/Group/Subgroup/Defs.lean,Mathlib/Algebra/Order/Ring/Ordering/Basic.lean 3 57 ['Rob23oba', 'YaelDillies', 'artie2000', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'vihdzp'] joneugster
assignee:joneugster
9-8899
9 days ago
16-75238
16 days ago
22-38372
22 days
26259 Raph-DG
author:Raph-DG
 feat(Topology): Connecting different notions of locally finite In this PR we connect the notions of local finiteness of an indexed family of sets (as in LocallyFinite) and of a set of sets (as in Function.locallyFinsuppWithin) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-topology 38/0 Mathlib/Topology/LocallyFinsupp.lean 1 18 ['Raph-DG', 'chrisflav', 'github-actions', 'jcommelin', 'kckennylau'] jcommelin
assignee:jcommelin
8-39576
8 days ago
8-64892
8 days ago
97-28880
97 days
29275 wwylele
author:wwylele
 feat(GroupTheory): add DivisibleHull This is part of Hahn embedding theorem #27268, where an a ordered group is first embedded in a divisible group / Q-module. I am aware at #25662 there is also an ongoing rewrite of `LocalizedModule` that this PR uses. Hopefully I avoided interfering it by using mostly with public API. --- - [x] depends on: #29277 - [x] depends on: #29388 - [x] depends on: #29386 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-group-theory maintainer-merge 451/3 Mathlib.lean,Mathlib/Algebra/Order/Monoid/Defs.lean,Mathlib/Algebra/Order/Monoid/PNat.lean,Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean,Mathlib/Data/NNRat/Defs.lean,Mathlib/GroupTheory/DivisibleHull.lean 6 106 ['YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'vihdzp', 'wwylele'] tb65536
assignee:tb65536
8-8899
8 days ago
15-34776
15 days ago
25-11976
25 days
29110 NotWearingPants
author:NotWearingPants
 feat(Counterexamples): Euler's sum of powers conjecture feat(Counterexamples): Euler's sum of powers conjecture --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip maintainer-merge new-contributor 158/0 Counterexamples.lean,Counterexamples/EulerSumOfPowers.lean 2 43 ['MichaelStollBayreuth', 'NotWearingPants', 'eric-wieser', 'github-actions', 'tb65536', 'urkud'] MichaelStollBayreuth
assignee:MichaelStollBayreuth
7-27867
7 days ago
7-27923
7 days ago
24-25032
24 days
29513 grunweg
author:grunweg
 fix(lint-style): parse linter options and load environment extensions correctly Parse options and load linter set extension correctly. This fixes two issues: - We never called the `toOptions` function that parses Lakefile options into a `Lean.Options` structure: the function we use instead is only meant for command-line options and doesn't handle the `weak.` prefix correctly. - The way we load linter sets was incorrect: `withImportModules` stopped updating environment extensions since [lean4#6325](https://github.com/leanprover/lean4/pull/6325), and that is exactly what we use to store linter sets. At the time of writing, `importModules` might be a suitable replacement (but this is not very safe, and not documented to be stable). Instead, write a small elaborator returning the environment at the point of elaboration, and use that instead. --- - [x] depends on: #29584 - [x] depends on: #29585 - [x] depends on: #29586 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-meta 28/12 scripts/lint-style.lean 1 13 ['Vierkantor', 'adomani', 'github-actions', 'grunweg', 'mathlib4-dependent-issues-bot'] nobody
6-49551
6 days ago
6-62868
6 days ago
15-49268
15 days
29693 kckennylau
author:kckennylau
 feat(RingTheory): make Euclidean domain from DVR --- Zulip: https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Leading.20term.20of.20valuation/near/539666529 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-ring-theory maintainer-merge 82/0 Mathlib/RingTheory/DiscreteValuationRing/Basic.lean 1 6 ['github-actions', 'kckennylau', 'pechersky'] chrisflav
assignee:chrisflav
6-8886
6 days ago
17-49507
17 days ago
18-9008
18 days
29501 Vierkantor
author:Vierkantor
 test(TacticAnalysis): ensure `classical`'s effects are picked up This test case used to fail, and needed a fix to the `classical` tactic in the standard library: - [x] depends on: https://github.com/leanprover/lean4/pull/10332 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-meta 10/0 MathlibTest/TacticAnalysis.lean 1 6 ['Vierkantor', 'github-actions', 'grunweg', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] nobody
4-68219
4 days ago
6-60696
6 days ago
8-67589
8 days
28395 joelriou
author:joelriou
 feat(AlgebraicTopology/SimplicialSet): nondegenerate simplices in the standard simplex In this PR, we show that `d`-dimensional nondegenerate simplices in `Δ[n]` identify to `Fin (d + 1) ↪o Fin (n + 1)`. (This PR also contains some general additional API for (non)degenerate simplices. For this reason, three definitions related to subcomplexes generated by a simplex had to be moved from `StdSimplex.lean` to `Subcomplex.lean`.) --- - [x] depends on: #28337 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebraic-topology maintainer-merge 247/20 Mathlib/AlgebraicTopology/SimplicialSet/Degenerate.lean,Mathlib/AlgebraicTopology/SimplicialSet/Simplices.lean,Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean,Mathlib/AlgebraicTopology/SimplicialSet/Subcomplex.lean,Mathlib/Order/Hom/Basic.lean 5 24 ['github-actions', 'joelriou', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'robin-carlier'] robin-carlier
assignee:robin-carlier
4-40547
4 days ago
4-45893
4 days ago
23-17325
23 days
24965 erdOne
author:erdOne
 refactor: Make `IsLocalHom` take unbundled map --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-algebra merge-conflict awaiting-author
label:t-algebra$
 16/7 Mathlib/Algebra/Group/Units/Hom.lean,Mathlib/AlgebraicGeometry/Scheme.lean,Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean,Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean,Mathlib/Geometry/RingedSpace/OpenImmersion.lean 5 6 ['alreadydone', 'erdOne', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant'] nobody
123-2926
4 months ago
123-2927
4 months ago
10-26015
10 days
26912 pechersky
author:pechersky
 chore(Algebra/Ring/Subring): simp tag `Subring.smul_def` s-multiplying by a subtype is easiest to manipulate when both terms are in the ambient type. Many places that had to use the _def lemma for a rewrite, or to include it in a simp set, no longer have to. Ported from #25308 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) I found this being not-simp frustrating when talking about submodules over a valuation subring. maintainer-merge t-algebra merge-conflict
label:t-algebra$
 68/67 Mathlib/Algebra/Algebra/Subalgebra/Basic.lean,Mathlib/Algebra/Field/Subfield/Basic.lean,Mathlib/Algebra/Group/Subgroup/Actions.lean,Mathlib/Algebra/Group/Submonoid/MulAction.lean,Mathlib/Algebra/Module/LocalizedModule/Basic.lean,Mathlib/Algebra/Module/LocalizedModule/Exact.lean,Mathlib/Algebra/Module/LocalizedModule/IsLocalization.lean,Mathlib/Algebra/Module/LocalizedModule/Submodule.lean,Mathlib/Algebra/Ring/Periodic.lean,Mathlib/Algebra/Ring/Subring/Basic.lean,Mathlib/Algebra/Ring/Subsemiring/Basic.lean,Mathlib/Analysis/CStarAlgebra/Basic.lean,Mathlib/FieldTheory/KummerExtension.lean,Mathlib/GroupTheory/GroupAction/Defs.lean,Mathlib/GroupTheory/GroupAction/MultiplePrimitivity.lean,Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean,Mathlib/GroupTheory/GroupAction/SubMulAction/OfFixingSubgroup.lean,Mathlib/GroupTheory/GroupAction/SubMulAction/OfStabilizer.lean,Mathlib/LinearAlgebra/RootSystem/Irreducible.lean,Mathlib/LinearAlgebra/RootSystem/RootPositive.lean,Mathlib/LinearAlgebra/RootSystem/WeylGroup.lean,Mathlib/RingTheory/Etale/Kaehler.lean,Mathlib/RingTheory/LocalProperties/Projective.lean,Mathlib/RingTheory/Localization/InvSubmonoid.lean,Mathlib/RingTheory/OreLocalization/Basic.lean 25 19 ['artie2000', 'eric-wieser', 'github-actions', 'j-loreaux', 'linesthatinterlace', 'mathlib4-merge-conflict-bot', 'pechersky'] joelriou
assignee:joelriou
32-50817
1 month ago
32-50818
1 month ago
51-74059
51 days
28737 astrainfinita
author:astrainfinita
 refactor: deprecate `MulEquivClass` This PR continues the work from #18806. Original PR: https://github.com/leanprover-community/mathlib4/pull/18806 maintainer-merge t-algebra merge-conflict awaiting-author
label:t-algebra$
 67/77 Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Algebra/Group/Equiv/Basic.lean,Mathlib/Algebra/Group/Equiv/Defs.lean,Mathlib/Algebra/Group/Irreducible/Lemmas.lean,Mathlib/Algebra/Group/Subgroup/Map.lean,Mathlib/Algebra/Group/Submonoid/Operations.lean,Mathlib/Algebra/Group/Units/Equiv.lean,Mathlib/Algebra/GroupWithZero/Equiv.lean,Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean,Mathlib/Algebra/Module/Equiv/Defs.lean,Mathlib/Algebra/Order/CauSeq/Basic.lean,Mathlib/Algebra/Order/Hom/Monoid.lean,Mathlib/Algebra/Prime/Lemmas.lean,Mathlib/Algebra/Ring/Divisibility/Basic.lean,Mathlib/Algebra/Ring/Equiv.lean,Mathlib/Algebra/Star/MonoidHom.lean,Mathlib/Combinatorics/Additive/FreimanHom.lean,Mathlib/GroupTheory/GroupExtension/Defs.lean,Mathlib/GroupTheory/Submonoid/Center.lean,Mathlib/LinearAlgebra/FreeModule/Finite/CardQuotient.lean,Mathlib/RingTheory/Bialgebra/Equiv.lean,Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean,Mathlib/RingTheory/Multiplicity.lean,Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean,Mathlib/Topology/Algebra/ContinuousMonoidHom.lean,Mathlib/Topology/Algebra/InfiniteSum/Basic.lean 26 20 ['Vierkantor', 'alreadydone', 'astrainfinita', 'github-actions', 'grunweg', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib4-merge-conflict-bot'] Vierkantor
assignee:Vierkantor
23-54677
23 days ago
23-54678
23 days ago
4-17723
4 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
25945 adomani
author:adomani
 feat: the empty line in commands linter This linter flags empty lines within a command. It allows empty lines within doc-strings, module-docs and a couple of other "sensible" places. It also skips files that are likely to contain meta-code, since there the use of empty lines in definition is more widespread. This PR continues the work from #25236. large-import t-linter maintainer-merge awaiting-author 375/7 Mathlib.lean,Mathlib/Analysis/Meromorphic/FactorizedRational.lean,Mathlib/CategoryTheory/Comma/StructuredArrow/CommaMap.lean,Mathlib/Init.lean,Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/EmptyLine.lean,MathlibTest/EmptyLine.lean 8 12 ['adomani', 'bryangingechen', 'eric-wieser', 'github-actions'] bryangingechen
assignee:bryangingechen
67-46739
2 months ago
67-46739
2 months ago
42-26074
42 days
24669 qawbecrdtey
author:qawbecrdtey
 feat(Analysis/Normed/Operator/LinearIsometry): added definition `LinearIsometryEquiv.prodComm` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) This commit defines a `LinearIsometryEquiv`, and states some trivial theorems about it. ```lean def prodComm [Module R E₂] : E × E₂ ≃ₗᵢ[R] E₂ × E ``` maintainer-merge t-analysis awaiting-author 8/1 Mathlib/Analysis/Normed/Operator/LinearIsometry.lean 1 12 ['Ruben-VandeVelde', 'eric-wieser', 'faenuccio', 'github-actions', 'j-loreaux', 'jcommelin', 'qawbecrdtey'] faenuccio
assignee:faenuccio
26-6941
26 days ago
115-81173
3 months ago
32-83569
32 days
27292 gasparattila
author:gasparattila
 feat: asymptotic cone of a set This PR defines the asymptotic cone of a set in a normed affine space and proves its main properties. This is partial progress towards showing that an unbounded finite-dimensional convex set contains a ray. --- - [x] depends on: #27221 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge new-contributor t-analysis 466/0 Mathlib.lean,Mathlib/Analysis/Normed/Affine/AsymptoticCone.lean,Mathlib/Order/Filter/Map.lean,Mathlib/Topology/Algebra/AsymptoticCone.lean 4 45 ['AntoineChambert-Loir', 'YaelDillies', 'gasparattila', 'github-actions', 'mathlib4-dependent-issues-bot'] YaelDillies
assignee:YaelDillies
16-76847
16 days ago
59-38740
1 month ago
73-56272
73 days
26660 strihanje01
author:strihanje01
 feat(Combinatorics/Additive/VerySmallDoubling): weak non-commutative Kneser's theorem add theorem about the structure of a doubling smaller than the golden ratio --- - [x] depends on: #28653 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) large-import maintainer-merge new-contributor t-combinatorics 215/41 Mathlib/Algebra/Group/Action/Pointwise/Finset.lean,Mathlib/Combinatorics/Additive/VerySmallDoubling.lean 2 79 ['YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'strihanje01'] YaelDillies
assignee:YaelDillies
10-51418
10 days ago
10-84067
10 days ago
52-26043
52 days
28295 artie2000
author:artie2000
 feat(Algebra/Order/Ring/Ordering): basic results about ring (pre)orderings * Basic automation for membership of ring orderings * Alternative constructors for ring preorderings and ring orderings * Basic results about ring preorderings and their supports, including the special case over a field --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) - [x] depends on: #27282 maintainer-merge t-algebra
label:t-algebra$
 203/0 Mathlib.lean,Mathlib/Algebra/Group/Subgroup/Defs.lean,Mathlib/Algebra/Order/Ring/Ordering/Basic.lean 3 57 ['Rob23oba', 'YaelDillies', 'artie2000', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'vihdzp'] joneugster
assignee:joneugster
9-8899
9 days ago
16-75238
16 days ago
22-38372
22 days
26259 Raph-DG
author:Raph-DG
 feat(Topology): Connecting different notions of locally finite In this PR we connect the notions of local finiteness of an indexed family of sets (as in LocallyFinite) and of a set of sets (as in Function.locallyFinsuppWithin) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-topology 38/0 Mathlib/Topology/LocallyFinsupp.lean 1 18 ['Raph-DG', 'chrisflav', 'github-actions', 'jcommelin', 'kckennylau'] jcommelin
assignee:jcommelin
8-39576
8 days ago
8-64892
8 days ago
97-28880
97 days
29275 wwylele
author:wwylele
 feat(GroupTheory): add DivisibleHull This is part of Hahn embedding theorem #27268, where an a ordered group is first embedded in a divisible group / Q-module. I am aware at #25662 there is also an ongoing rewrite of `LocalizedModule` that this PR uses. Hopefully I avoided interfering it by using mostly with public API. --- - [x] depends on: #29277 - [x] depends on: #29388 - [x] depends on: #29386 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-group-theory maintainer-merge 451/3 Mathlib.lean,Mathlib/Algebra/Order/Monoid/Defs.lean,Mathlib/Algebra/Order/Monoid/PNat.lean,Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean,Mathlib/Data/NNRat/Defs.lean,Mathlib/GroupTheory/DivisibleHull.lean 6 106 ['YaelDillies', 'github-actions', 'mathlib4-dependent-issues-bot', 'vihdzp', 'wwylele'] tb65536
assignee:tb65536
8-8899
8 days ago
15-34776
15 days ago
25-11976
25 days
29110 NotWearingPants
author:NotWearingPants
 feat(Counterexamples): Euler's sum of powers conjecture feat(Counterexamples): Euler's sum of powers conjecture --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip maintainer-merge new-contributor 158/0 Counterexamples.lean,Counterexamples/EulerSumOfPowers.lean 2 43 ['MichaelStollBayreuth', 'NotWearingPants', 'eric-wieser', 'github-actions', 'tb65536', 'urkud'] MichaelStollBayreuth
assignee:MichaelStollBayreuth
7-27867
7 days ago
7-27923
7 days ago
24-25032
24 days
29513 grunweg
author:grunweg
 fix(lint-style): parse linter options and load environment extensions correctly Parse options and load linter set extension correctly. This fixes two issues: - We never called the `toOptions` function that parses Lakefile options into a `Lean.Options` structure: the function we use instead is only meant for command-line options and doesn't handle the `weak.` prefix correctly. - The way we load linter sets was incorrect: `withImportModules` stopped updating environment extensions since [lean4#6325](https://github.com/leanprover/lean4/pull/6325), and that is exactly what we use to store linter sets. At the time of writing, `importModules` might be a suitable replacement (but this is not very safe, and not documented to be stable). Instead, write a small elaborator returning the environment at the point of elaboration, and use that instead. --- - [x] depends on: #29584 - [x] depends on: #29585 - [x] depends on: #29586 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-meta 28/12 scripts/lint-style.lean 1 13 ['Vierkantor', 'adomani', 'github-actions', 'grunweg', 'mathlib4-dependent-issues-bot'] nobody
6-49551
6 days ago
6-62868
6 days ago
15-49268
15 days
29693 kckennylau
author:kckennylau
 feat(RingTheory): make Euclidean domain from DVR --- Zulip: https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Leading.20term.20of.20valuation/near/539666529 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-ring-theory maintainer-merge 82/0 Mathlib/RingTheory/DiscreteValuationRing/Basic.lean 1 6 ['github-actions', 'kckennylau', 'pechersky'] chrisflav
assignee:chrisflav
6-8886
6 days ago
17-49507
17 days ago
18-9008
18 days
29501 Vierkantor
author:Vierkantor
 test(TacticAnalysis): ensure `classical`'s effects are picked up This test case used to fail, and needed a fix to the `classical` tactic in the standard library: - [x] depends on: https://github.com/leanprover/lean4/pull/10332 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-meta 10/0 MathlibTest/TacticAnalysis.lean 1 6 ['Vierkantor', 'github-actions', 'grunweg', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] nobody
4-68219
4 days ago
6-60696
6 days ago
8-67589
8 days
28395 joelriou
author:joelriou
 feat(AlgebraicTopology/SimplicialSet): nondegenerate simplices in the standard simplex In this PR, we show that `d`-dimensional nondegenerate simplices in `Δ[n]` identify to `Fin (d + 1) ↪o Fin (n + 1)`. (This PR also contains some general additional API for (non)degenerate simplices. For this reason, three definitions related to subcomplexes generated by a simplex had to be moved from `StdSimplex.lean` to `Subcomplex.lean`.) --- - [x] depends on: #28337 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebraic-topology maintainer-merge 247/20 Mathlib/AlgebraicTopology/SimplicialSet/Degenerate.lean,Mathlib/AlgebraicTopology/SimplicialSet/Simplices.lean,Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean,Mathlib/AlgebraicTopology/SimplicialSet/Subcomplex.lean,Mathlib/Order/Hom/Basic.lean 5 24 ['github-actions', 'joelriou', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'robin-carlier'] robin-carlier
assignee:robin-carlier
4-40547
4 days ago
4-45893
4 days ago
23-17325
23 days
28484 euprunin
author:euprunin
 chore(Data): golf entire `toReal_eq_toReal`, `count_eq_of_nodup` and `smul_mat_cons` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data maintainer-merge 6/11 Mathlib/Data/ENNReal/Real.lean,Mathlib/Data/List/Nodup.lean,Mathlib/LinearAlgebra/Matrix/Notation.lean 3 11 ['bryangingechen', 'github-actions', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib4-merge-conflict-bot', 'pechersky', 'qawbecrdtey'] pechersky
assignee:pechersky
0-82107
22 hours ago
1-5998
1 day ago
48-81705
48 days
30111 sgouezel
author:sgouezel
 feat: composing a continuous multilinear map with continuous linear maps is analytic in both variables --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-analysis 133/0 Mathlib/Analysis/Analytic/CPolynomial.lean,Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean 2 15 ['github-actions', 'loefflerd', 'sgouezel'] nobody
0-60646
16 hours ago
0-60646
16 hours ago
1-3814
1 day
27465 erdOne
author:erdOne
 feat: the definition of nonarchimedean local fields --- - [x] depends on: #27430 - [x] depends on: #27412 - [x] depends on: #27213 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-number-theory 214/25 Mathlib.lean,Mathlib/NumberTheory/LocalField/Basic.lean,Mathlib/RingTheory/Valuation/RankOne.lean,Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean,Mathlib/Topology/Algebra/Valued/ValuativeRel.lean 5 61 ['erdOne', 'faenuccio', 'github-actions', 'kbuzzard', 'kckennylau', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'pechersky', 'riccardobrasca'] tb65536
assignee:tb65536
0-51856
14 hours ago
1-61146
1 day ago
14-72212
14 days
29759 NotWearingPants
author:NotWearingPants
 feat(Analysis/SpecificLimits/Fibonacci): prove that the ratio of consecutive Fibonacci numbers tends to the golden ratio --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge new-contributor t-analysis 36/0 Mathlib.lean,Mathlib/Analysis/SpecificLimits/Fibonacci.lean 2 7 ['NotWearingPants', 'Ruben-VandeVelde', 'github-actions', 'kckennylau'] nobody
0-45999
12 hours ago
0-46000
12 hours ago
8-14977
8 days
26282 AntoineChambert-Loir
author:AntoineChambert-Loir
 feat: a theorem of Jordan on primitive subgroups of the permutation group A theorem of Jordan on the primitive subgroups of a permutation group: * if it contains a swap, it is equal to the permutation group, * if it contains a 3-cycle, it contains the alternating group. This PR continues the work from #24131. --- - [x] depends on: #26281 - [x] depends on: #26280 - [x] depends on: #26279 Original PR: https://github.com/leanprover-community/mathlib4/pull/24131 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-group-theory large-import maintainer-merge 939/137 Mathlib.lean,Mathlib/Data/Set/Card.lean,Mathlib/GroupTheory/GroupAction/FixingSubgroup.lean,Mathlib/GroupTheory/GroupAction/Jordan.lean,Mathlib/GroupTheory/GroupAction/MultiplePrimitivity.lean,Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean,Mathlib/GroupTheory/GroupAction/Primitive.lean,Mathlib/GroupTheory/GroupAction/SubMulAction/OfFixingSubgroup.lean,Mathlib/GroupTheory/GroupAction/SubMulAction/OfStabilizer.lean,Mathlib/GroupTheory/Perm/Cycle/Type.lean,Mathlib/SetTheory/Cardinal/Embedding.lean 11 n/a ['AntoineChambert-Loir', 'adomani', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'tb65536'] nobody
0-31239
8 hours ago
unknown
unknown
27844 CBirkbeck
author:CBirkbeck
 Add q-expansion identities for Eisenstein series. This is PR contains some q-expansion identities that are needed to give the q-expansions of Eisenstein series, which will be added as part of #27606. --- - [x] depends on: #27212 - [x] depends on: #27837 - [x] depends on: #27839 - [x] depends on: #27840 - [x] depends on: #27841 - [x] depends on: #26016 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-number-theory 257/0 Mathlib.lean,Mathlib/Analysis/Complex/Exponential.lean,Mathlib/Analysis/Complex/SummableUniformlyOn.lean,Mathlib/Analysis/Normed/Module/FiniteDimension.lean,Mathlib/NumberTheory/LSeries/RiemannZeta.lean,Mathlib/NumberTheory/ModularForms/EisensteinSeries/Defs.lean,Mathlib/NumberTheory/ModularForms/EisensteinSeries/QExpansion.lean 7 44 ['CBirkbeck', 'MichaelStollBayreuth', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] nobody
0-16280
4 hours ago
0-27869
7 hours ago
0-62383
17 hours
24965 erdOne
author:erdOne
 refactor: Make `IsLocalHom` take unbundled map --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-algebra merge-conflict awaiting-author
label:t-algebra$
 16/7 Mathlib/Algebra/Group/Units/Hom.lean,Mathlib/AlgebraicGeometry/Scheme.lean,Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean,Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean,Mathlib/Geometry/RingedSpace/OpenImmersion.lean 5 6 ['alreadydone', 'erdOne', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant'] nobody
123-2926
4 months ago
123-2927
4 months ago
10-26015
10 days
26912 pechersky
author:pechersky
 chore(Algebra/Ring/Subring): simp tag `Subring.smul_def` s-multiplying by a subtype is easiest to manipulate when both terms are in the ambient type. Many places that had to use the _def lemma for a rewrite, or to include it in a simp set, no longer have to. Ported from #25308 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) I found this being not-simp frustrating when talking about submodules over a valuation subring. maintainer-merge t-algebra merge-conflict
label:t-algebra$
 68/67 Mathlib/Algebra/Algebra/Subalgebra/Basic.lean,Mathlib/Algebra/Field/Subfield/Basic.lean,Mathlib/Algebra/Group/Subgroup/Actions.lean,Mathlib/Algebra/Group/Submonoid/MulAction.lean,Mathlib/Algebra/Module/LocalizedModule/Basic.lean,Mathlib/Algebra/Module/LocalizedModule/Exact.lean,Mathlib/Algebra/Module/LocalizedModule/IsLocalization.lean,Mathlib/Algebra/Module/LocalizedModule/Submodule.lean,Mathlib/Algebra/Ring/Periodic.lean,Mathlib/Algebra/Ring/Subring/Basic.lean,Mathlib/Algebra/Ring/Subsemiring/Basic.lean,Mathlib/Analysis/CStarAlgebra/Basic.lean,Mathlib/FieldTheory/KummerExtension.lean,Mathlib/GroupTheory/GroupAction/Defs.lean,Mathlib/GroupTheory/GroupAction/MultiplePrimitivity.lean,Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean,Mathlib/GroupTheory/GroupAction/SubMulAction/OfFixingSubgroup.lean,Mathlib/GroupTheory/GroupAction/SubMulAction/OfStabilizer.lean,Mathlib/LinearAlgebra/RootSystem/Irreducible.lean,Mathlib/LinearAlgebra/RootSystem/RootPositive.lean,Mathlib/LinearAlgebra/RootSystem/WeylGroup.lean,Mathlib/RingTheory/Etale/Kaehler.lean,Mathlib/RingTheory/LocalProperties/Projective.lean,Mathlib/RingTheory/Localization/InvSubmonoid.lean,Mathlib/RingTheory/OreLocalization/Basic.lean 25 19 ['artie2000', 'eric-wieser', 'github-actions', 'j-loreaux', 'linesthatinterlace', 'mathlib4-merge-conflict-bot', 'pechersky'] joelriou
assignee:joelriou
32-50817
1 month ago
32-50818
1 month ago
51-74059
51 days
28737 astrainfinita
author:astrainfinita
 refactor: deprecate `MulEquivClass` This PR continues the work from #18806. Original PR: https://github.com/leanprover-community/mathlib4/pull/18806 maintainer-merge t-algebra merge-conflict awaiting-author
label:t-algebra$
 67/77 Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Algebra/Group/Equiv/Basic.lean,Mathlib/Algebra/Group/Equiv/Defs.lean,Mathlib/Algebra/Group/Irreducible/Lemmas.lean,Mathlib/Algebra/Group/Subgroup/Map.lean,Mathlib/Algebra/Group/Submonoid/Operations.lean,Mathlib/Algebra/Group/Units/Equiv.lean,Mathlib/Algebra/GroupWithZero/Equiv.lean,Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean,Mathlib/Algebra/Module/Equiv/Defs.lean,Mathlib/Algebra/Order/CauSeq/Basic.lean,Mathlib/Algebra/Order/Hom/Monoid.lean,Mathlib/Algebra/Prime/Lemmas.lean,Mathlib/Algebra/Ring/Divisibility/Basic.lean,Mathlib/Algebra/Ring/Equiv.lean,Mathlib/Algebra/Star/MonoidHom.lean,Mathlib/Combinatorics/Additive/FreimanHom.lean,Mathlib/GroupTheory/GroupExtension/Defs.lean,Mathlib/GroupTheory/Submonoid/Center.lean,Mathlib/LinearAlgebra/FreeModule/Finite/CardQuotient.lean,Mathlib/RingTheory/Bialgebra/Equiv.lean,Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean,Mathlib/RingTheory/Multiplicity.lean,Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean,Mathlib/Topology/Algebra/ContinuousMonoidHom.lean,Mathlib/Topology/Algebra/InfiniteSum/Basic.lean 26 20 ['Vierkantor', 'alreadydone', 'astrainfinita', 'github-actions', 'grunweg', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib4-merge-conflict-bot'] Vierkantor
assignee:Vierkantor
23-54677
23 days ago
23-54678
23 days ago
4-17723
4 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
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-zulip t-computability new-contributor awaiting-author 298/0 Mathlib.lean,Mathlib/Computability/GNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/RegularExpressions.lean,docs/references.bib 5 6 ['github-actions', 'mathlib4-dependent-issues-bot', 'meithecatte', 'trivial1711'] nobody
151-18065
4 months ago
151-18074
4 months ago
23-54870
23 days
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/) awaiting-zulip t-computability new-contributor 490/0 Mathlib.lean,Mathlib/Computability/RegularExpressionsToEpsilonNFA.lean,docs/references.bib 3 5 ['github-actions', 'mathlib4-dependent-issues-bot', 'meithecatte', 'qawbecrdtey'] nobody
151-17376
4 months ago
151-18011
4 months ago
75-77754
75 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-zulip t-computability new-contributor awaiting-author 159/0 Mathlib/Computability/DFA.lean,Mathlib/Computability/Language.lean 2 59 ['EtienneC30', 'YaelDillies', 'github-actions', 'maemre', 'meithecatte', 'urkud'] EtienneC30
assignee:EtienneC30
121-70236
3 months ago
151-17975
4 months ago
48-67492
48 days
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/) awaiting-zulip t-computability new-contributor 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
118-27627
3 months ago
118-27628
3 months ago
34-10595
34 days
29072 yury-harmonic
author:yury-harmonic
 feat({Nat,Int}/ModEq): add lemmas --- I'm not sure that I named these lemmas correctly. Suggestions about better names are welcome! [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data awaiting-zulip 171/15 Mathlib/Data/Int/ModEq.lean,Mathlib/Data/Nat/ModEq.lean 2 5 ['eric-wieser', 'github-actions', 'yury-harmonic'] nobody
35-71509
1 month ago
35-71509
1 month ago
0-55232
15 hours
29582 YaelDillies
author:YaelDillies
 chore: rename `_root_.prop` to `Prop.finite` This was a surprising name! --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data awaiting-zulip 1/1 Mathlib/Data/Fintype/EquivFin.lean 1 11 ['YaelDillies', 'bryangingechen', 'eric-wieser', 'github-actions', 'grunweg', 'plp127'] nobody
10-83751
10 days ago
10-83752
10 days ago
3-1360
3 days
29110 NotWearingPants
author:NotWearingPants
 feat(Counterexamples): Euler's sum of powers conjecture feat(Counterexamples): Euler's sum of powers conjecture --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip maintainer-merge new-contributor 158/0 Counterexamples.lean,Counterexamples/EulerSumOfPowers.lean 2 43 ['MichaelStollBayreuth', 'NotWearingPants', 'eric-wieser', 'github-actions', 'tb65536', 'urkud'] MichaelStollBayreuth
assignee:MichaelStollBayreuth
7-27867
7 days ago
7-27923
7 days ago
24-25032
24 days
24754 urkud
author:urkud
 feat: define `pathIntegral` This is a step towards formalizing of the Poincaré lemma for 1-forms. --- - [x] depends on: #24831 - [x] depends on: #25047 - [x] depends on: #25048 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-analysis awaiting-author 580/9 Mathlib.lean,Mathlib/Analysis/Convex/PathConnected.lean,Mathlib/Analysis/Normed/Module/Basic.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/ContDiff.lean,Mathlib/MeasureTheory/Integral/PathIntegral/Basic.lean 6 42 ['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'sgouezel', 'urkud'] j-loreaux
assignee:j-loreaux
6-32448
6 days ago
6-32448
6 days ago
17-56980
17 days
29002 grunweg
author:grunweg
 chore: move Data/Real/Irrational to RingTheory It certainly has nothing to do with data (structures). --- I'm less sure where to put it instead. [zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Cleaning.20up.20.60Data.60/with/536301893) suggested this place; in the future, this could also be split. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) file-removed awaiting-zulip 10/10 Counterexamples/IrrationalPowerOfIrrational.lean,Mathlib.lean,Mathlib/Analysis/Real/Pi/Irrational.lean,Mathlib/Data/Real/GoldenRatio.lean,Mathlib/NumberTheory/DiophantineApproximation/Basic.lean,Mathlib/NumberTheory/Rayleigh.lean,Mathlib/NumberTheory/Transcendental/Liouville/Basic.lean,Mathlib/RingTheory/Real/Irrational.lean,Mathlib/Tactic/NormNum/Irrational.lean,Mathlib/Topology/Instances/AddCircle/DenseSubgroup.lean,Mathlib/Topology/Instances/Irrational.lean 11 2 ['github-actions', 'mathlib4-merge-conflict-bot'] nobody
5-64322
5 days ago
5-64405
5 days ago
0-67
1 minute
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/) file-removed awaiting-zulip 0/564 Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/LinearCombination'.lean,Mathlib/Tactic/Linter/UnusedTactic.lean,MathlibTest/linear_combination'.lean 5 3 ['euprunin', 'github-actions', 'grunweg'] nobody
5-35886
5 days ago
39-21794
1 month ago
0-1
1 second
11800 JADekker
author:JADekker
 feat : Define KappaLindelöf spaces Define KappaLindelöf spaces by following the first one-third of the API for Lindelöf spaces. The remainder will be added in a future PR. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-topology merge-conflict please-adopt 301/2 Mathlib.lean,Mathlib/Topology/Compactness/KappaLindelof.lean,Mathlib/Topology/Compactness/Lindelof.lean 3 38 ['ADedecker', 'JADekker', 'PatrickMassot', 'StevenClontz', 'adomani', 'github-actions', 'grunweg', 'kim-em', 'urkud'] nobody
382-81498
1 year ago
383-17073
1 year ago
119-10687
119 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/) awaiting-zulip t-order t-algebra merge-conflict
label:t-algebra$
 146/44 Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean 2 11 ['FR-vdash-bot', 'YaelDillies', 'github-actions', 'j-loreaux'] nobody
317-54748
10 months ago
317-54748
10 months ago
33-64877
33 days
8370 eric-wieser
author:eric-wieser
 refactor(Analysis/NormedSpace/Exponential): remove the `𝕂` argument from `exp` This argument is still needed for almost all the lemmas, which means it can longer be found by unification. We keep around `expSeries 𝕂 A`, as it's needed for talking about the radius of convergence over different base fields. This is a prerequisite for #8372, as we can't merge the functions until they have the same interface.\ Zulip thread: [#mathlib4 > Real.exp @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Real.2Eexp/near/401602245) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) This is started from the mathport output on https://github.com/leanprover-community/mathlib/pull/19244 awaiting-zulip t-analysis merge-conflict 432/387 Mathlib/Analysis/CStarAlgebra/Exponential.lean,Mathlib/Analysis/CStarAlgebra/Spectrum.lean,Mathlib/Analysis/Normed/Algebra/Exponential.lean,Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean,Mathlib/Analysis/Normed/Algebra/QuaternionExponential.lean,Mathlib/Analysis/Normed/Algebra/Spectrum.lean,Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean,Mathlib/Analysis/NormedSpace/DualNumber.lean,Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean,Mathlib/Analysis/SpecialFunctions/Exponential.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Series.lean 11 29 ['YaelDillies', 'eric-wieser', 'girving', 'github-actions', 'j-loreaux', 'kbuzzard', 'leanprover-community-bot-assistant', 'urkud'] nobody
162-10125
5 months ago
173-38755
5 months ago
29-60989
29 days
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-zulip t-computability new-contributor merge-conflict awaiting-author 307/5 Mathlib/Computability/NFA.lean 1 15 ['TpmKranz', 'YaelDillies', 'dupuisf', 'github-actions', 'leanprover-community-bot-assistant', 'meithecatte'] nobody
137-40631
4 months ago
137-40632
4 months ago
45-84611
45 days
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-zulip t-computability new-contributor merge-conflict awaiting-author 218/2 Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean 2 90 ['EtienneC30', 'b-mehta', 'github-actions', 'leanprover-community-bot-assistant', 'meithecatte', 'rudynicolop'] EtienneC30
assignee:EtienneC30
137-39705
4 months ago
137-39707
4 months ago
39-67601
39 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/) awaiting-zulip t-algebra merge-conflict
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
90-84774
2 months ago
90-84774
2 months ago
0-66650
18 hours
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/) awaiting-zulip new-contributor t-algebraic-geometry merge-conflict 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
90-83612
2 months ago
90-83613
2 months ago
6-51040
6 days
28298 thorimur
author:thorimur
 chore: dedent `to_additive` docstrings This PR uses automation to dedent `to_additive` docstrings throughout Mathlib. It does not lint against indentation or in any way enforce indentation standards for future docstrings. The convention was chosen in accordance with the discussion and polls at [this Zulip thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Poll.3A.20Indentation.20style.20for.20.60to_additive.60.20docstrings/with/534285603). --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip merge-conflict documentation 949/949 Mathlib/Algebra/BigOperators/Fin.lean,Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Algebra/BigOperators/Finsupp/Basic.lean,Mathlib/Algebra/BigOperators/Group/Finset/Lemmas.lean,Mathlib/Algebra/BigOperators/Group/List/Basic.lean,Mathlib/Algebra/BigOperators/Group/Multiset/Defs.lean,Mathlib/Algebra/BigOperators/Pi.lean,Mathlib/Algebra/Category/Grp/Basic.lean,Mathlib/Algebra/Category/Grp/FilteredColimits.lean,Mathlib/Algebra/Category/Grp/Limits.lean,Mathlib/Algebra/Category/Grp/Ulift.lean,Mathlib/Algebra/Category/MonCat/Basic.lean,Mathlib/Algebra/Category/MonCat/FilteredColimits.lean,Mathlib/Algebra/Category/MonCat/Limits.lean,Mathlib/Algebra/Category/Semigrp/Basic.lean,Mathlib/Algebra/Free.lean,Mathlib/Algebra/FreeMonoid/Basic.lean,Mathlib/Algebra/Group/Action/Defs.lean,Mathlib/Algebra/Group/Action/Pi.lean,Mathlib/Algebra/Group/Action/Pointwise/Finset.lean,Mathlib/Algebra/Group/Basic.lean,Mathlib/Algebra/Group/Defs.lean,Mathlib/Algebra/Group/Embedding.lean,Mathlib/Algebra/Group/Equiv/Basic.lean,Mathlib/Algebra/Group/Equiv/Defs.lean,Mathlib/Algebra/Group/Equiv/Opposite.lean,Mathlib/Algebra/Group/Even.lean,Mathlib/Algebra/Group/Hom/Basic.lean,Mathlib/Algebra/Group/Hom/Defs.lean,Mathlib/Algebra/Group/Hom/Instances.lean,Mathlib/Algebra/Group/Indicator.lean,Mathlib/Algebra/Group/Pi/Lemmas.lean,Mathlib/Algebra/Group/Pi/Units.lean,Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean,Mathlib/Algebra/Group/Pointwise/Set/Basic.lean,Mathlib/Algebra/Group/Prod.lean,Mathlib/Algebra/Group/Subgroup/Basic.lean,Mathlib/Algebra/Group/Subgroup/Defs.lean,Mathlib/Algebra/Group/Subgroup/Ker.lean,Mathlib/Algebra/Group/Subgroup/Lattice.lean,Mathlib/Algebra/Group/Subgroup/Map.lean,Mathlib/Algebra/Group/Subgroup/Pointwise.lean,Mathlib/Algebra/Group/Submonoid/Basic.lean,Mathlib/Algebra/Group/Submonoid/BigOperators.lean,Mathlib/Algebra/Group/Submonoid/Defs.lean,Mathlib/Algebra/Group/Submonoid/Membership.lean,Mathlib/Algebra/Group/Submonoid/MulAction.lean,Mathlib/Algebra/Group/Submonoid/Operations.lean,Mathlib/Algebra/Group/Subsemigroup/Basic.lean,Mathlib/Algebra/Group/Subsemigroup/Operations.lean,Mathlib/Algebra/Group/UniqueProds/Basic.lean,Mathlib/Algebra/Group/Units/Defs.lean,Mathlib/Algebra/Group/Units/Equiv.lean,Mathlib/Algebra/Group/Units/Hom.lean,Mathlib/Algebra/Group/Units/Opposite.lean,Mathlib/Algebra/Notation/Pi/Basic.lean,Mathlib/Algebra/Opposites.lean,Mathlib/Algebra/Order/BigOperators/Group/List.lean,Mathlib/Algebra/Order/Group/Abs.lean,Mathlib/Algebra/Order/Group/Basic.lean,Mathlib/Algebra/Order/Group/Cone.lean,Mathlib/Algebra/Order/Group/OrderIso.lean,Mathlib/Algebra/Order/Group/Units.lean,Mathlib/Algebra/Order/Hom/Monoid.lean,Mathlib/Algebra/Order/Monoid/Basic.lean,Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean,Mathlib/Algebra/Order/Monoid/Submonoid.lean,Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean,Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean,Mathlib/Algebra/Order/Monoid/Units.lean,Mathlib/Algebra/Order/Pi.lean,Mathlib/Algebra/Regular/Defs.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/CategoryTheory/Monoidal/Discrete.lean,Mathlib/Data/Finset/NoncommProd.lean,Mathlib/Data/Fintype/BigOperators.lean,Mathlib/Data/Set/MulAntidiagonal.lean,Mathlib/Data/Set/SMulAntidiagonal.lean,Mathlib/Data/Vector/Basic.lean,Mathlib/Dynamics/Ergodic/Action/OfMinimal.lean,Mathlib/Dynamics/FixedPoints/Prufer.lean,Mathlib/Geometry/Manifold/Algebra/SmoothFunctions.lean,Mathlib/GroupTheory/Complement.lean,Mathlib/GroupTheory/Congruence/Basic.lean,Mathlib/GroupTheory/Congruence/Defs.lean,Mathlib/GroupTheory/Coprod/Basic.lean,Mathlib/GroupTheory/Coset/Basic.lean,Mathlib/GroupTheory/Divisible.lean,Mathlib/GroupTheory/EckmannHilton.lean,Mathlib/GroupTheory/FreeGroup/Basic.lean,Mathlib/GroupTheory/FreeGroup/Reduce.lean,Mathlib/GroupTheory/GroupAction/Basic.lean,Mathlib/GroupTheory/GroupAction/Blocks.lean,Mathlib/GroupTheory/GroupAction/Defs.lean,Mathlib/GroupTheory/GroupAction/FixedPoints.lean,Mathlib/GroupTheory/GroupAction/Hom.lean,Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean,Mathlib/GroupTheory/GroupAction/Primitive.lean,Mathlib/GroupTheory/GroupAction/Quotient.lean,Mathlib/GroupTheory/GroupAction/SubMulAction.lean 141 10 ['eric-wieser', 'github-actions', 'grunweg', 'mathlib4-merge-conflict-bot', 'thorimur'] nobody
50-25706
1 month ago
51-13078
1 month ago
0-61617
17 hours
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 awaiting-zulip slow-typeclass-synthesis t-algebra t-analysis merge-conflict
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
31-12857
1 month ago
31-12858
1 month ago
0-20585
5 hours
17518 grunweg
author:grunweg
 feat: lint on declarations mentioning `Invertible` or `Unique` Using the same infrastructure as for #10235. Depends on that PR to land first, and also (for the first lint) a zulip discussion if that change is desired/about the best way to enact it. --- - [ ] depends on: #10235 awaiting-zulip t-linter merge-conflict blocked-by-other-PR 149/7 Mathlib.lean,Mathlib/Algebra/MvPolynomial/PDeriv.lean,Mathlib/Computability/Halting.lean,Mathlib/Computability/TuringMachine.lean,Mathlib/Data/Fintype/Card.lean,Mathlib/GroupTheory/Perm/DomMulAct.lean,Mathlib/Logic/Basic.lean,Mathlib/Logic/Encodable/Basic.lean,Mathlib/NumberTheory/JacobiSum/Basic.lean,Mathlib/Order/Heyting/Regular.lean,Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/UnusedAssumptionInType.lean 13 3 ['github-actions', 'mathlib4-dependent-issues-bot', 'mergify'] nobody
335-35217
11 months ago
361-23739
11 months 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/) awaiting-zulip t-computability new-contributor merge-conflict blocked-by-other-PR 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
151-18025
4 months ago
151-18030
4 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
30107 grunweg
author:grunweg
 chore: track occurrences of 'nonrec' as technical debt Matches leanprover-community/leanprover-community.github.io#689: only merge when that is deemed a good idea. -------- TODO: make the count more robust, for instance count all occurrences of "^nonrec " plus those of "^[private|protected] nonrec ". --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) tech debt CI 1/0 scripts/technical-debt-metrics.sh 1 1 ['github-actions'] nobody
2-50934
2 days ago
2-68184
2 days ago
2-68163
2 days