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: June 09, 2025 at 20:21 UTC

Stale ready-to-merge'd PRs

Number Author Title Description Labels +/- Modified files (first 100) 📝 💬 All users who commented or reviewed Assignee(s) Updated Last status change total time in review
24480 mariainesdff
author:mariainesdff
 feat(RingTheory/DividedPowers/SubPDIdeal): add SubDPIdeal Let `A` be a commutative (semi)ring and let `I` be an ideal of `A` with a divided power structure `hI`. A subideal `J` of `I` is a *sub-dp-ideal* of `(I, hI)` if, for all `n ∈ ℕ > 0` and all `x ∈ J`, `hI.dpow n x ∈ J`. The "TODOs" listed on the file docstring have been formalized by the authors and will be added in subsequent PRs. Co-authored-by: @AntoineChambert-Loir --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebra t-number-theory ready-to-merge delegated
label:t-algebra$
 373/0 Mathlib.lean,Mathlib/RingTheory/DividedPowers/SubDPIdeal.lean,Mathlib/RingTheory/Ideal/Span.lean 3 20 ['AntoineChambert-Loir', 'github-actions', 'mathlib-bors', 'riccardobrasca'] riccardobrasca
assignee:riccardobrasca
6-36131
6 days ago
6-37742
6 days ago
33-65896
33 days

Stale maintainer-merge'd PRs

Number Author Title Description Labels +/- Modified files (first 100) 📝 💬 All users who commented or reviewed Assignee(s) Updated Last status change total time in review
24816 ciskiko
author:ciskiko
 feat(GroupTheory): add Regular Wreath Product feat: add regular wreath product and some results; add iterated wreath product; add the isomorphism of iterated wreath product of Z_p to sylow p subgroup of S_{p^n}. Needs some work simplifying final result. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge new-contributor t-algebra
label:t-algebra$
 285/1 Mathlib.lean,Mathlib/Algebra/Group/End.lean,Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean,Mathlib/Data/Nat/Multiplicity.lean,Mathlib/GroupTheory/RegularWreathProduct.lean,Mathlib/Logic/Equiv/Fin/Basic.lean,Mathlib/SetTheory/Cardinal/Finite.lean 7 102 ['ciskiko', 'github-actions', 'tb65536'] tb65536
assignee:tb65536
15-34284
15 days ago
15-34285
15 days ago
24-38880
24 days
24689 chrisflav
author:chrisflav
 feat(Topology): compact open covered sets This is used to define the fpqc topology for schemes. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-algebraic-geometry t-topology 219/0 Mathlib.lean,Mathlib/Data/Set/Sigma.lean,Mathlib/Topology/Compactness/Compact.lean,Mathlib/Topology/Sets/CompactOpenCovered.lean,Mathlib/Topology/Sets/Opens.lean,Mathlib/Topology/Spectral/Prespectral.lean 6 5 ['chrisflav', 'erdOne', 'github-actions', 'leanprover-community-bot-assistant'] nobody
10-5868
10 days ago
10-6253
10 days ago
31-65992
31 days
25236 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. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) large-import t-linter maintainer-merge 373/11 Archive/Wiedijk100Theorems/BuffonsNeedle.lean,Mathlib.lean,Mathlib/CategoryTheory/Limits/Shapes/NormalMono/Equalizers.lean,Mathlib/Init.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/EmptyLine.lean,MathlibTest/EmptyLine.lean 7 23 ['adomani', 'bryangingechen', 'github-actions', 'grunweg', 'leanprover-community-bot-assistant'] nobody
5-39896
5 days ago
6-24476
6 days ago
13-21682
13 days
25407 adomani
author:adomani
 feat: check that the mathlib options exist This PR adds a simple check that all the options mentioned in `mathlibStandardSet` exist (at least, the ones that do exist!). --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge 18/0 Mathlib/Init.lean 1 5 ['adomani', 'github-actions', 'grunweg'] nobody
4-86052
4 days ago
4-86052
4 days ago
5-83711
5 days
24465 adomani
author:adomani
 feat: a linter to enforce formatting This linter enforces that the hypotheses of every declaration are correctly formatted. This already required multiple PRs to make mathlib compliant. Ideally, little by little the linter can be extended to format more of mathlib. --- The default linter option is `false`, but the lakefile enforces it to be `true`. This means that the linter does not run on `MathlibTest`. However, the tests should still be compliant, since the default option was `true` in development and the tests were fixed. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) large-import t-linter maintainer-merge 876/4 Mathlib.lean,Mathlib/Algebra/Group/Int/Defs.lean,Mathlib/Algebra/Group/Nat/Defs.lean,Mathlib/Algebra/Ring/Int/Defs.lean,Mathlib/Data/FunLike/Basic.lean,Mathlib/Data/SetLike/Basic.lean,Mathlib/Init.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/CommandStart.lean,Mathlib/Tactic/Simps/NotationClass.lean,MathlibTest/CommandStart.lean,MathlibTest/EuclideanSpace.lean,MathlibTest/Simps.lean,MathlibTest/Traversable.lean,MathlibTest/antidiagonal.lean,MathlibTest/delabLinearIndependent.lean,MathlibTest/matrix.lean,MathlibTest/norm_num.lean,MathlibTest/set_like.lean,MathlibTest/vec_notation.lean 20 89 ['Parcly-Taxel', 'adomani', 'eric-wieser', 'github-actions', 'grunweg', 'leanprover-community-bot-assistant'] grunweg
assignee:grunweg
4-31543
4 days ago
27-43236
27 days ago*
40-47955
40 days*
25265 FMLJohn
author:FMLJohn
 feat(Order/SupClosed): `compl_image_latticeClosure` and `compl_image_latticeClosure_eq_of_compl_image_eq_self` The main results in this pull request are: 1. `compl_image_latticeClosure`: given any Boolean algebra `α` and `s : Set α`, `compl '' latticeClosure s` is the same as `latticeClosure (compl '' s)`; 2. `compl_image_latticeClosure_eq_of_compl_image_eq_self`: given any Boolean algebra `α` and `s : Set α` such that `compl '' s = s`, we have `compl '' latticeClosure s = latticeClosure s`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-order 59/1 Mathlib/Order/SupClosed.lean 1 8 ['FMLJohn', 'YaelDillies', 'github-actions'] bryangingechen
assignee:bryangingechen
4-23003
4 days ago
7-2975
7 days ago
11-12593
11 days
25172 eric-wieser
author:eric-wieser
 feat: restricting `Affine.Simplex` to an affine subspace that contains it Also removes a redundant `Nonempty` argument. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-euclidean-geometry 68/5 Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean,Mathlib/LinearAlgebra/AffineSpace/Independent.lean 2 10 ['eric-wieser', 'github-actions', 'jsm28', 'ocfnash'] nobody
