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: April 14, 2026 at 15:38 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
36216 michaellee94
author:michaellee94
 feat(CategoryTheory): characterize pullback squares via the `Over` category --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-category-theory new-contributor maintainer-merge awaiting-author 47/0 Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean 1 18 ['dagurtomas', 'github-actions', 'joelriou', 'michaellee94'] robin-carlier
assignee:robin-carlier
18-67335
18 days ago
18-67335
18 days ago
2-50782
2 days
37738 khwilson
author:khwilson
 feat(Topology/Order/Bornology): generalize `cobounded_eq` `Real.cobounded_eq` and `Int.cobounded_eq` are used in several places throughout Mathlib. They are currently proved in terms of the Metric topology on `Int` and `Real`, but they're really properties of the order bornology on those objects. Generalize those constructions to `IsOrderBornology` for `LinearOrder`'s and add a few more constructions that are true in other circumstances, e.g., `cobounded NNReal = .atTop` follows from the fact that `NNReal` is both `NoMaxOrder` and `OrderBot`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-order 57/18 Mathlib/Analysis/Polynomial/Basic.lean,Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean,Mathlib/Topology/Instances/Int.lean,Mathlib/Topology/Instances/Real/Lemmas.lean,Mathlib/Topology/Order/Bornology.lean 5 14 ['YaelDillies', 'github-actions', 'khwilson', 'vihdzp'] nobody
6-59051
6 days ago
7-10597
7 days ago
7-11435
7 days
37057 erdOne
author:erdOne
 feat(AlgebraicTopology): `SimplexCategory.toTop_map_δ_apply` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebraic-topology maintainer-merge awaiting-author merge-conflict 48/2 Mathlib/AlgebraicTopology/CechNerve.lean,Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean,Mathlib/AlgebraicTopology/SimplexCategory/Defs.lean,Mathlib/AlgebraicTopology/TopologicalSimplex.lean,Mathlib/Data/Fin/SuccPred.lean 5 17 ['Raph-DG', 'dagurtomas', 'erdOne', 'github-actions', 'joelriou', 'mathlib-merge-conflicts', 'riccardobrasca'] robin-carlier