4-17046
4 days ago
15-27025
15 days ago
15-67897
15 days
25255 Raph-DG
author:Raph-DG
 feat(RingTheory): Order of vanishing in a ring In this PR we define the order of vanishing of a ring and its extension to elements of the function field (as in stacks project 02MD) as well as some basic API. Note that I'm slightly unsure that some of the lemmas used to prove this are at the right level of generality, and further I'm not quite sure where some of these lemmas belong (as indicated by the comments in the main OrderOfVanishing.lean file). Any comments about this would be very much appreciated. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge new-contributor t-algebra RFC
label:t-algebra$
 247/0 Mathlib.lean,Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean,Mathlib/RingTheory/Artinian/Module.lean,Mathlib/RingTheory/Ideal/Operations.lean,Mathlib/RingTheory/Ideal/Quotient/Operations.lean,Mathlib/RingTheory/OrderOfVanishing.lean 6 83 ['Raph-DG', 'chrisflav', 'erdOne', 'github-actions', 'jcommelin'] nobody
3-82277
3 days ago
3-82863
3 days ago
10-62245
10 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 21/1 Mathlib/Analysis/Normed/Operator/LinearIsometry.lean 1 7 ['Ruben-VandeVelde', 'eric-wieser', 'faenuccio', 'github-actions', 'jcommelin', 'qawbecrdtey'] faenuccio
assignee:faenuccio
3-57895
3 days ago
5-40535
5 days ago
32-57362
32 days
25059 s235282
author:s235282
 feat(Combinatorics/SimpleGraph/Bipartite): a graph is 2-colorable iff it's bipartite Define a predicate for a simple graph to be bipartite (`def IsBipartite (G : SimpleGraph V) : Prop := G.Colorable 2`) and prove ` G.IsBipartite ↔ ∃ s t : Set V, G.IsBipartiteWith s t`. --- This is my first attempt at contributing to mathlib and therefore I have a couple of points of uncertainty related to: - Naming conventions for theorems - Seeing a lot of isBipartite vs IsBipartite in the original work. What do we want to go with when? - Definition placement - Where should I put the IsBipartite definition. - Structure of biimplication theorems - Should I combine the different lemmas into 1 bgi theorem? Feedback is greatly appreciated :) [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) large-import maintainer-merge new-contributor t-combinatorics 36/3 Mathlib/Combinatorics/SimpleGraph/Bipartite.lean 1 30 ['YaelDillies', 'github-actions', 'mitchell-horner', 's235282'] nobody
2-37309
2 days ago
2-37856
2 days ago
8-85285
8 days
25089 Bergschaf
author:Bergschaf
 feat(Order/Sublocale): definition of sublocales There are several possible definition of sublocales. I used one from [nlab](https://ncatlab.org/nlab/show/sublocale) which states that a sublocale is a subset of a locale which is closed under all meets and for any ∈ S and x ∈ X, we have x ⇨ s ∈ S. This PR also includes an order isomorphism between (Nucleus)ᵒᵈ and Sublocale. --- I am open to better name suggestions for the order isomorphism. - [x] depends on: #24941 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-order 265/8 Mathlib.lean,Mathlib/Order/Hom/Lattice.lean,Mathlib/Order/Nucleus.lean,Mathlib/Order/Sublocale.lean,Mathlib/Order/Synonym.lean,docs/references.bib 6 71 ['Bergschaf', 'YaelDillies', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'xhalo32'] nobody
2-1809
2 days ago
2-1809
2 days ago
15-67631
15 days
25563 Komyyy
author:Komyyy
 chore: move `Topology.StoneCech` into `Topology.Compactification` (1/2) At present, the `Topology.Compactification` directory includes results on one-point compactifications, but results on Stone-Čech compactifications are currently located elsewhere. The removed file `Topology.Compactification` is deprecated in another PR (#25583) to leave a good git diff history. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) file-removed maintainer-merge t-topology 9/9 Mathlib.lean,Mathlib/Combinatorics/Hindman.lean,Mathlib/Topology/Category/CompHaus/Basic.lean,Mathlib/Topology/Category/CompHaus/Projective.lean,Mathlib/Topology/Category/Profinite/Projective.lean,Mathlib/Topology/Category/Stonean/Adjunctions.lean,Mathlib/Topology/Compactification/StoneCech.lean,Mathlib/Topology/ExtremallyDisconnected.lean,Mathlib/Topology/Maps/Proper/UniversallyClosed.lean,Mathlib/Topology/Separation/CompletelyRegular.lean 10 4 ['Komyyy', 'github-actions', 'grunweg'] nobody
1-42965
1 day ago
1-42965
1 day ago
2-18496
2 days
24382 joelriou
author:joelriou
 feat(CategoryTheory): pseudofunctors from strict bicategories This PR provides an API for pseudofunctors `F` from a strict bicategory `B`. In particular, this shall apply to pseudofunctors from locally discrete bicategories. We first introduce more flexible variants of `mapId` and `mapComp`: for example, if `f` and `g` are composable morphisms and `fg` is such that `h : fg = f ≫ f`, we provide an isomorphism `F.mapComp' f g fg h : F.map fg ≅ F.map f ≫ F.map g`. We study the compatibilities of these isomorphisms with respect to composition with identities and associativity. Secondly, given a commutative square `t ≫ r = l ≫ b` in `B`, we construct an isomorphism `F.map t ≫ F.map r ≅ F.map l ≫ F.map b`. Co-authored-by: Christian Merten --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-category-theory 168/0 Mathlib.lean,Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean,Mathlib/CategoryTheory/Bicategory/Functor/Strict.lean 3 17 ['callesonne', 'erdOne', 'github-actions', 'joelriou'] nobody
1-13411
1 day ago
1-79195
1 day ago
44-6763
44 days
21751 vihdzp
author:vihdzp
 refactor(SetTheory/Ordinal/Arithmetic): rework `Ordinal.pred` API This PR does the following: - give a simpler definition of `Ordinal.pred` - replace `¬ ∃ a, o = succ a` and `∀ a, o ≠ succ a` by `IsSuccPrelimit o` throughout - improve theorem names --- There's a legitimate question of whether we even want `Ordinal.pred` (see [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Ordinal.2Epred)) but this should be a good change in the meanwhile regardless. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-set-theory maintainer-merge merge-conflict 102/67 Mathlib/SetTheory/Ordinal/Arithmetic.lean,Mathlib/SetTheory/Ordinal/Exponential.lean 2 13 ['YaelDillies', 'github-actions', 'grunweg', 'vihdzp'] nobody
33-80652
1 month ago
80-59279
2 months ago
36-50134
36 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
6-63620
6 days ago
6-63621
6 days ago
10-26015
10 days
23961 FR-vdash-bot
author:FR-vdash-bot
 refactor: unbundle algebra from `ENormed*` Further speed up the search in the algebraic typeclass hierarchy by avoiding searching for `TopologicalSpace`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) slow-typeclass-synthesis maintainer-merge t-algebra t-analysis merge-conflict awaiting-author
label:t-algebra$
 32/25 Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/Analysis/Normed/Group/Continuity.lean,Mathlib/Analysis/NormedSpace/IndicatorFunction.lean,Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean 5 12 ['FR-vdash-bot', 'github-actions', 'grunweg', 'jcommelin', 'leanprover-bot', 'leanprover-community-bot-assistant'] nobody
2-47838
2 days ago
2-47838
2 days ago
17-72244
17 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
24816 ciskiko
author:ciskiko
 feat(GroupTheory): add Regular Wreath Product feat: add regular wreath product and some results; add iterated wreath product; add the isomorphism of iterated wreath product of Z_p to sylow p subgroup of S_{p^n}. Needs some work simplifying final result. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge new-contributor t-algebra
label:t-algebra$
 285/1 Mathlib.lean,Mathlib/Algebra/Group/End.lean,Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean,Mathlib/Data/Nat/Multiplicity.lean,Mathlib/GroupTheory/RegularWreathProduct.lean,Mathlib/Logic/Equiv/Fin/Basic.lean,Mathlib/SetTheory/Cardinal/Finite.lean 7 102 ['ciskiko', 'github-actions', 'tb65536'] tb65536
assignee:tb65536
15-34284
15 days ago
15-34285
15 days ago
24-38880
24 days
24689 chrisflav
author:chrisflav
 feat(Topology): compact open covered sets This is used to define the fpqc topology for schemes. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-algebraic-geometry t-topology 219/0 Mathlib.lean,Mathlib/Data/Set/Sigma.lean,Mathlib/Topology/Compactness/Compact.lean,Mathlib/Topology/Sets/CompactOpenCovered.lean,Mathlib/Topology/Sets/Opens.lean,Mathlib/Topology/Spectral/Prespectral.lean 6 5 ['chrisflav', 'erdOne', 'github-actions', 'leanprover-community-bot-assistant'] nobody
10-5868
10 days ago
10-6253
10 days ago
31-65992
31 days
25236 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. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) large-import t-linter maintainer-merge 373/11 Archive/Wiedijk100Theorems/BuffonsNeedle.lean,Mathlib.lean,Mathlib/CategoryTheory/Limits/Shapes/NormalMono/Equalizers.lean,Mathlib/Init.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/EmptyLine.lean,MathlibTest/EmptyLine.lean 7 23 ['adomani', 'bryangingechen', 'github-actions', 'grunweg', 'leanprover-community-bot-assistant'] nobody
5-39896
5 days ago
6-24476
6 days ago
13-21682
13 days
25407 adomani
author:adomani
 feat: check that the mathlib options exist This PR adds a simple check that all the options mentioned in `mathlibStandardSet` exist (at least, the ones that do exist!). --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge 18/0 Mathlib/Init.lean 1 5 ['adomani', 'github-actions', 'grunweg'] nobody
4-86052
4 days ago
4-86052
4 days ago
5-83711
5 days
24465 adomani
author:adomani
 feat: a linter to enforce formatting This linter enforces that the hypotheses of every declaration are correctly formatted. This already required multiple PRs to make mathlib compliant. Ideally, little by little the linter can be extended to format more of mathlib. --- The default linter option is `false`, but the lakefile enforces it to be `true`. This means that the linter does not run on `MathlibTest`. However, the tests should still be compliant, since the default option was `true` in development and the tests were fixed. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) large-import t-linter maintainer-merge 876/4 Mathlib.lean,Mathlib/Algebra/Group/Int/Defs.lean,Mathlib/Algebra/Group/Nat/Defs.lean,Mathlib/Algebra/Ring/Int/Defs.lean,Mathlib/Data/FunLike/Basic.lean,Mathlib/Data/SetLike/Basic.lean,Mathlib/Init.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/CommandStart.lean,Mathlib/Tactic/Simps/NotationClass.lean,MathlibTest/CommandStart.lean,MathlibTest/EuclideanSpace.lean,MathlibTest/Simps.lean,MathlibTest/Traversable.lean,MathlibTest/antidiagonal.lean,MathlibTest/delabLinearIndependent.lean,MathlibTest/matrix.lean,MathlibTest/norm_num.lean,MathlibTest/set_like.lean,MathlibTest/vec_notation.lean 20 89 ['Parcly-Taxel', 'adomani', 'eric-wieser', 'github-actions', 'grunweg', 'leanprover-community-bot-assistant'] grunweg
assignee:grunweg
4-31543
4 days ago
27-43236
27 days ago*
40-47955
40 days*
25265 FMLJohn
author:FMLJohn
 feat(Order/SupClosed): `compl_image_latticeClosure` and `compl_image_latticeClosure_eq_of_compl_image_eq_self` The main results in this pull request are: 1. `compl_image_latticeClosure`: given any Boolean algebra `α` and `s : Set α`, `compl '' latticeClosure s` is the same as `latticeClosure (compl '' s)`; 2. `compl_image_latticeClosure_eq_of_compl_image_eq_self`: given any Boolean algebra `α` and `s : Set α` such that `compl '' s = s`, we have `compl '' latticeClosure s = latticeClosure s`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-order 59/1 Mathlib/Order/SupClosed.lean 1 8 ['FMLJohn', 'YaelDillies', 'github-actions'] bryangingechen
assignee:bryangingechen
4-23003
4 days ago
7-2975
7 days ago
11-12593
11 days
25172 eric-wieser
author:eric-wieser
 feat: restricting `Affine.Simplex` to an affine subspace that contains it Also removes a redundant `Nonempty` argument. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-euclidean-geometry 68/5 Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean,Mathlib/LinearAlgebra/AffineSpace/Independent.lean 2 10 ['eric-wieser', 'github-actions', 'jsm28', 'ocfnash'] nobody
4-17046
4 days ago
15-27025
15 days ago
15-67897
15 days
25255 Raph-DG
author:Raph-DG
 feat(RingTheory): Order of vanishing in a ring In this PR we define the order of vanishing of a ring and its extension to elements of the function field (as in stacks project 02MD) as well as some basic API. Note that I'm slightly unsure that some of the lemmas used to prove this are at the right level of generality, and further I'm not quite sure where some of these lemmas belong (as indicated by the comments in the main OrderOfVanishing.lean file). Any comments about this would be very much appreciated. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge new-contributor t-algebra RFC
label:t-algebra$
 247/0 Mathlib.lean,Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean,Mathlib/RingTheory/Artinian/Module.lean,Mathlib/RingTheory/Ideal/Operations.lean,Mathlib/RingTheory/Ideal/Quotient/Operations.lean,Mathlib/RingTheory/OrderOfVanishing.lean 6 83 ['Raph-DG', 'chrisflav', 'erdOne', 'github-actions', 'jcommelin'] nobody