assignee:robin-carlier
6-34138
6 days ago
7-81778
7 days ago
4-49805
4 days
37544 SnirBroshi
author:SnirBroshi
 chore(Combinatorics/SimpleGraph/Coloring): move `ConcreteColorings.lean` and `EdgeLabeling.lean` to `Coloring/` Moves `SimpleGraph/ConcreteColorings.lean` to `SimpleGraph/Coloring/Constructions.lean` and `SimpleGraph/EdgeLabeling.lean` to `SimpleGraph/Coloring/EdgeLabeling.lean`. See [Zulip](https://leanprover.zulipchat.com/#narrow/channel/252551-graph-theory/topic/Coloring.20module.20names/with/583281500) --- [Zulip](https://leanprover.zulipchat.com/#narrow/channel/252551-graph-theory/topic/Coloring.20module.20names/with/583281500) might want to rename `ConcreteColorings` (Edit: the poll chose `Constructions.lean`) #37546 adds module deprecations [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) file-removed t-combinatorics maintainer-merge 2/2 Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Coloring/Constructions.lean,Mathlib/Combinatorics/SimpleGraph/Coloring/EdgeLabeling.lean 3 2 ['YaelDillies', 'github-actions', 'ooovi'] nobody
6-23367
6 days ago
9-3819
9 days ago
9-3958
9 days
37603 Parcly-Taxel
author:Parcly-Taxel
 refactor: review of `SetSemiring` * Rename `Set.up` and `SetSemiring.down` to `SetSemiring.ofSet` and `SetSemiring.toSet` respectively. Unprotect both and make them equivalences, following `FreeMonoid`. * Derive `CompleteAtomicBooleanAlgebra` for `SetSemiring` immediately. * Add `imageHom_id` and `imageHom_comp`. The three existing lemmas about `imageHom` are coalesced into `imageHom_apply`. Ultimately inspired by https://github.com/leanprover-community/mathlib4/pull/36934#issuecomment-4183475568. maintainer-merge 120/165 Mathlib/Algebra/Algebra/Operations.lean,Mathlib/Data/Set/Semiring.lean 2 41 ['Parcly-Taxel', 'YaelDillies', 'eric-wieser', 'github-actions', 'mathlib-merge-conflicts', 'sgouezel'] nobody
6-4125
6 days ago
6-4383
6 days ago
7-31782
7 days
37291 IvanRenison
author:IvanRenison
 refactor(Combinatorics/SimpleGraph): move `chromaticNumber_le_two_iff_isBipartite` and `chromaticNumber_eq_two_iff` to `Bipartite` file --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-combinatorics maintainer-merge 10/12 Mathlib/Combinatorics/SimpleGraph/Bipartite.lean,Mathlib/Combinatorics/SimpleGraph/ConcreteColorings.lean 2 2 ['Ruben-VandeVelde', 'github-actions'] nobody
4-71709
4 days ago
17-59517
17 days ago
17-59512
17 days
37400 SnirBroshi
author:SnirBroshi
 feat(Combinatorics/SimpleGraph/Acyclic): endpoints of a path have at most one neighbor in the path --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-combinatorics maintainer-merge 15/0 Mathlib/Combinatorics/SimpleGraph/Acyclic.lean 1 4 ['Rida-Hamadani', 'Ruben-VandeVelde', 'github-actions'] nobody
4-70616
4 days ago
14-46512
14 days ago
14-46507
14 days
37420 artie2000
author:artie2000
 refactor: change definitions to avoid `ConvexCone` Change the definitions of `PointedCone.positive` and `PointedCone.closure` to avoid mentioning `ConvexCone`. This PR is part of a series deprecating `ConvexCone`: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Replacing.20.60ConvexCone.60.20with.20.60PointedCone.60/with/582738985 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-convex-geometry maintainer-merge 10/4 Mathlib/Analysis/Convex/Cone/Closure.lean,Mathlib/Geometry/Convex/Cone/Pointed.lean 2 2 ['YaelDillies', 'github-actions', 'ooovi', 'vihdzp'] nobody
4-39530
4 days ago
14-23371
14 days ago
14-23503
14 days
36416 j-loreaux
author:j-loreaux
 feat(Analysis/CStarAlgebra): norms of sums of orthogonal selfadjoint elements --- - [ ] depends on: #36407 - [ ] depends on: #37569 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-analysis maintainer-merge 130/1 Mathlib/Algebra/Star/BigOperators.lean,Mathlib/Algebra/Star/SelfAdjoint.lean,Mathlib/Analysis/CStarAlgebra/Fuglede.lean,Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean 4 22 ['github-actions', 'grunweg', 'j-loreaux', 'loefflerd', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'themathqueen'] loefflerd
assignee:loefflerd
4-28553
4 days ago
4-44128
4 days ago
10-23153
10 days
33443 sahanwijetunga
author:sahanwijetunga
 feat: Define Isometries of Bilinear Spaces --- We define Isometries of Bilinear Spaces, closely following the implementation of isometries of quadratic spaces. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebra new-contributor maintainer-merge
label:t-algebra$
 278/0 Mathlib.lean,Mathlib/LinearAlgebra/BilinearForm/Isometry.lean,Mathlib/LinearAlgebra/BilinearForm/IsometryEquiv.lean 3 25 ['github-actions', 'robin-carlier', 'sahanwijetunga'] mattrobball
assignee:mattrobball
4-28372
4 days ago
4-28531
4 days ago
52-55634
52 days
36401 JovanGerb
author:JovanGerb
 feat(positivity): positivity extension for `a - b` This PR adds support in `positivity` for proving things about subtraction. For example, if the goal is `0 < a - b`, and there is a local hypothesis of type `b < a`, then we close the goal. The motivation is that we want `positivity` to be a flexible tactic. So, when trying to prove `0 < a - b` using a local hypothesis, we should look for the simp normal form of this, which is `b < a`. --- [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Can.20I.20make.20positivity.20work.20for.20this.3F/near/578277240) [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-meta maintainer-merge 63/26 Mathlib/Analysis/Calculus/Taylor.lean,Mathlib/Analysis/Complex/AbelLimit.lean,Mathlib/Analysis/Complex/BorelCaratheodory.lean,Mathlib/Analysis/Complex/Hadamard.lean,Mathlib/Analysis/Convex/BetweenList.lean,Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean,Mathlib/Analysis/SpecificLimits/FloorPow.lean,Mathlib/Geometry/Manifold/Riemannian/PathELength.lean,Mathlib/Tactic/Positivity/Basic.lean,MathlibTest/positivity.lean 10 10 ['JovanGerb', 'github-actions', 'hrmacbeth', 'j-loreaux', 'joneugster', 'leanprover-radar'] joneugster
assignee:joneugster
4-17074
4 days ago
4-20987
4 days ago
21-78285
21 days
37846 grunweg
author:grunweg
 fix(positivity): still prove non-negativity in the `Nat.cast` extension if positivity fails --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-meta maintainer-merge 11/2 Mathlib/Tactic/Positivity/Basic.lean,MathlibTest/positivity.lean 2 4 ['dwrensha', 'github-actions'] dwrensha
assignee:dwrensha
3-50419
3 days ago
4-12639
4 days ago
4-12636
4 days
35906 scp020
author:scp020
 feat(Combinatorics/SimpleGraph/Walk): chords of walks Define `Walk.IsChord` and `Walk.IsChordless` predicates in a new file `SimpleGraph/Walk/Chord.lean`. See "chord" in https://en.wikipedia.org/wiki/Glossary_of_graph_theory --- [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Walk.2EIsChordless.20live.20in.20mathlib.3F/with/575277309) [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-combinatorics new-contributor maintainer-merge 59/0 Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Walk/Chord.lean 2 68 ['SnirBroshi', 'YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'scp020'] YaelDillies
assignee:YaelDillies
3-32100
3 days ago
9-50517
9 days ago
34-40377
34 days
36308 SnirBroshi
author:SnirBroshi
 feat(Combinatorics/SimpleGraph/Subgraph): a couple of `subgraphOfAdj` lemmas Also golf a lemma (it's one line longer but it looks simpler to me). --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-combinatorics maintainer-merge 14/5 Mathlib/Combinatorics/SimpleGraph/Subgraph.lean 1 3 ['YaelDillies', 'github-actions'] nobody
2-29033
2 days ago
38-31885
38 days ago
38-31880
38 days
34854 GrigorenkoPV
author:GrigorenkoPV
 chore(Combinatorics/Enumerative/Catalan): split into `Basic` & `Tree` --- Split off from #34853 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) new-contributor t-combinatorics maintainer-merge 225/194 Mathlib.lean,Mathlib/Combinatorics/Enumerative/Catalan.lean,Mathlib/Combinatorics/Enumerative/Catalan/Basic.lean,Mathlib/Combinatorics/Enumerative/Catalan/Tree.lean,Mathlib/Combinatorics/Enumerative/DyckWord.lean,Mathlib/RingTheory/PowerSeries/Catalan.lean 6 6 ['SnirBroshi', 'YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'vihdzp'] nobody
2-16458
2 days ago
2-16455
2 days ago
45-59230
45 days
37506 wwylele
author:wwylele
 feat(Analysis/InnerProductSpace): singleton basis for 1d space This was brought up in #36462. Similar to existing `FiniteDimensional.basisSingleton`, this provides a OrthonormalBasis version. Also adds simp lemma for `∀ (i j : ι), P i j` for subsingleton `ι`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-analysis maintainer-merge 49/4 Mathlib/Analysis/InnerProductSpace/Orthonormal.lean,Mathlib/Analysis/InnerProductSpace/PiL2.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean,Mathlib/Combinatorics/SimpleGraph/Diam.lean,Mathlib/Logic/Basic.lean 5 36 ['eric-wieser', 'github-actions', 'leanprover-radar', 'loefflerd', 'themathqueen', 'wwylele'] loefflerd
assignee:loefflerd
2-7083
2 days ago
9-8121
9 days ago
12-54767
12 days
37592 erdOne
author:erdOne
 feat: set up API for `ConvexSpace` We introduce `sConvexCombo` and the indexed version `iConvexCombo` as the main API for `ConvexSpace` and prove lemmas around the new definitions. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebra large-import maintainer-merge awaiting-author
label:t-algebra$
 452/133 Mathlib/Analysis/Convex/MetricSpace.lean,Mathlib/LinearAlgebra/ConvexSpace.lean,Mathlib/LinearAlgebra/ConvexSpace/AffineSpace.lean 3 37 ['YaelDillies', 'erdOne', 'faenuccio', 'github-actions'] faenuccio
assignee:faenuccio
2-2063
2 days ago
7-29690
7 days ago
3-64638
3 days
37678 vihdzp
author:vihdzp
 chore(Dynamics/FixedPoints/Defs): create `Defs` file --- I got a large import warning on another PR for simply importing the definition `Function.fixedPoints`, which I found rather silly. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-dynamics tech debt maintainer-merge 67/44 Mathlib.lean,Mathlib/Dynamics/FixedPoints/Basic.lean,Mathlib/Dynamics/FixedPoints/Defs.lean,Mathlib/Logic/Function/Defs.lean 4 2 ['Ruben-VandeVelde', 'github-actions'] urkud
assignee:urkud
1-24170
1 day ago
8-60858
8 days ago
8-61431
8 days
36965 vihdzp
author:vihdzp
 chore(SetTheory/Cardinal): tweak `succ` lemmas We leave the `SuccOrder` instance unexposed. It doesn't have any particularly good def-eqs, it's simply defined as the infimum of all larger cardinals. We also golf some surrounding theorems. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-set-theory maintainer-merge 54/61 Mathlib/LinearAlgebra/Dimension/Basic.lean,Mathlib/Order/SuccPred/CompleteLinearOrder.lean,Mathlib/SetTheory/Cardinal/Basic.lean,Mathlib/SetTheory/Cardinal/Order.lean,Mathlib/SetTheory/Ordinal/Basic.lean 5 4 ['YaelDillies', 'github-actions', 'mathlib-merge-conflicts'] b-mehta
assignee:b-mehta
1-20220
1 day ago
1-38077
1 day ago
23-32282
23 days
37138 dtumad
author:dtumad
 feat(Data/FinEnum): instances for standard signed and unsigned integer types Adds `FinEnum` instances for `UIntN`/`IntN` for various `N`, and for platform sized integers. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data new-contributor maintainer-merge 45/0 Mathlib/Data/FinEnum.lean 1 11 ['dtumad', 'github-actions', 'joneugster', 'linesthatinterlace'] joneugster
assignee:joneugster
1-18592
1 day ago
14-377
14 days ago
18-36605
18 days
37645 joelriou
author:joelriou
 feat(CategoryTheory/Limits): `sigmaConst` preserves colimits More precisely `sigmaConst.obj R` commutes with colimits. We also compute the cokernel of `(sigmaConst.obj R).map f` when `f` is a map in `Type*`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-category-theory maintainer-merge 144/48 Mathlib.lean,Mathlib/Algebra/Category/ModuleCat/Sheaf/Free.lean,Mathlib/CategoryTheory/Limits/Preserves/SigmaConst.lean 3 7 ['dagurtomas', 'github-actions', 'joelriou', 'robin-carlier'] robin-carlier
assignee:robin-carlier
1-18030
1 day ago
1-18079
1 day ago
9-17298
9 days
30077 agjftucker
author:agjftucker
 feat(Analysis/Calculus/ImplicitFunction): define implicitFunctionOfBivariate Introduce a further specialization of the implicit function theorem; one which applies to a curried bivariate function. --- - [x] depends on: #26985 This is in large part a response to sgouezel's review comment on #16743 > The real question is whether it's best to formulate the result for curried or uncurried function. My bet is that curried would be better since most functions on products in fact come in curried form, but since you've already written fully the uncurried version (and a todo saying that it would be good having the curried version as well), let's keep it like that for now. #26985 reviewed by j-loreaux and later on by winstonyin. #16743 and #26300 reviewed by sgouezel. [Zulip chat](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Inverse.20function.20theorem.20and.20ContinuousLinearEquiv/with/567586606) with Yury Kudryashov. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-analysis maintainer-merge 187/0 Mathlib.lean,Mathlib/Analysis/Calculus/FDeriv/Partial.lean,Mathlib/Analysis/Calculus/ImplicitFunction/Bivariate.lean,Mathlib/Analysis/Calculus/ImplicitFunction/ProdDomain.lean 4 14 ['agjftucker', 'github-actions', 'j-loreaux', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'mathlib4-merge-conflict-bot'] j-loreaux
assignee:j-loreaux
1-4362
1 day ago
1-4423
1 day ago
52-71118
52 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
36216 michaellee94
author:michaellee94
 feat(CategoryTheory): characterize pullback squares via the `Over` category --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-category-theory new-contributor maintainer-merge awaiting-author 47/0 Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean 1 18 ['dagurtomas', 'github-actions', 'joelriou', 'michaellee94'] robin-carlier
assignee:robin-carlier
18-67335
18 days ago
18-67335
18 days ago
2-50782
2 days
37738 khwilson
author:khwilson
 feat(Topology/Order/Bornology): generalize `cobounded_eq` `Real.cobounded_eq` and `Int.cobounded_eq` are used in several places throughout Mathlib. They are currently proved in terms of the Metric topology on `Int` and `Real`, but they're really properties of the order bornology on those objects. Generalize those constructions to `IsOrderBornology` for `LinearOrder`'s and add a few more constructions that are true in other circumstances, e.g., `cobounded NNReal = .atTop` follows from the fact that `NNReal` is both `NoMaxOrder` and `OrderBot`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-order 57/18 Mathlib/Analysis/Polynomial/Basic.lean,Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean,Mathlib/Topology/Instances/Int.lean,Mathlib/Topology/Instances/Real/Lemmas.lean,Mathlib/Topology/Order/Bornology.lean 5 14 ['YaelDillies', 'github-actions', 'khwilson', 'vihdzp'] nobody
6-59051
6 days ago
7-10597
7 days ago
7-11435
7 days
37057 erdOne
author:erdOne
 feat(AlgebraicTopology): `SimplexCategory.toTop_map_δ_apply` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebraic-topology maintainer-merge awaiting-author merge-conflict 48/2 Mathlib/AlgebraicTopology/CechNerve.lean,Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean,Mathlib/AlgebraicTopology/SimplexCategory/Defs.lean,Mathlib/AlgebraicTopology/TopologicalSimplex.lean,Mathlib/Data/Fin/SuccPred.lean 5 17 ['Raph-DG', 'dagurtomas', 'erdOne', 'github-actions', 'joelriou', 'mathlib-merge-conflicts', 'riccardobrasca'] robin-carlier
assignee:robin-carlier
6-34138
6 days ago
7-81778
7 days ago
4-49805
4 days
37544 SnirBroshi
author:SnirBroshi
 chore(Combinatorics/SimpleGraph/Coloring): move `ConcreteColorings.lean` and `EdgeLabeling.lean` to `Coloring/` Moves `SimpleGraph/ConcreteColorings.lean` to `SimpleGraph/Coloring/Constructions.lean` and `SimpleGraph/EdgeLabeling.lean` to `SimpleGraph/Coloring/EdgeLabeling.lean`. See [Zulip](https://leanprover.zulipchat.com/#narrow/channel/252551-graph-theory/topic/Coloring.20module.20names/with/583281500) --- [Zulip](https://leanprover.zulipchat.com/#narrow/channel/252551-graph-theory/topic/Coloring.20module.20names/with/583281500) might want to rename `ConcreteColorings` (Edit: the poll chose `Constructions.lean`) #37546 adds module deprecations [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) file-removed t-combinatorics maintainer-merge 2/2 Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Coloring/Constructions.lean,Mathlib/Combinatorics/SimpleGraph/Coloring/EdgeLabeling.lean 3 2 ['YaelDillies', 'github-actions', 'ooovi'] nobody
6-23367
6 days ago
9-3819
9 days ago
9-3958
9 days
37603 Parcly-Taxel
author:Parcly-Taxel
 refactor: review of `SetSemiring` * Rename `Set.up` and `SetSemiring.down` to `SetSemiring.ofSet` and `SetSemiring.toSet` respectively. Unprotect both and make them equivalences, following `FreeMonoid`. * Derive `CompleteAtomicBooleanAlgebra` for `SetSemiring` immediately. * Add `imageHom_id` and `imageHom_comp`. The three existing lemmas about `imageHom` are coalesced into `imageHom_apply`. Ultimately inspired by https://github.com/leanprover-community/mathlib4/pull/36934#issuecomment-4183475568. maintainer-merge 120/165 Mathlib/Algebra/Algebra/Operations.lean,Mathlib/Data/Set/Semiring.lean 2 41 ['Parcly-Taxel', 'YaelDillies', 'eric-wieser', 'github-actions', 'mathlib-merge-conflicts', 'sgouezel'] nobody
6-4125
6 days ago
6-4383
6 days ago
7-31782
7 days
37291 IvanRenison
author:IvanRenison
 refactor(Combinatorics/SimpleGraph): move `chromaticNumber_le_two_iff_isBipartite` and `chromaticNumber_eq_two_iff` to `Bipartite` file --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-combinatorics maintainer-merge 10/12 Mathlib/Combinatorics/SimpleGraph/Bipartite.lean,Mathlib/Combinatorics/SimpleGraph/ConcreteColorings.lean 2 2 ['Ruben-VandeVelde', 'github-actions'] nobody
4-71709
4 days ago
17-59517
17 days ago
17-59512
17 days
37400 SnirBroshi
author:SnirBroshi
 feat(Combinatorics/SimpleGraph/Acyclic): endpoints of a path have at most one neighbor in the path --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-combinatorics maintainer-merge 15/0 Mathlib/Combinatorics/SimpleGraph/Acyclic.lean 1 4 ['Rida-Hamadani', 'Ruben-VandeVelde', 'github-actions'] nobody
4-70616
4 days ago
14-46512
14 days ago
14-46507
14 days
37420 artie2000
author:artie2000
 refactor: change definitions to avoid `ConvexCone` Change the definitions of `PointedCone.positive` and `PointedCone.closure` to avoid mentioning `ConvexCone`. This PR is part of a series deprecating `ConvexCone`: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Replacing.20.60ConvexCone.60.20with.20.60PointedCone.60/with/582738985 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-convex-geometry maintainer-merge 10/4 Mathlib/Analysis/Convex/Cone/Closure.lean,Mathlib/Geometry/Convex/Cone/Pointed.lean 2 2 ['YaelDillies', 'github-actions', 'ooovi', 'vihdzp'] nobody
4-39530
4 days ago
14-23371
14 days ago
14-23503
14 days
36416 j-loreaux
author:j-loreaux
 feat(Analysis/CStarAlgebra): norms of sums of orthogonal selfadjoint elements --- - [ ] depends on: #36407 - [ ] depends on: #37569 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-analysis maintainer-merge 130/1 Mathlib/Algebra/Star/BigOperators.lean,Mathlib/Algebra/Star/SelfAdjoint.lean,Mathlib/Analysis/CStarAlgebra/Fuglede.lean,Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean 4 22 ['github-actions', 'grunweg', 'j-loreaux', 'loefflerd', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'themathqueen'] loefflerd
assignee:loefflerd
4-28553
4 days ago
4-44128
4 days ago
10-23153
10 days
33443 sahanwijetunga
author:sahanwijetunga
 feat: Define Isometries of Bilinear Spaces --- We define Isometries of Bilinear Spaces, closely following the implementation of isometries of quadratic spaces. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebra new-contributor maintainer-merge
label:t-algebra$
 278/0 Mathlib.lean,Mathlib/LinearAlgebra/BilinearForm/Isometry.lean,Mathlib/LinearAlgebra/BilinearForm/IsometryEquiv.lean 3 25 ['github-actions', 'robin-carlier', 'sahanwijetunga'] mattrobball
assignee:mattrobball
4-28372
4 days ago
4-28531
4 days ago
52-55634
52 days
36401 JovanGerb
author:JovanGerb
 feat(positivity): positivity extension for `a - b` This PR adds support in `positivity` for proving things about subtraction. For example, if the goal is `0 < a - b`, and there is a local hypothesis of type `b < a`, then we close the goal. The motivation is that we want `positivity` to be a flexible tactic. So, when trying to prove `0 < a - b` using a local hypothesis, we should look for the simp normal form of this, which is `b < a`. --- [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Can.20I.20make.20positivity.20work.20for.20this.3F/near/578277240) [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-meta maintainer-merge 63/26 Mathlib/Analysis/Calculus/Taylor.lean,Mathlib/Analysis/Complex/AbelLimit.lean,Mathlib/Analysis/Complex/BorelCaratheodory.lean,Mathlib/Analysis/Complex/Hadamard.lean,Mathlib/Analysis/Convex/BetweenList.lean,Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean,Mathlib/Analysis/SpecificLimits/FloorPow.lean,Mathlib/Geometry/Manifold/Riemannian/PathELength.lean,Mathlib/Tactic/Positivity/Basic.lean,MathlibTest/positivity.lean 10 10 ['JovanGerb', 'github-actions', 'hrmacbeth', 'j-loreaux', 'joneugster', 'leanprover-radar'] joneugster
assignee:joneugster
4-17074
4 days ago
4-20987
4 days ago
21-78285
21 days
37846 grunweg
author:grunweg
 fix(positivity): still prove non-negativity in the `Nat.cast` extension if positivity fails --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-meta maintainer-merge 11/2 Mathlib/Tactic/Positivity/Basic.lean,MathlibTest/positivity.lean 2 4 ['dwrensha', 'github-actions'] dwrensha
assignee:dwrensha
3-50419
3 days ago
4-12639
4 days ago
4-12636
4 days
35906 scp020
author:scp020
 feat(Combinatorics/SimpleGraph/Walk): chords of walks Define `Walk.IsChord` and `Walk.IsChordless` predicates in a new file `SimpleGraph/Walk/Chord.lean`. See "chord" in https://en.wikipedia.org/wiki/Glossary_of_graph_theory --- [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Walk.2EIsChordless.20live.20in.20mathlib.3F/with/575277309) [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-combinatorics new-contributor maintainer-merge 59/0 Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Walk/Chord.lean 2 68 ['SnirBroshi', 'YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'scp020'] YaelDillies
assignee:YaelDillies
3-32100
3 days ago
9-50517
9 days ago
34-40377
34 days
36308 SnirBroshi
author:SnirBroshi
 feat(Combinatorics/SimpleGraph/Subgraph): a couple of `subgraphOfAdj` lemmas Also golf a lemma (it's one line longer but it looks simpler to me). --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-combinatorics maintainer-merge 14/5 Mathlib/Combinatorics/SimpleGraph/Subgraph.lean 1 3 ['YaelDillies', 'github-actions'] nobody
2-29033
2 days ago
38-31885
38 days ago
38-31880
38 days
34854 GrigorenkoPV
author:GrigorenkoPV
 chore(Combinatorics/Enumerative/Catalan): split into `Basic` & `Tree` --- Split off from #34853 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) new-contributor t-combinatorics maintainer-merge 225/194 Mathlib.lean,Mathlib/Combinatorics/Enumerative/Catalan.lean,Mathlib/Combinatorics/Enumerative/Catalan/Basic.lean,Mathlib/Combinatorics/Enumerative/Catalan/Tree.lean,Mathlib/Combinatorics/Enumerative/DyckWord.lean,Mathlib/RingTheory/PowerSeries/Catalan.lean 6 6 ['SnirBroshi', 'YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'vihdzp'] nobody
2-16458
2 days ago
2-16455
2 days ago
45-59230
45 days
37506 wwylele
author:wwylele
 feat(Analysis/InnerProductSpace): singleton basis for 1d space This was brought up in #36462. Similar to existing `FiniteDimensional.basisSingleton`, this provides a OrthonormalBasis version. Also adds simp lemma for `∀ (i j : ι), P i j` for subsingleton `ι`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-analysis maintainer-merge 49/4 Mathlib/Analysis/InnerProductSpace/Orthonormal.lean,Mathlib/Analysis/InnerProductSpace/PiL2.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean,Mathlib/Combinatorics/SimpleGraph/Diam.lean,Mathlib/Logic/Basic.lean 5 36 ['eric-wieser', 'github-actions', 'leanprover-radar', 'loefflerd', 'themathqueen', 'wwylele'] loefflerd
assignee:loefflerd
2-7083
2 days ago
9-8121
9 days ago
12-54767
12 days
37592 erdOne
author:erdOne
 feat: set up API for `ConvexSpace` We introduce `sConvexCombo` and the indexed version `iConvexCombo` as the main API for `ConvexSpace` and prove lemmas around the new definitions. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebra large-import maintainer-merge awaiting-author
label:t-algebra$
 452/133 Mathlib/Analysis/Convex/MetricSpace.lean,Mathlib/LinearAlgebra/ConvexSpace.lean,Mathlib/LinearAlgebra/ConvexSpace/AffineSpace.lean 3 37 ['YaelDillies', 'erdOne', 'faenuccio', 'github-actions'] faenuccio
assignee:faenuccio
2-2063
2 days ago
7-29690
7 days ago
3-64638
3 days
37678 vihdzp
author:vihdzp
 chore(Dynamics/FixedPoints/Defs): create `Defs` file --- I got a large import warning on another PR for simply importing the definition `Function.fixedPoints`, which I found rather silly. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-dynamics tech debt maintainer-merge 67/44 Mathlib.lean,Mathlib/Dynamics/FixedPoints/Basic.lean,Mathlib/Dynamics/FixedPoints/Defs.lean,Mathlib/Logic/Function/Defs.lean 4 2 ['Ruben-VandeVelde', 'github-actions'] urkud
assignee:urkud
1-24170
1 day ago
8-60858
8 days ago
8-61431
8 days
36965 vihdzp
author:vihdzp
 chore(SetTheory/Cardinal): tweak `succ` lemmas We leave the `SuccOrder` instance unexposed. It doesn't have any particularly good def-eqs, it's simply defined as the infimum of all larger cardinals. We also golf some surrounding theorems. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-set-theory maintainer-merge 54/61 Mathlib/LinearAlgebra/Dimension/Basic.lean,Mathlib/Order/SuccPred/CompleteLinearOrder.lean,Mathlib/SetTheory/Cardinal/Basic.lean,Mathlib/SetTheory/Cardinal/Order.lean,Mathlib/SetTheory/Ordinal/Basic.lean 5 4 ['YaelDillies', 'github-actions', 'mathlib-merge-conflicts'] b-mehta
assignee:b-mehta
1-20220
1 day ago
1-38077
1 day ago
23-32282
23 days
37138 dtumad
author:dtumad
 feat(Data/FinEnum): instances for standard signed and unsigned integer types Adds `FinEnum` instances for `UIntN`/`IntN` for various `N`, and for platform sized integers. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data new-contributor maintainer-merge 45/0 Mathlib/Data/FinEnum.lean 1 11 ['dtumad', 'github-actions', 'joneugster', 'linesthatinterlace'] joneugster
assignee:joneugster
1-18592
1 day ago
14-377
14 days ago
18-36605
18 days
37645 joelriou
author:joelriou
 feat(CategoryTheory/Limits): `sigmaConst` preserves colimits More precisely `sigmaConst.obj R` commutes with colimits. We also compute the cokernel of `(sigmaConst.obj R).map f` when `f` is a map in `Type*`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-category-theory maintainer-merge 144/48 Mathlib.lean,Mathlib/Algebra/Category/ModuleCat/Sheaf/Free.lean,Mathlib/CategoryTheory/Limits/Preserves/SigmaConst.lean 3 7 ['dagurtomas', 'github-actions', 'joelriou', 'robin-carlier'] robin-carlier
assignee:robin-carlier
1-18030
1 day ago
1-18079
1 day ago
9-17298
9 days
30077 agjftucker
author:agjftucker
 feat(Analysis/Calculus/ImplicitFunction): define implicitFunctionOfBivariate Introduce a further specialization of the implicit function theorem; one which applies to a curried bivariate function. --- - [x] depends on: #26985 This is in large part a response to sgouezel's review comment on #16743 > The real question is whether it's best to formulate the result for curried or uncurried function. My bet is that curried would be better since most functions on products in fact come in curried form, but since you've already written fully the uncurried version (and a todo saying that it would be good having the curried version as well), let's keep it like that for now. #26985 reviewed by j-loreaux and later on by winstonyin. #16743 and #26300 reviewed by sgouezel. [Zulip chat](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Inverse.20function.20theorem.20and.20ContinuousLinearEquiv/with/567586606) with Yury Kudryashov. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-analysis maintainer-merge 187/0 Mathlib.lean,Mathlib/Analysis/Calculus/FDeriv/Partial.lean,Mathlib/Analysis/Calculus/ImplicitFunction/Bivariate.lean,Mathlib/Analysis/Calculus/ImplicitFunction/ProdDomain.lean 4 14 ['agjftucker', 'github-actions', 'j-loreaux', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'mathlib4-merge-conflict-bot'] j-loreaux
assignee:j-loreaux
1-4362
1 day ago
1-4423
1 day ago
52-71118
52 days
33935 mckoen
author:mckoen
 feat(CategoryTheory/Monoidal/Arrow): define monoidal structure on arrow category defines a monoidal category structure on the arrow category of a cartesian closed category. --- - [x] depends on: #33974 - [x] depends on: #34887 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-category-theory maintainer-merge 659/0 Mathlib.lean,Mathlib/CategoryTheory/Monoidal/Arrow.lean,Mathlib/CategoryTheory/Monoidal/Closed/Braided.lean,Mathlib/CategoryTheory/Monoidal/Limits/HasLimits.lean,Mathlib/CategoryTheory/Monoidal/Limits/Shapes/Pullback.lean,Mathlib/CategoryTheory/Monoidal/PushoutProduct.lean 6 42 ['dagurtomas', 'github-actions', 'joelriou', 'mathlib-dependent-issues', 'mckoen'] joelriou
assignee:joelriou
0-68769
19 hours ago
0-68824
19 hours ago
34-24804
34 days
37874 yuanyi-350
author:yuanyi-350
 refactor(Analysis/PSeries): simplify `Real.summable_one_div_nat_add_rpow` via asymptotics ## Summary - replace the manual eventual-positivity and limit argument in `Real.summable_one_div_nat_add_rpow` with an asymptotic-equivalence proof - use `IsEquivalent.add_const_of_norm_tendsto_atTop` together with `Asymptotics.IsEquivalent.summable_iff_nat` - add the imports needed for the asymptotics-based proof This also removes the local `set_option linter.unusedSimpArgs false` workaround from the proof. t-analysis large-import maintainer-merge awaiting-author 14/26 Mathlib/Analysis/PSeries.lean,Mathlib/NumberTheory/LSeries/Nonvanishing.lean 2 11 ['YaelDillies', 'github-actions', 'grunweg', 'leanprover-radar', 'yuanyi-350'] ADedecker
assignee:ADedecker
0-55963
15 hours ago
0-80814
22 hours ago
3-40896
3 days
36958 JovanGerb
author:JovanGerb
 chore(Topology/Order/Basic): use `Preorder.topology` in `OrderTopology` This PR addresses the comment: ``` TODO: define `Preorder.topology` before `OrderTopology` and reuse the def ``` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-topology maintainer-merge 22/19 Mathlib/Topology/Instances/Discrete.lean,Mathlib/Topology/Order/Basic.lean 2 4 ['JovanGerb', 'github-actions', 'vihdzp'] nobody
0-52681
14 hours ago
23-44818
23 days ago
23-45148
23 days
34649 peabrainiac
author:peabrainiac
 feat(Analysis/Calculus/ContDiff): add notation `ℕ∞ω` for `WithTop ℕ∞` Add a `ContDiff`-scoped notation `ℕ∞ω` for `WithTop ℕ∞`, accompanying the existing notations `∞` and `ω` for `(⊤ : ℕ∞) : ℕ∞ω` and `⊤ : ℕ∞ω`. --- [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/RFC.3A.20notation.20for.20.60WithTop.20.E2.84.95.E2.88.9E.60/near/573917824) I've also replaced `WithTop ℕ∞` with this new notation already in the files that mention it the most, but not in all files yet; many mention `WithTop ℕ∞` just a couple of times but don't open the `ContDiff` namespace. I'm not sure whether that should be taken as a sign to not make the notation scoped, or whether the solution is just to `open scoped ContDiff` in these files or not use the notation there. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-differential-geometry t-analysis maintainer-merge 276/272 Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean,Mathlib/Analysis/Calculus/ContDiff/Basic.lean,Mathlib/Analysis/Calculus/ContDiff/Bounds.lean,Mathlib/Analysis/Calculus/ContDiff/CPolynomial.lean,Mathlib/Analysis/Calculus/ContDiff/Comp.lean,Mathlib/Analysis/Calculus/ContDiff/Defs.lean,Mathlib/Analysis/Calculus/ContDiff/Deriv.lean,Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean,Mathlib/Analysis/Calculus/ContDiff/Operations.lean,Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean,Mathlib/Analysis/Calculus/ImplicitContDiff.lean,Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean,Mathlib/Analysis/Calculus/IteratedDeriv/FaaDiBruno.lean,Mathlib/Analysis/Calculus/VectorField.lean,Mathlib/Analysis/Complex/UpperHalfPlane/Manifold.lean,Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean,Mathlib/Analysis/Distribution/TestFunction.lean,Mathlib/Analysis/Fourier/FourierTransformDeriv.lean,Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/InverseDeriv.lean,Mathlib/Geometry/Manifold/Algebra/LeftInvariantDerivation.lean,Mathlib/Geometry/Manifold/Algebra/LieGroup.lean,Mathlib/Geometry/Manifold/Algebra/Monoid.lean,Mathlib/Geometry/Manifold/Algebra/SmoothFunctions.lean,Mathlib/Geometry/Manifold/Algebra/Structures.lean,Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean,Mathlib/Geometry/Manifold/ContMDiff/Basic.lean,Mathlib/Geometry/Manifold/ContMDiff/Defs.lean,Mathlib/Geometry/Manifold/Diffeomorph.lean,Mathlib/Geometry/Manifold/Immersion.lean,Mathlib/Geometry/Manifold/Instances/Real.lean,Mathlib/Geometry/Manifold/Instances/Sphere.lean,Mathlib/Geometry/Manifold/Instances/UnitsOfNormedAlgebra.lean,Mathlib/Geometry/Manifold/IsManifold/Basic.lean,Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean,Mathlib/Geometry/Manifold/Riemannian/Basic.lean,Mathlib/Geometry/Manifold/Riemannian/PathELength.lean,Mathlib/Geometry/Manifold/SmoothEmbedding.lean,Mathlib/Geometry/Manifold/VectorBundle/Basic.lean,Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/Basic.lean,Mathlib/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean,Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean,Mathlib/Geometry/Manifold/VectorBundle/Riemannian.lean,Mathlib/Geometry/Manifold/VectorBundle/SmoothSection.lean,Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean,Mathlib/Geometry/Manifold/VectorField/LieBracket.lean,Mathlib/Geometry/Manifold/VectorField/Pullback.lean 47 12 ['JovanGerb', 'github-actions', 'j-loreaux', 'mathlib-merge-conflicts', 'peabrainiac'] sgouezel
assignee:sgouezel
0-44666
12 hours ago
0-44691
12 hours ago
12-21147
12 days
31425 robertmaxton42
author:robertmaxton42
 feat(Topology): implement delaborators for non-standard topology notation Add delaborators for unary and binary notation related to non-standard topologies in the TopologicalSpace namespace. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-topology maintainer-merge 265/5 Mathlib.lean,Mathlib/Topology/Defs/Basic.lean,Mathlib/Util/DelabNonCanonical.lean,MathlibTest/Delab/TopologicalSpace.lean 4 52 ['eric-wieser', 'github-actions', 'j-loreaux', 'jcommelin', 'kckennylau', 'robertmaxton42'] alreadydone
assignee:alreadydone
0-38960
10 hours ago
0-39020
10 hours ago
124-36377
124 days
37347 JovanGerb
author:JovanGerb
 feat: implementation of `@[use_set_notation_for_order]` This PR allows the use of `⊆` notation while the underlying constant is `≤`. Similarly for `⊂`/`<`, `⊇`/`≥` and `⊃`/`>`. - The idea is to later extend this feature to other set notation constants, such as union/intersection. - There are some types for which we cannot use `LE.le` as the underlying constant, such as `List` and `Multiset`. So, the elaborator for the `⊆` notation needs to make a decision which underlying constant to elaborate to, depending on the type. Sometimes the type is not known yet, which makes things awkward. Most of these cases are solved by delaying the elaboration until later when the type is known. - However, in some cases this doesn't work either, such as `simp_rw [and_comm (_ ⊆ _)]`, where it is impossible to tell the type when elaborating the term. So, some such cases need to be fixed by making it `simp_rw [and_comm (_ ≤ _)]`. This is because `simp_rw`, unlike `rw`, fully elaborates the rewrite rules before using them. So, when we get the new rewrite tactic, this problem will mostly go away. See also https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Any.20infimum.20based.20version.20of.20.60OmegaCompletePartialOrder.60.3F/near/579333629 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-meta maintainer-merge 345/0 Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/SetNotationForOrder.lean,MathlibTest/SetNotationForOrder.lean 4 44 ['JovanGerb', 'github-actions', 'thorimur'] alexjbest and thorimur
assignee:alexjbest assignee:thorimur
0-24673
6 hours ago
1-58085
1 day ago
14-85567
14 days
37972 vihdzp
author:vihdzp
 chore: deprecate various theorems about `Ordinal.ToType` We should generally be writing theorems about "well-orders of order type `o`", rather than theorems about `o.ToType` (which is just one such well-order, defined via choice). --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-set-theory maintainer-merge 31/18 Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean,Mathlib/CategoryTheory/Presentable/OrthogonalReflection.lean,Mathlib/FieldTheory/CardinalEmb.lean,Mathlib/SetTheory/Cardinal/Order.lean,Mathlib/SetTheory/Ordinal/Arithmetic.lean,Mathlib/SetTheory/Ordinal/Basic.lean 6 2 ['YaelDillies', 'github-actions'] nobody
0-20636
5 hours ago
1-39016
1 day ago
1-41957
1 day
35879 Jun2M
author:Jun2M
 feat(Combinatorics/Graph): graph deletion operations This PR adds definitions and basic lemmas for deleting edges and vertices from a graph in Mathlib/Combinatorics/Graph/Delete.lean. It introduces the following operations: - `restrict`: the subgraph of `G` restricted to the edges in `F` without removing vertices - `deleteEdges`: the subgraph of `G` with the edges in `F` deleted - `induce`: the subgraph of `G` induced by the set `X` of vertices - `deleteVerts` : the graph obtained from `G` by deleting the set `X` of vertices These definitions are accompanied by simp lemmas describing their edge sets, incidence relations, and basic properties such as monotonicity. Co-authored-by: Peter Nelson [apn.uni@gmail.com](mailto:apn.uni@gmail.com) --- - [x] depends on: #26770 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-combinatorics maintainer-merge 207/7 Mathlib.lean,Mathlib/Combinatorics/Graph/Basic.lean,Mathlib/Combinatorics/Graph/Delete.lean 3 31 ['Jun2M', 'YaelDillies', 'b-mehta', 'github-actions', 'mathlib-dependent-issues', 'mathlib-merge-conflicts'] nobody
0-20035
5 hours ago
3-74028
3 days ago
23-7527
23 days
37540 quantumsnow
author:quantumsnow
 feat(CategoryTheory/MorphismProperty/Comma): add MorphismProperty.Arrow This is needed for the category of topological pairs (#36621). --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-category-theory new-contributor maintainer-merge 109/8 Mathlib/CategoryTheory/MorphismProperty/Comma.lean 1 20 ['chrisflav', 'github-actions', 'joelriou', 'quantumsnow'] nobody
0-14504
4 hours ago
0-18857
5 hours ago
0-26261
7 hours
37053 artie2000
author:artie2000
 refactor(Analysis/Convex/Cone): use `PointedCone` in Riesz extension theorem Change the statement of the Riesz extension theorem to take a `PointedCone` rather than a `ConvexCone`. This PR is part of a series replacing `ConvexCone` with `PointedCone`. https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Replacing.20.60ConvexCone.60.20with.20.60PointedCone.60/near/581184307 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-convex-geometry maintainer-merge 15/12 Mathlib/Analysis/Convex/Cone/Extension.lean,Mathlib/Geometry/Convex/Cone/Pointed.lean 2 8 ['YaelDillies', 'artie2000', 'github-actions', 'mathlib-merge-conflicts', 'ocfnash'] nobody
0-7680
2 hours ago
0-7708
2 hours ago
19-49140
19 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
17623 astrainfinita
author:astrainfinita
 feat(Algebra/Order/GroupWithZero/Unbundled): add some lemmas Some lemmas in `Algebra.Order.GroupWithZero.Unbundled` have incorrect or unsatisfactory names, or assumptions that can be omitted using `ZeroLEOneClass`. The lemmas added in this PR are versions of existing lemmas that use the correct or better name or `ZeroLEOneClass` to omit an assumption. The original lemmas will be deprecated in #17593. | New name | Old name | |-------------------------|-------------------------| | `mul_le_one_left₀` | `Left.mul_le_one_of_le_of_le` | | `mul_lt_one_of_le_of_lt_left₀` (`0 ≤ ·` version) / `mul_lt_one_of_le_of_lt_of_pos_left` | `Left.mul_lt_of_le_of_lt_one_of_pos` | | `mul_lt_one_of_lt_of_le_left₀` | `Left.mul_lt_of_lt_of_le_one_of_nonneg` | | `mul_le_one_right₀` | `Right.mul_le_one_of_le_of_le` | | `mul_lt_one_of_lt_of_le_right₀` (`0 ≤ ·` version) / `mul_lt_one_of_lt_of_le_of_pos_right` | `Right.mul_lt_one_of_lt_of_le_of_pos` | | `mul_lt_one_of_le_of_lt_right₀` | `Right.mul_lt_one_of_le_of_lt_of_nonneg` | The following lemmas use `ZeroLEOneClass`. | New name | Old name | |-------------------------|-------------------------| | `(Left.)one_le_mul₀` | `Left.one_le_mul_of_le_of_le` | | `Left.one_lt_mul_of_le_of_lt₀` | `Left.one_lt_mul_of_le_of_lt_of_pos` | | `Left.one_lt_mul_of_lt_of_le₀` | `Left.lt_mul_of_lt_of_one_le_of_nonneg` / `one_lt_mul_of_lt_of_le` (still there) | | `(Left.)one_lt_mul₀` | | | `Right.one_le_mul₀` | `Right.one_le_mul_of_le_of_le` | | `Right.one_lt_mul_of_lt_of_le₀` | `Right.one_lt_mul_of_lt_of_le_of_pos` | | `Right.one_lt_mul_of_le_of_lt₀` | `Right.one_lt_mul_of_le_of_lt_of_nonneg` / `one_lt_mul_of_le_of_lt` (still there) / `one_lt_mul` (still there) | | `Right.one_lt_mul₀` | `Right.one_lt_mul_of_lt_of_lt` | --- Split from #17593. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) merge-conflict t-algebra awaiting-zulip t-order
label:t-algebra$
 146/44 Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean 2 11 ['YaelDillies', 'astrainfinita', 'github-actions', 'j-loreaux'] nobody
510-12070
1 year ago
517-4629
517 days ago
33-53295
33 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/) blocked-by-other-PR new-contributor t-computability merge-conflict awaiting-zulip 985/2 Mathlib.lean,Mathlib/Computability/GNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean,Mathlib/Computability/RegularExpressions.lean,Mathlib/Data/FinEnum/Option.lean,docs/references.bib 7 3 ['github-actions', 'leanprover-community-mathlib4-bot', 'meithecatte'] nobody
343-61747
11 months ago
612-84932
612 days ago
0-179
2 minutes
17458 urkud
author:urkud
 refactor(Algebra/Group): make `IsUnit` a typeclass Also change some lemmas to assume `[IsUnit _]` instead of `[Invertible _]`. Motivated by potential non-defeq diamonds in #14986, see also [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Invertible.20and.20data) I no longer plan to merge this PR, but I'm going to cherry-pick some changes to a new PR before closing this one. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) merge-conflict t-algebra awaiting-zulip
label:t-algebra$
 82/72 Mathlib/Algebra/CharP/Invertible.lean,Mathlib/Algebra/Group/Invertible/Basic.lean,Mathlib/Algebra/Group/Units/Defs.lean,Mathlib/Algebra/GroupWithZero/Invertible.lean,Mathlib/Algebra/GroupWithZero/Units/Basic.lean,Mathlib/Algebra/Polynomial/Degree/Units.lean,Mathlib/Algebra/Polynomial/Splits.lean,Mathlib/Analysis/Convex/Segment.lean,Mathlib/Analysis/Normed/Affine/Isometry.lean,Mathlib/Analysis/Normed/Ring/Units.lean,Mathlib/CategoryTheory/Linear/Basic.lean,Mathlib/FieldTheory/Finite/Basic.lean,Mathlib/FieldTheory/Separable.lean,Mathlib/FieldTheory/SeparableDegree.lean,Mathlib/GroupTheory/Submonoid/Inverses.lean,Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean,Mathlib/LinearAlgebra/AffineSpace/Combination.lean,Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean,Mathlib/LinearAlgebra/CliffordAlgebra/Inversion.lean,Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean,Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean,Mathlib/NumberTheory/MulChar/Basic.lean,Mathlib/RingTheory/Localization/NumDen.lean,Mathlib/RingTheory/Polynomial/Content.lean,Mathlib/RingTheory/Polynomial/GaussLemma.lean,Mathlib/RingTheory/Valuation/Basic.lean 26 12 ['MichaelStollBayreuth', 'acmepjz', 'eric-wieser', 'github-actions', 'leanprover-bot', 'leanprover-community-bot-assistant', 'urkud'] nobody
283-42096
9 months ago
554-76139
554 days 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/) merge-conflict t-algebraic-geometry awaiting-zulip new-contributor 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
283-40934
9 months ago
316-16051
316 days ago
6-44784
6 days
28803 astrainfinita
author:astrainfinita
 refactor: unbundle algebra from `ENormed*` Further speed up the search in the algebraic typeclass hierarchy by avoiding searching for `TopologicalSpace`. This PR continues the work from #23961. - Change `ESeminormed(Add)Monoid` and `ENormed(Add)Monoid` so they no longer carry algebraic data. - Deprecate `ESeminormed(Add)CommMonoid` and `ENormed(Add)CommMonoid` in favor of `ESeminormed(Add)Monoid` and `ENormed(Add)Monoid` with a commutative algebraic typeclass. |Old|New| |---|---| | `[ESeminormed(Add)(Comm)Monoid E]` | `[(Add)(Comm)Monoid E] [ESeminormed(Add)Monoid E]` | | `[ENormed(Add)(Comm)Monoid]` | `[(Add)(Comm)Monoid E] [ENormed(Add)Monoid]` | See [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2328803.20refactor.3A.20unbundle.20algebra.20from.20.60ENormed*.60/with/536024350) ------------ - [x] depends on: #28813 t-algebra merge-conflict slow-typeclass-synthesis awaiting-zulip t-analysis
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
223-56579
7 months ago
232-7733
232 days ago
0-19882
5 hours
28925 grunweg
author:grunweg
 chore: remove `linear_combination'` tactic When `linear_combination` was refactored in #15899, the old code was kept as the `linear_combination'` tactic, for easier migration. The consensus of the zulip discussion ([#mathlib4 > Narrowing the scope of `linear_combination` @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Narrowing.20the.20scope.20of.20.60linear_combination.60/near/470237816)) was to wait, and "revisit this once people have experienced the various tactics in practice". One year later, the old tactic has almost no uses: it is unused in mathlib; [searching on github](https://github.com/search?q=linear_combination%27%20path%3A*.lean&type=code) yields 37 hits --- all of which are in various forks of mathlib. Thus, removing this tactic seems appropriate. --- Do not merge before the zulip discussion has concluded! [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) merge-conflict 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 4 ['euprunin', 'github-actions', 'grunweg', 'mathlib4-merge-conflict-bot'] nobody
180-33789
5 months ago
231-65586
231 days ago
0-1
1 second
30150 imbrem
author:imbrem
 feat(CategoryTheory/Monoidal): to_additive for MonoidalCategory Add `AddMonoidalCategory`, the additive version of `MonoidalCategory`. To get this to work, I needed to _remove_ the `to_additive` attributes in `Discrete.lean`, since existing code relies on the `AddMonoid M → MonoidalCategory M` instance. For now, we simply implement the additive variants by hand instead. --- As discussed in #28718; I added an `AddMonoidalCategory` struct and tagged `MonoidalCategory` with `to_additive`, along with the lemmas in `Category.lean`. I think this is the right approach, since under this framework the "correct" additive version of `Discrete.lean` would be mapping an `AddMonoid` to an `AddMonoidalCategory`. Next steps would be to: - Make `monoidal_coherence` and `coherence` support `AddMonoidalCategory` - Add `CocartesianMonoidalCategory` extending `AddMonoidalCategory` [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-category-theory large-import new-contributor merge-conflict awaiting-zulip t-meta 444/125 Mathlib/CategoryTheory/Monoidal/Category.lean,Mathlib/CategoryTheory/Monoidal/Discrete.lean,Mathlib/Tactic/ToAdditive/GuessName.lean 3 22 ['JovanGerb', 'YaelDillies', 'github-actions', 'imbrem', 'mathlib4-merge-conflict-bot'] nobody
152-44663
5 months ago
192-23329
192 days ago
1-160
1 day
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/) new-contributor t-computability merge-conflict awaiting-author awaiting-zulip 307/5 Mathlib/Computability/NFA.lean 1 27 ['TpmKranz', 'YaelDillies', 'dupuisf', 'github-actions', 'leanprover-community-bot-assistant', 'meithecatte', 'rudynicolop'] nobody
147-61795
4 months ago
567-2783
567 days ago
45-84611
45 days
15649 TpmKranz
author:TpmKranz
 feat(Computability): introduce Generalised NFA as bridge to Regular Expression Lays the groundwork for a proof of equivalence of NFA and RE, w.r.t. described language. Actual connection to NFA comes later, after the groundwork for the opposite direction has been laid. Second chunk of #12648 --- - [x] depends on: #15647 [Data.FinEnum.Option unchanged since then] [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) new-contributor t-computability merge-conflict awaiting-author awaiting-zulip 298/0 Mathlib.lean,Mathlib/Computability/GNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/RegularExpressions.lean,docs/references.bib 5 7 ['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'meithecatte', 'trivial1711'] nobody
146-78036
4 months ago
492-41566
492 days 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/) merge-conflict t-computability awaiting-zulip new-contributor 490/0 Mathlib.lean,Mathlib/Computability/RegularExpressionsToEpsilonNFA.lean,docs/references.bib 3 7 ['anthonyde', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'meithecatte', 'qawbecrdtey'] nobody
146-28804
4 months ago
343-61733
343 days ago
75-77754
75 days
11800 JADekker
author:JADekker
 feat: KappaLindelöf spaces Define KappaLindelöf spaces by following the first one-third of the API for Lindelöf spaces. The remainder will be added in a future PR. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) please-adopt merge-conflict t-topology awaiting-zulip 301/2 Mathlib.lean,Mathlib/Topology/Compactness/KappaLindelof.lean,Mathlib/Topology/Compactness/Lindelof.lean 3 38 ['ADedecker', 'JADekker', 'PatrickMassot', 'StevenClontz', 'adomani', 'github-actions', 'grunweg', 'kim-em', 'urkud'] nobody
146-670
4 months ago
621-20952
621 days ago
123-25636
123 days
30668 astrainfinita
author:astrainfinita
 feat: `QuotType` This typeclass is primarily for use by type synonyms of `Quot` and `Quotient`. Using `QuotType` API for type synonyms of `Quot` and `Quotient` will avoid defeq abuse caused by directly using `Quot` and `Quotient` APIs. This PR also adds some typeclasses to support different ways to find the quotient map that should be used. See the documentation comments of these typeclasses for examples of usage. --- It's not a typical design to use these auxiliary typeclasses and term elaborators, but I haven't found a better way to support these notations. Some of the naming may need to be discussed. For example: - `⟦·⟧` is currently called `mkQ` in names. This distinguishes it from other `.mk`s and makes it possible to write the quotient map as `mkQ` `mkQ'` ~~`mkQ_ h`~~. But this will also require changing the old lemma names. - It would be helpful if the names of new type classes explained their functionality better. [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/migrate.20to.20.60QuotLike.60.20API) This PR continues the work from #16421. Original PR: https://github.com/leanprover-community/mathlib4/pull/16421 RFC t-data awaiting-zulip 629/0 Mathlib.lean,Mathlib/Data/QuotType.lean,MathlibTest/QuotType.lean 3 20 ['YaelDillies', 'astrainfinita', 'github-actions', 'mathlib4-merge-conflict-bot', 'plp127', 'vihdzp'] nobody
124-68916
4 months ago
177-37769
177 days ago
0-81
1 minute
33368 urkud
author:urkud
 feat: define `Complex.UnitDisc.shift` Also review the existing API UPD: I'm going to define a `PSL(2, Real)` action instead. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-analysis awaiting-zulip merge-conflict 273/39 Mathlib.lean,Mathlib/Analysis/Complex/UnitDisc/Basic.lean,Mathlib/Analysis/Complex/UnitDisc/Shift.lean 3 7 ['github-actions', 'j-loreaux', 'mathlib4-merge-conflict-bot', 'sgouezel', 'urkud'] j-loreaux
assignee:j-loreaux
97-37229
3 months ago
97-83962
97 days ago
7-33574
7 days
32828 Hagb
author:Hagb
 feat(Algebra/Order/Group/Defs): add `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid'` It is similar to `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid`, while with different hypotheses. The conclusion `IsOrderedCancelMonoid α` on `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` still holds when the hypothesis `CommGroup α` is weakened to `CancelCommMonoid α` while `PartialOrder α` is strengthened to `LinearOrder α`. --- [`IsOrderedAddMonoid.toIsOrderedCancelAddMonoid`](https://leanprover-community.github.io/mathlib4_docs/find/?pattern=IsOrderedAddMonoid.toIsOrderedCancelAddMonoid#doc) and `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid'`: https://github.com/leanprover-community/mathlib4/blob/97f78b1a4311fed1844b94f1c069219a48a098e1/Mathlib/Algebra/Order/Group/Defs.lean#L52-L62 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-algebra
label:t-algebra$
 4/0 Mathlib/Algebra/Order/Group/Defs.lean 1 8 ['Garmelon', 'Vierkantor', 'artie2000', 'github-actions', 'leanprover-radar'] eric-wieser
assignee:eric-wieser
81-86064
2 months ago
81-86064
81 days ago
40-42357
40 days
33031 chiyunhsu
author:chiyunhsu
 feat(Combinatorics/Enumerative/Partition): add combinatorial proof of Euler's partition theorem The new file EulerComb.lean contains the combinatorial proof of Euler's partition theorem. The analytic proof of the theorem and its generalization of Glaisher's Theorem has already been formalized in [Glaisher.lean](https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Combinatorics/Enumerative/Partition/Glaisher.lean). The generalization of the combinatorial proof from this file to Glaisher's Theorem is within reach. --- Zulip discussion: [#mathlib4 > Glaisher’s Bijection on integer partitions](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Glaisher.E2.80.99s.20Bijection.20on.20integer.20partitions/with/570808111) [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-combinatorics new-contributor awaiting-zulip 531/0 Mathlib.lean,Mathlib/Combinatorics/Enumerative/Partition/EulerComb.lean 2 5 ['chiyunhsu', 'github-actions', 'tb65536', 'vihdzp'] b-mehta
assignee:b-mehta
75-4482
2 months ago
75-4482
75 days ago
42-22427
42 days
32742 LTolDe
author:LTolDe
 feat(MeasureTheory/Constructions/Polish/Basic): add class SuslinSpace add new class `SuslinSpace` for a topological space that is an analytic set in itself This will be useful to prove the **Effros Theorem**, see [zulip thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Effros.20Theorem/with/558712441). --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) new-contributor awaiting-zulip t-measure-probability 4/0 Mathlib/MeasureTheory/Constructions/Polish/Basic.lean 1 9 ['ADedecker', 'LTolDe', 'dupuisf', 'github-actions', 'jcommelin'] PatrickMassot
assignee:PatrickMassot
72-16892
2 months ago
98-1024
98 days ago
11-7507
11 days
34720 Paul-Lez
author:Paul-Lez
 feat(RingTheory/PowerSeries/Composition): define composition of power series This PR defines the composition of two power series, and adds various pieces of API lemmas (this is mostly fixing up and upstreaming code from [this repo](https://github.com/rmhi/formal_deriv)). This is the first of a series of PRs upstreaming work that was done at the CFT workshop in Oxford last summer, working towards proving some results about the `exp` and `log` power series (and their composition!), and constructing the isomorphism $(\mathfrak{m}_K ^ n, +) \cong (1 + \mathfrak{m}_K ^ n, \times)$ for sufficiently large $n$, where $K$ is a characteristic zero local field. Co-authored-by: Richard Hill Co-authored-by: Calle Sönne --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-ring-theory awaiting-zulip 844/0 Mathlib.lean,Mathlib/RingTheory/PowerSeries/Composition.lean 2 3 ['Paul-Lez', 'github-actions', 'vihdzp'] nobody
63-62901
2 months ago
71-14821
71 days ago
0-10
10 seconds
33441 dupuisf
author:dupuisf
 feat: add `LawfulInv` class for types with an inverse that behaves like `Ring.inverse` This PR introduces a new typeclass `LawfulInv` for types which have an `Inv` instance that is equal to zero on non-invertible elements. This is meant to replace `Ring.inverse`. The current plan is to do this refactor in several steps: 1. This PR, which only introduces the class and adds instances for matrices and continuous linear maps. 2. Add instances for all C*-algebras, and make `CStarAlgebra` extend this. 3. Deprecate `Ring.inverse`. --- [![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$
 185/27 Mathlib/Algebra/GroupWithZero/Defs.lean,Mathlib/Algebra/GroupWithZero/Invertible.lean,Mathlib/Algebra/GroupWithZero/Units/Basic.lean,Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean,Mathlib/LinearAlgebra/Matrix/PosDef.lean,Mathlib/RingTheory/DividedPowers/Padic.lean,Mathlib/Topology/Algebra/Module/Equiv.lean 7 35 ['dupuisf', 'eric-wieser', 'github-actions', 'j-loreaux', 'mathlib-merge-conflicts', 'mathlib4-merge-conflict-bot', 'plp127'] nobody
55-35240
1 month ago
83-68375
83 days ago
7-54141
7 days
26299 adomani
author:adomani
 perf: the `whitespace` linter only acts on modified files Introduces an `IO.Ref` to allow the `commandStart` linter to only run on files that git considers modified with respect to `master`. The linter is also active on files that have had some error, as these are likely being modified! The PR should also mitigate the speed-up that the linter introduced: [#mathlib4 > A whitespace linter @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/A.20whitespace.20linter/near/525091877) Assuming that this goes well, a similar mechanism could be applied to several linters that do not need to run on all code, just on the modified code. Implementation detail: the linter is currently either on or off in "whole" files. It may be also a future development to make this more granular and only run the linter on "modifed commands in modified files", but this is not currently the plan for this modification! --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-linter awaiting-zulip awaiting-author 55/7 Mathlib/Tactic/Linter/Whitespace.lean 1 19 ['adomani', 'eric-wieser', 'github-actions', 'grunweg', 'joneugster', 'kim-em', 'leanprover-bot', 'leanprover-radar', 'mathlib-bors', 'mathlib4-merge-conflict-bot'] grunweg
assignee:grunweg
55-27666
1 month ago
228-23984
228 days ago
66-73556
66 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/) new-contributor t-computability merge-conflict awaiting-author awaiting-zulip 159/0 Mathlib/Computability/DFA.lean,Mathlib/Computability/Language.lean 2 60 ['EtienneC30', 'YaelDillies', 'github-actions', 'maemre', 'mathlib4-merge-conflict-bot', 'meithecatte', 'urkud'] nobody
47-22038
1 month ago
392-86377
392 days ago
48-67492
48 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/) new-contributor t-computability merge-conflict awaiting-author awaiting-zulip 218/2 Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean 2 91 ['EtienneC30', 'b-mehta', 'ctchou', 'github-actions', 'leanprover-community-bot-assistant', 'meithecatte', 'rudynicolop'] nobody
47-22022
1 month ago
344-3916
344 days ago
39-61332
39 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/) t-computability awaiting-zulip new-contributor awaiting-author 101/10 Mathlib/Computability/EpsilonNFA.lean,Mathlib/Computability/NFA.lean 2 42 ['YaelDillies', 'dagurtomas', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'meithecatte'] nobody
46-42051
1 month ago
310-71350
310 days ago
34-10092
34 days
34245 staroperator
author:staroperator
 feat(Data/Set): add `Set.Uncountable` There are `Set` specialized shortcuts `Set.Finite`, `Set.Infinite` and `Set.Countable`, but lacking `Set.Uncountable`. I find this useful in #34246. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data awaiting-zulip 82/4 Mathlib/Analysis/Real/Cardinality.lean,Mathlib/Data/Set/Countable.lean,Mathlib/SetTheory/Cardinal/Basic.lean 3 17 ['github-actions', 'joneugster', 'staroperator', 'vihdzp'] joneugster
assignee:joneugster
39-20265
1 month ago
69-79912
69 days ago
12-21154
12 days
35524 grunweg
author:grunweg
 feat: text-based linter against \t followed by tactic mode Wait for the zulip discussion to converge. **If** there is consensus in favour of this change, summarise the motivation here. [zulip discuss](https://leanprover.zulipchat.com/#narrow/channel/345428-mathlib-reviewers/topic/proposal.3A.20no.20more.20use.20of.20.60.E2.96.B8.60.20in.20Mathlib.3F/with/574680826) --- There are currently 80 remaining exceptions in mathlib: ideally, these would get fixed before merging this. Works best when combined with #35523. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-linter awaiting-zulip merge-conflict 23/2 Mathlib/Tactic/Linter/TextBased.lean 1 5 ['github-actions', 'grunweg', 'joneugster', 'mathlib-merge-conflicts', 'vihdzp'] nobody
27-59803
27 days ago
54-20965
54 days ago
0-187
3 minutes
32608 PrParadoxy
author:PrParadoxy
 feat(LinearAlgebra/PiTensorProduct): API for PiTensorProducts indexed by sets This PR addresses a TODO item in LinearAlgebra/PiTensorProduct.lean: * API for the various ways ι can be split into subsets; connect this with the binary tensor product -- specifically by describing tensors of type ⨂ (i : S), M i, for S : Set ι. Our primary motivation is to formalise the notion of "restricted tensor products". This will be the content of a follow-up PR. Beyond that, the Set API is natural in contexts where the index type has an independent interpretation. An example is quantum physics, where ι ranges over distinguishable degrees of freedom, and where its is common practice to annotate objects by the set of indices they are defined on. --- Stub file with preliminary definition of the restricted tensor product as a direct limit of tensors indexed by finite subsets of an index type: https://github.com/PrParadoxy/mathlib4/blob/restricted-stub/Mathlib/LinearAlgebra/PiTensorProduct/Restricted.lean --- - [x] depends on: #32598 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) new-contributor awaiting-zulip t-algebra
label:t-algebra$
 300/2 Mathlib.lean,Mathlib/LinearAlgebra/PiTensorProduct.lean,Mathlib/LinearAlgebra/PiTensorProduct/Set.lean 3 28 ['PrParadoxy', 'dagurtomas', 'eric-wieser', 'github-actions', 'goliath-klein', 'leanprover-radar', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] nobody
26-81198
26 days ago
112-80389
112 days ago
10-66980
10 days
36890 vihdzp
author:vihdzp
 chore(SetTheory): `le_mul_left` → `le_mul_of_pos_left` The new theorem names/statements match [`Nat.le_mul_of_pos_left`](https://leanprover-community.github.io/mathlib4_docs/Init/Data/Nat/Lemmas.html#Nat.le_mul_of_pos_left). The cardinal one has also been moved to an earlier file. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-set-theory awaiting-zulip merge-conflict 28/23 Mathlib/SetTheory/Cardinal/Arithmetic.lean,Mathlib/SetTheory/Cardinal/Basic.lean,Mathlib/SetTheory/Cardinal/Free.lean,Mathlib/SetTheory/Ordinal/Arithmetic.lean,Mathlib/SetTheory/Ordinal/Exponential.lean,Mathlib/SetTheory/Ordinal/Notation.lean 6 2 ['github-actions', 'mathlib-merge-conflicts'] nobody
22-32207
22 days ago
25-18947
25 days ago
0-10825
3 hours
34077 kbuzzard
author:kbuzzard
 perf: increase priority of instSMulOfMul #31040 deprecated `Mul.toSMul` in place of the core instance `instSMulOfMul`, which is at a lowered priority of 910. This PR undeprecates it and makes it a higher priority instance (1100) which seems better for mathlib. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) This PR follows the philosophy seen in Mathlib's `Algebra.id : Algebra R R`, which also has raised priority. The idea is the same as `Algebra.id`: if you're looking for an instance of `Algebra R S` with R not equal to S then `Algebra.id` is extremely likely to fail quickly in practice, and if you're looking for an instance of `Algebra R R` then `Algebra.id` is unambiguously the right answer so should be tried ASAP. However the instance is defined so early in mathlib that in in practice it is tried last unless the priority is raised. The same philosophy holds here; if you're looking for an instance of `SMul X X` then you absolutely want to try `Mul.toSMul` first and if you're looking for an instance of `SMul X Y` with Y not X then `Mul.toSMul` will in practice be quick to fail. This PR was inspired by #33908 (another "this should be quick to fail and if it fits then it's almost certainly what we want" prio change) which made an instance of `IsScalarTower R A A` high priority and gave a performance boost. This PR also gives a performance boost. Note that the performance in #31040 looks very bad but the radar output is incorrect; there was a hardware change between the two runs. In fact #31040 produced no changes in profiling, as one might expect. I don't know the correct way to change the priority of a core instance in mathlib, and I didn't know if just changing the priority naively would work repo-wide rather than just file-wide, which was why this PR introduces a second instance. Zulip discussion at [#mathlib4 > priority hacks](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/priority.20hacks/with/574353616) t-algebra awaiting-zulip
label:t-algebra$
 3/9 Mathlib/Algebra/Group/Action/Defs.lean,Mathlib/Algebra/Group/Action/Units.lean 2 26 ['alreadydone', 'github-actions', 'kbuzzard', 'leanprover-radar', 'mathlib-merge-conflicts'] jcommelin
assignee:jcommelin
18-61896
18 days ago
55-28991
55 days ago
0-58585
16 hours
35578 Shreyas4991
author:Shreyas4991
 fix: writer monad should use an additive logging type The Writer monad's w type is supposed to be additive, not multiplicative. This is how it is conceptually used in Haskell (as a logging type). Haskell uses `Monoid` because it doesn't make a distinction between `AddMonoid` and `Monoid`. [#mathlib4 > Writer should use an additive monoid @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Writer.20should.20use.20an.20additive.20monoid/near/574990415) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data awaiting-zulip merge-conflict 10/10 Mathlib/Control/Monad/Cont.lean,Mathlib/Control/Monad/Writer.lean 2 5 ['Shreyas4991', 'eric-wieser', 'github-actions', 'mathlib-merge-conflicts'] nobody
18-42682
18 days ago
52-63200
52 days ago
0-18707
5 hours
36087 matthewjasper
author:matthewjasper
 chore: fix diamonds for Real/Complex Algebra instances Unfold or make `implicit_reducible` some definitions used to define `Algebra ℝ ℂ` . This should allow reducing use of `set_option backward.isDefEq.respectTransparency false`. --- - [x] depends on: #36694 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip 24/19 Mathlib/Algebra/Algebra/Defs.lean,Mathlib/Algebra/Algebra/Pi.lean,Mathlib/Algebra/Algebra/Prod.lean,Mathlib/Analysis/Complex/Basic.lean,Mathlib/Data/Complex/Basic.lean,Mathlib/LinearAlgebra/Complex/Module.lean,MathlibTest/instance_diamonds.lean 7 8 ['eric-wieser', 'github-actions', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'matthewjasper'] eric-wieser
assignee:eric-wieser
15-63002
15 days ago
16-78358
16 days ago
11-84307
11 days
30750 SnirBroshi
author:SnirBroshi
 feat(Data/Quot): `toSet` and `equivClassOf` Define `toSet` which gets the set corresponding to an element of a quotient, and `equivClassOf` which gets the equivalence class of an element under a quotient. --- I found these definitions helpful when working with quotients, specifically `ConnectedComponents` of a `TopologicalSpace`. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data awaiting-author awaiting-zulip 162/0 Mathlib/Data/Quot.lean,Mathlib/Data/Set/Image.lean,Mathlib/Data/SetLike/Basic.lean,Mathlib/Data/Setoid/Basic.lean 4 8 ['SnirBroshi', 'TwoFX', 'eric-wieser', 'github-actions', 'linesthatinterlace', 'mathlib-merge-conflicts'] TwoFX
assignee:TwoFX
0-14191
3 hours ago
138-27592
138 days ago
35-84279
35 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
37503 Vierkantor
author:Vierkantor
 chore(*): remove comments mentioning obsolete note `[nolint_ge]` In Lean 3 times we used to have a `ge_or_gt` linter which complained if theorem statements contained `≥` or `>`, and it would be silenced with a reference to the library note `[nolint_ge]`. But the linter and its note never got ported, so the references are irrelevant and we should drop them. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-linter tech debt 1/6 Mathlib/Algebra/Order/CauSeq/Basic.lean,Mathlib/Order/Basic.lean,Mathlib/Order/Filter/AtTopBot/Finite.lean,Mathlib/Topology/EMetricSpace/Basic.lean,Mathlib/Topology/MetricSpace/Cauchy.lean 5 4 ['Vierkantor', 'github-actions', 'grunweg'] nobody
12-20297
12 days ago
13-1209
13 days ago
13-1204
13 days
37358 grunweg
author:grunweg
 chore(Geometry/Manifold): don't expose definitions depending on choice Some definitions in `Immersion.lean` still depend on choice, but need to be exposed for subsequent instances using their definition. We leave them alone for now. Also make not exposing definition the default in `LocalDiffeomorph.lean`; four definitions have useful definitional equalities, the others do not. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-differential-geometry tech debt 12/12 Mathlib/Geometry/Manifold/Immersion.lean,Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean,Mathlib/Geometry/Manifold/LocalDiffeomorph.lean,Mathlib/Geometry/Manifold/VectorBundle/Basic.lean 4 1 ['github-actions'] PatrickMassot
assignee:PatrickMassot
2-52268
2 days ago
3-84462
3 days ago
3-84830
3 days
37678 vihdzp
author:vihdzp
 chore(Dynamics/FixedPoints/Defs): create `Defs` file --- I got a large import warning on another PR for simply importing the definition `Function.fixedPoints`, which I found rather silly. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-dynamics tech debt maintainer-merge 67/44 Mathlib.lean,Mathlib/Dynamics/FixedPoints/Basic.lean,Mathlib/Dynamics/FixedPoints/Defs.lean,Mathlib/Logic/Function/Defs.lean 4 2 ['Ruben-VandeVelde', 'github-actions'] urkud
assignee:urkud
1-24170
1 day ago
8-60858
8 days ago
8-61431
8 days
38007 JovanGerb
author:JovanGerb
 perf(Data/Complex/Basic): `no_expose` the `Inv` and `Norm` instance This PR hides some more implementation details of complex numbers. It would be possible to `no_expose` even more definitions, but this could be at the cost of some proof writing convenience. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) tech debt 11/12 Mathlib/Analysis/Complex/Basic.lean,Mathlib/Analysis/Complex/Norm.lean,Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean,Mathlib/Data/Complex/Basic.lean 4 6 ['JovanGerb', 'github-actions', 'grunweg', 'leanprover-radar'] nobody
0-59866
16 hours ago
0-78943
21 hours ago
0-79027
21 hours