3-82277
3 days ago
3-82863
3 days ago
10-62245
10 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 21/1 Mathlib/Analysis/Normed/Operator/LinearIsometry.lean 1 7 ['Ruben-VandeVelde', 'eric-wieser', 'faenuccio', 'github-actions', 'jcommelin', 'qawbecrdtey'] faenuccio
assignee:faenuccio
3-57895
3 days ago
5-40535
5 days ago
32-57362
32 days
25059 s235282
author:s235282
 feat(Combinatorics/SimpleGraph/Bipartite): a graph is 2-colorable iff it's bipartite Define a predicate for a simple graph to be bipartite (`def IsBipartite (G : SimpleGraph V) : Prop := G.Colorable 2`) and prove ` G.IsBipartite ↔ ∃ s t : Set V, G.IsBipartiteWith s t`. --- This is my first attempt at contributing to mathlib and therefore I have a couple of points of uncertainty related to: - Naming conventions for theorems - Seeing a lot of isBipartite vs IsBipartite in the original work. What do we want to go with when? - Definition placement - Where should I put the IsBipartite definition. - Structure of biimplication theorems - Should I combine the different lemmas into 1 bgi theorem? Feedback is greatly appreciated :) [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) large-import maintainer-merge new-contributor t-combinatorics 36/3 Mathlib/Combinatorics/SimpleGraph/Bipartite.lean 1 30 ['YaelDillies', 'github-actions', 'mitchell-horner', 's235282'] nobody
2-37309
2 days ago
2-37856
2 days ago
8-85285
8 days
25089 Bergschaf
author:Bergschaf
 feat(Order/Sublocale): definition of sublocales There are several possible definition of sublocales. I used one from [nlab](https://ncatlab.org/nlab/show/sublocale) which states that a sublocale is a subset of a locale which is closed under all meets and for any ∈ S and x ∈ X, we have x ⇨ s ∈ S. This PR also includes an order isomorphism between (Nucleus)ᵒᵈ and Sublocale. --- I am open to better name suggestions for the order isomorphism. - [x] depends on: #24941 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-order 265/8 Mathlib.lean,Mathlib/Order/Hom/Lattice.lean,Mathlib/Order/Nucleus.lean,Mathlib/Order/Sublocale.lean,Mathlib/Order/Synonym.lean,docs/references.bib 6 71 ['Bergschaf', 'YaelDillies', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'xhalo32'] nobody
2-1809
2 days ago
2-1809
2 days ago
15-67631
15 days
25563 Komyyy
author:Komyyy
 chore: move `Topology.StoneCech` into `Topology.Compactification` (1/2) At present, the `Topology.Compactification` directory includes results on one-point compactifications, but results on Stone-Čech compactifications are currently located elsewhere. The removed file `Topology.Compactification` is deprecated in another PR (#25583) to leave a good git diff history. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) file-removed maintainer-merge t-topology 9/9 Mathlib.lean,Mathlib/Combinatorics/Hindman.lean,Mathlib/Topology/Category/CompHaus/Basic.lean,Mathlib/Topology/Category/CompHaus/Projective.lean,Mathlib/Topology/Category/Profinite/Projective.lean,Mathlib/Topology/Category/Stonean/Adjunctions.lean,Mathlib/Topology/Compactification/StoneCech.lean,Mathlib/Topology/ExtremallyDisconnected.lean,Mathlib/Topology/Maps/Proper/UniversallyClosed.lean,Mathlib/Topology/Separation/CompletelyRegular.lean 10 4 ['Komyyy', 'github-actions', 'grunweg'] nobody
1-42965
1 day ago
1-42965
1 day ago
2-18496
2 days
24382 joelriou
author:joelriou
 feat(CategoryTheory): pseudofunctors from strict bicategories This PR provides an API for pseudofunctors `F` from a strict bicategory `B`. In particular, this shall apply to pseudofunctors from locally discrete bicategories. We first introduce more flexible variants of `mapId` and `mapComp`: for example, if `f` and `g` are composable morphisms and `fg` is such that `h : fg = f ≫ f`, we provide an isomorphism `F.mapComp' f g fg h : F.map fg ≅ F.map f ≫ F.map g`. We study the compatibilities of these isomorphisms with respect to composition with identities and associativity. Secondly, given a commutative square `t ≫ r = l ≫ b` in `B`, we construct an isomorphism `F.map t ≫ F.map r ≅ F.map l ≫ F.map b`. Co-authored-by: Christian Merten --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-category-theory 168/0 Mathlib.lean,Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean,Mathlib/CategoryTheory/Bicategory/Functor/Strict.lean 3 17 ['callesonne', 'erdOne', 'github-actions', 'joelriou'] nobody
1-13411
1 day ago
1-79195
1 day ago
44-6763
44 days
25600 Komyyy
author:Komyyy
 refactor: lemma expressing `ContinuousAt` using a punctured neighbourhood --- This lemma is used to prove that the Riemann zeta function is meromorphic in #25597. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-topology 4/0 Mathlib/Topology/ContinuousOn.lean 1 5 ['Komyyy', 'github-actions', 'grunweg'] nobody
0-80082
22 hours ago
0-80082
22 hours ago
1-5568
1 day
21751 vihdzp
author:vihdzp
 refactor(SetTheory/Ordinal/Arithmetic): rework `Ordinal.pred` API This PR does the following: - give a simpler definition of `Ordinal.pred` - replace `¬ ∃ a, o = succ a` and `∀ a, o ≠ succ a` by `IsSuccPrelimit o` throughout - improve theorem names --- There's a legitimate question of whether we even want `Ordinal.pred` (see [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Ordinal.2Epred)) but this should be a good change in the meanwhile regardless. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-set-theory maintainer-merge merge-conflict 102/67 Mathlib/SetTheory/Ordinal/Arithmetic.lean,Mathlib/SetTheory/Ordinal/Exponential.lean 2 13 ['YaelDillies', 'github-actions', 'grunweg', 'vihdzp'] nobody
33-80652
1 month ago
80-59279
2 months ago
36-50134
36 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
6-63620
6 days ago
6-63621
6 days ago
10-26015
10 days
23961 FR-vdash-bot
author:FR-vdash-bot
 refactor: unbundle algebra from `ENormed*` Further speed up the search in the algebraic typeclass hierarchy by avoiding searching for `TopologicalSpace`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) slow-typeclass-synthesis maintainer-merge t-algebra t-analysis merge-conflict awaiting-author
label:t-algebra$
 32/25 Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/Analysis/Normed/Group/Continuity.lean,Mathlib/Analysis/NormedSpace/IndicatorFunction.lean,Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean 5 12 ['FR-vdash-bot', 'github-actions', 'grunweg', 'jcommelin', 'leanprover-bot', 'leanprover-community-bot-assistant'] nobody
2-47838
2 days ago
2-47838
2 days ago
17-72244
17 days

PRs from a fork of mathlib

Number Author Title Description Labels +/- Modified files (first 100) 📝 💬 All users who commented or reviewed Assignee(s) Updated Last status change total time in review
23772 SEU-Prime
author:SEU-Prime
 Create Amice.lean i built amice equiv [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-number-theory WIP 283/0 Mathlib/NumberTheory/Padics/Amice.lean 1 2 ['grunweg'] nobody
63-22448
2 months ago
63-22448
2 months ago
0-0
0 seconds
23986 ShouxinZhang
author:ShouxinZhang
 feat(FieldTheory/RatFunc): add RatFunc.toFractionRingAlgEquiv --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) will-close-soon t-algebra
label:t-algebra$
 17/0 Mathlib/FieldTheory/RatFunc/Basic.lean 1 1 ['joneugster'] nobody
52-81630
1 month ago
52-81630
1 month ago
0-0
0 seconds
25516 kim-em
author:kim-em
 chore: test PR from fork This PR tests making a PR from a fork. 1/0 Mathlib/Computability/AkraBazzi/AkraBazzi.lean 1 1 ['bryangingechen'] nobody
3-22889
3 days ago
3-59392
3 days ago
0-0
0 seconds
25537 literandltx
author:literandltx
 feat(number_theory/legendre_symbol): Add sqrt‐of‐residue theorems for p=4k+3 and p=8k+5 Add a new file `QuadraticResidueRoots.lean` under `Mathlib/NumberTheory/LegendreSymbol/` that proves two explicit “square-root of quadratic residue” theorems for primes of the specific form. - **`exists_sqrt_of_residue_mod4_eq3`** for primes `p = 4*k + 3` - **`exists_sqrt_of_residue_mod8_eq5`** for primes `p = 8*k + 5` It also introduces the helper lemmas `euler_criterion_traditional` and `legendreSym.at_two_mod8_eq_5`. Import lines in `Mathlib.lean` and `Mathlib/NumberTheory/LegendreSymbol/Basic.lean` have been updated accordingly. new-contributor 217/0 Mathlib.lean,Mathlib/NumberTheory/LegendreSymbol/Basic.lean,Mathlib/NumberTheory/LegendreSymbol/QuadraticReciprocity.lean,Mathlib/NumberTheory/LegendreSymbol/QuadraticResidueRoots.lean 4 0 [] nobody
3-20589
3 days ago
3-20589
3 days ago
0-0
0 seconds
25599 adomani
author:adomani
 test: autolabel from forks --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) test-ci awaiting-author WIP 1/1 Mathlib/Tactic/Eval.lean,newFileOnMaster.md 2 3 ['adomani', 'bryangingechen', 'github-actions'] nobody
0-34663
9 hours ago
1-10125
1 day ago
0-0
0 seconds
25623 mattrobball
author:mattrobball
 feat: decidable equality for `Quiver.Path` Given a quiver with decidable equality on its vertices and arrows, we construct an instance of decidable equality for `Quiver.Path`. We proceed through a recursion on the length of the path utilizing an intermediate subtype of uniformly bounded paths `Quiver.Path.BoundedPath`. This was motivated by doing computations on small quivers with Lean. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) 69/0 Mathlib/Combinatorics/Quiver/Path.lean 1 1 ['github-actions'] nobody
0-23368
6 hours ago
0-23457
6 hours ago
0-0
0 seconds
3610 TimothyGu
author:TimothyGu
 feat: derive Infinite automatically for inductive types Deals with recursive types, but not mutually recursive types or types with indices right now. See docstring for details. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-meta merge-conflict awaiting-author 517/0 Mathlib.lean,Mathlib/Tactic/DeriveInfinite.lean,test/DeriveInfinite.lean 3 11 ['TimothyGu', 'digama0', 'eric-wieser', 'grunweg', 'kim-em', 'kmill'] kmill
assignee:kmill
155-57260
5 months ago
155-57260
5 months ago
0-0
0 seconds

PRs blocked on a zulip discussion

Number Author Title Description Labels +/- Modified files (first 100) 📝 💬 All users who commented or reviewed Assignee(s) Updated Last status change total time in review
23866 kim-em
author:kim-em
 chore: remove `[AtLeastTwo n]` hypothesis from the `NatCast` to `OfNat` instance This PR observes that we can change ``` instance (priority := 100) instOfNatAtLeastTwo {n : ℕ} [NatCast R] [Nat.AtLeastTwo n] : OfNat R n ``` to ``` instance (priority := 100) instOfNatAtLeastTwo {n : ℕ} [NatCast R] : OfNat R n ``` with minimal fall-out. A follow-up PR #23867 then observes that we can remove nearly all the `[Nat.AtLeastTwo n]` hypotheses in Mathlib. This is slightly dangerous -- it does make it more likely that we'll generate non-defeq instances, but it appears to happen very rarely. However, it will make life slightly easier for something Leo and I are trying to do with `grind` and Grobner bases (we'd like to be able to assume types we consume have `[∀ n, OfNat α n]`, which is possible with this change, but not without...). Zulip thread: [#PR reviews > #23866 and #23867, removing most `[Nat.AtLeastTwo n]` @ 💬](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2323866.20and.20.2323867.2C.20removing.20most.20.60.5BNat.2EAtLeastTwo.20n.5D.60/near/511157297) awaiting-zulip 21/26 Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean,Mathlib/Data/Nat/Cast/Defs.lean,Mathlib/Data/Nat/Cast/Order/Basic.lean 3 3 ['eric-wieser', 'github-actions', 'urkud'] nobody
61-4882
2 months ago
61-4971
2 months ago
0-23929
6 hours
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
34-78759
1 month ago
34-78768
1 month 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
34-78070
1 month ago
34-78705
1 month ago
75-77754
75 days
23048 scholzhannah
author:scholzhannah
 feat: PartialEquiv on closed sets restricts to closed map This PR shows that a PartialEquiv that is continuous on both source and target restricts to a homeomorphism. It then uses that to show that a PartialEquiv with closed source and target and which is continuous on both the source and target restricts to a closed map. --- See [this Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Generalizing.20.60PartialHomeomorph.60.3F) that will probably mean that I close this PR. I need the latter statement to prove that one can transport a CW complex along a PartialEquiv. I had trouble finding a good spot for these statements; I hope this solution works. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-topology 53/0 Mathlib.lean,Mathlib/Topology/PartialEquiv.lean 2 3 ['ADedecker', 'github-actions', 'scholzhannah'] ADedecker
assignee:ADedecker
27-16254
27 days ago
31-23030
1 month ago
51-86236
51 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
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 11 ['MichaelStollBayreuth', 'acmepjz', 'eric-wieser', 'github-actions', 'leanprover-bot', 'urkud'] nobody
21-64720
21 days ago
21-85147
21 days ago
0-66650
18 hours
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
5-44530
5 days ago
34-78669
1 month ago
48-67492
48 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/) awaiting-zulip new-contributor t-algebraic-geometry 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 29 ['MichaelStollBayreuth', 'Multramate', 'acmepjz', 'github-actions', 'grunweg', 'kckennylau'] nobody
3-80611
3 days ago
7-33023
7 days ago
6-51040
6 days
23658 grunweg
author:grunweg
 feat: require that real or complex models with corners have convex interior Follow-up to #18403. --- - [x] depends on: #23657 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-differential-geometry WIP 116/18 Mathlib/Geometry/Manifold/Instances/Real.lean,Mathlib/Geometry/Manifold/IsManifold/Basic.lean 2 5 ['github-actions', 'grunweg', 'mathlib4-dependent-issues-bot', 'sgouezel'] nobody
2-31879
2 days ago
6-15326
6 days ago
0-9
9 seconds
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
2-1921
2 days ago
2-1922
2 days ago
34-10595
34 days
11800 JADekker
author:JADekker
 feat : Define KappaLindelöf spaces Define KappaLindelöf spaces by following the first one-third of the API for Lindelöf spaces. The remainder will be added in a future PR. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-topology merge-conflict please-adopt 301/2 Mathlib.lean,Mathlib/Topology/Compactness/KappaLindelof.lean,Mathlib/Topology/Compactness/Lindelof.lean 3 38 ['ADedecker', 'JADekker', 'PatrickMassot', 'StevenClontz', 'adomani', 'github-actions', 'grunweg', 'kim-em', 'urkud'] nobody
266-55792
8 months ago
266-77767
8 months ago
119-10687
119 days
17518 grunweg
author:grunweg
 feat: lint on declarations mentioning `Invertible` or `Unique` Using the same infrastructure as for #10235. Depends on that PR to land first, and also (for the first lint) a zulip discussion if that change is desired/about the best way to enact it. --- - [ ] depends on: #10235 awaiting-zulip t-linter merge-conflict blocked-by-other-PR 149/7 Mathlib.lean,Mathlib/Algebra/MvPolynomial/PDeriv.lean,Mathlib/Computability/Halting.lean,Mathlib/Computability/TuringMachine.lean,Mathlib/Data/Fintype/Card.lean,Mathlib/GroupTheory/Perm/DomMulAct.lean,Mathlib/Logic/Basic.lean,Mathlib/Logic/Encodable/Basic.lean,Mathlib/NumberTheory/JacobiSum/Basic.lean,Mathlib/Order/Heyting/Regular.lean,Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/UnusedAssumptionInType.lean 13 3 ['github-actions', 'mathlib4-dependent-issues-bot', 'mergify'] nobody
219-9511
7 months ago
244-84433
8 months ago*
0-0
0 seconds*
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
201-29042
6 months ago
201-29042
6 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
45-70819
1 month ago
57-13049
1 month ago
29-60989
29 days
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
34-78719
1 month ago
34-78724
1 month ago
0-179
2 minutes
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
21-14925
21 days ago
21-14926
21 days 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
21-13999
21 days ago
21-14001
21 days ago
39-67601
39 days
24409 urkud
author:urkud
 chore(*): fix `nmem` vs `not_mem` names --- There are some missing/buggy deprecations, I'm going to fix them later today or tomorrow. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip tech debt merge-conflict delegated awaiting-author 317/176 Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Algebra/BigOperators/Group/Finset/Lemmas.lean,Mathlib/Algebra/Group/Indicator.lean,Mathlib/Algebra/Group/Support.lean,Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean,Mathlib/Algebra/Order/Group/Indicator.lean,Mathlib/Algebra/Polynomial/AlgebraMap.lean,Mathlib/Algebra/Polynomial/Degree/Operations.lean,Mathlib/Analysis/Calculus/BumpFunction/Basic.lean,Mathlib/Analysis/Calculus/DSlope.lean,Mathlib/Analysis/Calculus/Deriv/Basic.lean,Mathlib/Analysis/Calculus/Deriv/Support.lean,Mathlib/Analysis/Calculus/FDeriv/Basic.lean,Mathlib/Analysis/Calculus/Rademacher.lean,Mathlib/Analysis/Complex/RemovableSingularity.lean,Mathlib/Analysis/Convex/Cone/InnerDual.lean,Mathlib/Analysis/Convex/Cone/Proper.lean,Mathlib/Analysis/Convolution.lean,Mathlib/Analysis/Distribution/AEEqOfIntegralContDiff.lean,Mathlib/Data/LocallyFinsupp.lean,Mathlib/Data/Set/Basic.lean,Mathlib/Data/Set/Insert.lean,Mathlib/Dynamics/Ergodic/Conservative.lean,Mathlib/Dynamics/Ergodic/Ergodic.lean,Mathlib/Dynamics/Ergodic/Function.lean,Mathlib/Dynamics/PeriodicPts/Defs.lean,Mathlib/Geometry/Manifold/ContMDiff/Basic.lean,Mathlib/Geometry/Manifold/PartitionOfUnity.lean,Mathlib/GroupTheory/CosetCover.lean,Mathlib/LinearAlgebra/Dual/Lemmas.lean,Mathlib/LinearAlgebra/FreeModule/PID.lean,Mathlib/LinearAlgebra/PID.lean,Mathlib/LinearAlgebra/RootSystem/Base.lean,Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean,Mathlib/MeasureTheory/Function/ContinuousMapDense.lean,Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean,Mathlib/MeasureTheory/Function/L2Space.lean,Mathlib/MeasureTheory/Function/LocallyIntegrable.lean,Mathlib/MeasureTheory/Function/LpSpace/Indicator.lean,Mathlib/MeasureTheory/Integral/Average.lean,Mathlib/MeasureTheory/Integral/Bochner/Set.lean,Mathlib/MeasureTheory/Integral/Layercake.lean,Mathlib/MeasureTheory/Integral/Lebesgue/Add.lean,Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean,Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Basic.lean,Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Real.lean,Mathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean,Mathlib/MeasureTheory/Measure/AddContent.lean,Mathlib/MeasureTheory/Measure/DiracProba.lean,Mathlib/MeasureTheory/Measure/Haar/Unique.lean,Mathlib/MeasureTheory/Measure/Restrict.lean,Mathlib/MeasureTheory/Measure/WithDensity.lean,Mathlib/MeasureTheory/OuterMeasure/AE.lean,Mathlib/MeasureTheory/SetSemiring.lean,Mathlib/Order/Filter/AtTopBot/CountablyGenerated.lean,Mathlib/Order/Filter/Cocardinal.lean,Mathlib/Order/Filter/Cofinite.lean,Mathlib/Order/Filter/Tendsto.lean,Mathlib/Order/Filter/Ultrafilter/Basic.lean,Mathlib/Probability/Distributions/Uniform.lean,Mathlib/Probability/Kernel/Basic.lean,Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean,Mathlib/RingTheory/AdicCompletion/LocalRing.lean,Mathlib/RingTheory/Ideal/Maximal.lean,Mathlib/RingTheory/LaurentSeries.lean,Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean,Mathlib/RingTheory/MvPowerSeries/NoZeroDivisors.lean,Mathlib/RingTheory/Spectrum/Maximal/Localization.lean,Mathlib/RingTheory/Spectrum/Prime/RingHom.lean,Mathlib/RingTheory/Spectrum/Prime/Topology.lean,Mathlib/Topology/Algebra/InfiniteSum/Group.lean,Mathlib/Topology/Algebra/Module/Cardinality.lean,Mathlib/Topology/Algebra/Support.lean,Mathlib/Topology/Bases.lean,Mathlib/Topology/ContinuousMap/BoundedCompactlySupported.lean,Mathlib/Topology/Order/Basic.lean,Mathlib/Topology/UrysohnsLemma.lean 77 4 ['b-mehta', 'github-actions', 'jcommelin', 'leanprover-community-bot-assistant', 'mathlib-bors'] nobody
7-49897
7 days ago
7-49897
7 days ago
0-55045
15 hours
24396 JovanGerb
author:JovanGerb
 feat(Order/Defs): refactor in preparation of `to_dual` attribute When the `to_dual` attribute lands in Mathlib, we will tag many lemmas about order with this tag, which will automatically give us the dual statements. This PR prepares for this by - moving dual declarations closer together - replacing occurrences of `>` and `≥` with `<` and `≤` - consistently applying a new naming convention that helps us to name dual lemmas: we use the keywords `ge` and `gt` in place of `le` and `lt` to indicate that the same pair `a, b` in `a < b` is in the opposite order to the order in which it appeared the first time. - when we have to disambiguate the order of the argument to `<` or `≤`, we sometimes use `gt` or `ge` instead of `lt` or `le`. We also use this to get rid of many primed lemma names. This is a copy of #24376, but it doesn't remove the old lemma names, so doesn't require making changes in >500 files. deprecating these lemmas will be left to a future PR. [#mathlib4 > naming convention for ≤ and <](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/naming.20convention.20for.20.E2.89.A4.20and.20.3C) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-order merge-conflict 248/230 Mathlib/Algebra/Order/CauSeq/Basic.lean,Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean,Mathlib/Algebra/Polynomial/Degree/Domain.lean,Mathlib/Algebra/Tropical/Basic.lean,Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean,Mathlib/Computability/TuringMachine.lean,Mathlib/Data/Bool/Basic.lean,Mathlib/Data/Char.lean,Mathlib/Data/Complex/Order.lean,Mathlib/Data/ENat/Basic.lean,Mathlib/Data/Int/Order/Basic.lean,Mathlib/Data/Nat/Basic.lean,Mathlib/Data/Nat/Factorization/Defs.lean,Mathlib/Data/Nat/Find.lean,Mathlib/Data/Nat/PartENat.lean,Mathlib/Data/Num/Lemmas.lean,Mathlib/Data/Num/ZNum.lean,Mathlib/Data/PSigma/Order.lean,Mathlib/Data/Prod/Lex.lean,Mathlib/Data/Real/Basic.lean,Mathlib/Data/Setoid/Basic.lean,Mathlib/Data/Setoid/Partition.lean,Mathlib/Data/Sigma/Order.lean,Mathlib/Data/String/Basic.lean,Mathlib/Data/Sum/Order.lean,Mathlib/GroupTheory/MonoidLocalization/Order.lean,Mathlib/NumberTheory/Zsqrtd/Basic.lean,Mathlib/Order/Antisymmetrization.lean,Mathlib/Order/Basic.lean,Mathlib/Order/Booleanisation.lean,Mathlib/Order/Defs/LinearOrder.lean,Mathlib/Order/Defs/PartialOrder.lean,Mathlib/Order/RelClasses.lean,Mathlib/Order/WithBot.lean,Mathlib/Probability/Martingale/Upcrossing.lean,Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicity.lean,Mathlib/SetTheory/Game/Basic.lean,Mathlib/SetTheory/Ordinal/Basic.lean,Mathlib/SetTheory/Ordinal/Notation.lean,Mathlib/SetTheory/Surreal/Basic.lean,Mathlib/Tactic/Linarith/Frontend.lean,MathlibTest/linarith.lean 43 5 ['JovanGerb', 'bryangingechen', 'github-actions', 'leanprover-community-bot-assistant'] bryangingechen
assignee:bryangingechen
7-11999
7 days ago
7-12001
7 days ago
5-75236
5 days

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

Number Author Title Description Labels +/- Modified files (first 100) 📝 💬 All users who commented or reviewed Assignee(s) Updated Last status change total time in review
25556 Parcly-Taxel
author:Parcly-Taxel
 chore: remove >6 month old material in `Deprecated` file-removed tech debt 0/250 Mathlib.lean,Mathlib/Deprecated/Cardinal/Continuum.lean,Mathlib/Deprecated/Cardinal/Finite.lean,Mathlib/Deprecated/Cardinal/PartENat.lean,Mathlib/Deprecated/Order.lean 5 1 ['github-actions'] nobody
2-56647
2 days ago
2-56700
2 days ago
2-56757
2 days
25580 Parcly-Taxel
author:Parcly-Taxel
 chore: deprime `induction` in `AlgebraicTopology/CategoryTheory` Most replacements that are also in #23676 have been copied over, but some have been optimised further. tech debt 134/125 Mathlib/AlgebraicTopology/DoldKan/Decomposition.lean,Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean,Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean,Mathlib/AlgebraicTopology/DoldKan/Projections.lean,Mathlib/AlgebraicTopology/SimplexCategory/MorphismProperty.lean,Mathlib/AlgebraicTopology/SimplicialObject/Split.lean,Mathlib/AlgebraicTopology/SimplicialSet/Degenerate.lean,Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean,Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean,Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean,Mathlib/CategoryTheory/Abelian/GrothendieckCategory/Subobject.lean,Mathlib/CategoryTheory/Action/Concrete.lean,Mathlib/CategoryTheory/Action/Monoidal.lean,Mathlib/CategoryTheory/ComposableArrows.lean,Mathlib/CategoryTheory/Extensive.lean,Mathlib/CategoryTheory/Filtered/Basic.lean,Mathlib/CategoryTheory/Galois/Decomposition.lean,Mathlib/CategoryTheory/Galois/EssSurj.lean,Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean,Mathlib/CategoryTheory/Limits/Shapes/SequentialProduct.lean,Mathlib/CategoryTheory/Limits/Types/Colimits.lean,Mathlib/CategoryTheory/Limits/VanKampen.lean,Mathlib/CategoryTheory/Quotient.lean,Mathlib/CategoryTheory/Sites/Sheaf.lean,Mathlib/CategoryTheory/Subobject/Basic.lean,Mathlib/CategoryTheory/Subobject/FactorThru.lean,Mathlib/CategoryTheory/Subobject/Lattice.lean,Mathlib/CategoryTheory/Triangulated/TStructure/Basic.lean 28 3 ['Parcly-Taxel', 'eric-wieser', 'github-actions'] nobody
1-31786
1 day ago
1-57862
1 day ago
1-57846
1 day
22603 pechersky
author:pechersky
 chore(Topology): rename pi family from π to X Only in files that mentioned such a family, via a script: ``` git grep -e "π : . → Type" --name-only | rg Topology | xargs -I{} sed -i -e 's/π/X/g' {} ``` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) tech debt t-topology 238/238 Mathlib/Topology/AlexandrovDiscrete.lean,Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean,Mathlib/Topology/Algebra/Module/Equiv.lean,Mathlib/Topology/Algebra/Order/LiminfLimsup.lean,Mathlib/Topology/Bases.lean,Mathlib/Topology/Bornology/Constructions.lean,Mathlib/Topology/Connected/Basic.lean,Mathlib/Topology/Connected/Clopen.lean,Mathlib/Topology/Connected/LocallyConnected.lean,Mathlib/Topology/Connected/TotallyDisconnected.lean,Mathlib/Topology/Constructions.lean,Mathlib/Topology/ContinuousOn.lean,Mathlib/Topology/EMetricSpace/Diam.lean,Mathlib/Topology/EMetricSpace/Pi.lean,Mathlib/Topology/ExtremallyDisconnected.lean,Mathlib/Topology/Inseparable.lean,Mathlib/Topology/MetricSpace/Basic.lean,Mathlib/Topology/MetricSpace/Infsep.lean,Mathlib/Topology/MetricSpace/ProperSpace.lean,Mathlib/Topology/MetricSpace/Pseudo/Pi.lean,Mathlib/Topology/Metrizable/Basic.lean,Mathlib/Topology/Order/Basic.lean,Mathlib/Topology/Separation/Hausdorff.lean,Mathlib/Topology/UniformSpace/Ascoli.lean 24 1 ['github-actions'] nobody
0-67128
18 hours ago
0-67150
18 hours ago
6-60764
6 days
23676 Parcly-Taxel
author:Parcly-Taxel
 chore: deprime `induction` for localizations and quotients All these removed instances of `induction'` generate only one subgoal. In some cases `obtain` can be used. The relevant instances were identified by adding the following to `Mathlib.Tactic.Cases` ```diff diff --git a/Mathlib/Tactic/Cases.lean b/Mathlib/Tactic/Cases.lean index 4a60db6c551..08c06520879 100644 --- a/Mathlib/Tactic/Cases.lean +++ b/Mathlib/Tactic/Cases.lean @@ -122,6 +122,16 @@ elab (name := induction') "induction' " tgts:(Parser.Tactic.elimTarget,+) g.assign result.elimApp let subgoals ← ElimApp.evalNames elimInfo result.alts withArg (generalized := fvarIds) (toClear := targetFVarIds) (toTag := toTag) + let body ← inferType targets[0]! + let names : Array Format := if withArg.1.getArgs.size > 1 then + (withArg.1.getArgs[1]!).getArgs.map Syntax.prettyPrint else Array.empty + let gens : Array Format := if genArg.1.getArgs.size > 1 then + (genArg.1.getArgs[1]!).getArgs.map Syntax.prettyPrint else Array.empty + let inductor : Format := if usingArg.1.getArgs.size > 1 then + Syntax.prettyPrint usingArg.1.getArgs[1]! else "~" + if subgoals.toList.length ≤ 1 then + logInfoAt tgts m!"{body.getAppFn.setPPExplicit true} {inductor} {gens} {names} \ + {subgoals.toList.length}" setGoals <| (subgoals ++ result.others).toList ++ gs /-- The `cases'` tactic is similar to the `cases` tactic in Lean 4 core, but the syntax for giving ``` and then examining [the output](https://github.com/leanprover-community/mathlib4/actions/runs/14270845291/job/40003467676). tech debt 71/77 Mathlib/Algebra/Module/LocalizedModule/Basic.lean,Mathlib/Algebra/Pointwise/Stabilizer.lean,Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean,Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean,Mathlib/CategoryTheory/Action/Concrete.lean,Mathlib/CategoryTheory/Galois/EssSurj.lean,Mathlib/CategoryTheory/Limits/Types/Colimits.lean,Mathlib/CategoryTheory/Subobject/Basic.lean,Mathlib/CategoryTheory/Subobject/FactorThru.lean,Mathlib/CategoryTheory/Subobject/Lattice.lean,Mathlib/Data/Finset/NoncommProd.lean,Mathlib/Data/Finsupp/BigOperators.lean,Mathlib/Data/Fintype/Quotient.lean,Mathlib/Data/List/Cycle.lean,Mathlib/Data/Nat/ChineseRemainder.lean,Mathlib/Data/Setoid/Partition.lean,Mathlib/GroupTheory/Perm/Sign.lean,Mathlib/RingTheory/OreLocalization/Basic.lean,Mathlib/RingTheory/OreLocalization/Ring.lean 19 11 ['Parcly-Taxel', 'apnelson1', 'eric-wieser', 'github-actions', 'grunweg', 'leanprover-community-bot-assistant', 'urkud'] nobody
0-52678
14 hours ago
2-1648
2 days ago
63-66025
63 days
25617 Parcly-Taxel
author:Parcly-Taxel
 chore: fix more induction/recursor branch names These were found using the regex `\| h. =>` and `def.*rec.*\(h. :`. tech debt 88/79 Mathlib/Analysis/Convolution.lean,Mathlib/Data/ENat/Basic.lean,Mathlib/Data/Fin/Tuple/Basic.lean,Mathlib/Data/Fin/Tuple/NatAntidiagonal.lean,Mathlib/Data/Nat/Factorization/Induction.lean,Mathlib/Data/Seq/Computation.lean,Mathlib/Data/Set/Card.lean,Mathlib/Data/WSeq/Basic.lean,Mathlib/FieldTheory/KummerExtension.lean,Mathlib/Logic/Function/Iterate.lean,Mathlib/NumberTheory/ArithmeticFunction.lean,Mathlib/NumberTheory/SumFourSquares.lean,Mathlib/NumberTheory/SumTwoSquares.lean,Mathlib/Order/Synonym.lean 14 1 ['github-actions'] nobody
0-32980
9 hours ago
0-43779
12 hours ago
0-43762
12 hours