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: July 01, 2025 at 20:13 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
26161 leanprover-community-mathlib4-bot
author:leanprover-community-mathlib4-bot
chore: adaptations for nightly-2025-06-19 merge-conflict ready-to-merge 26/19 Mathlib/Algebra/CharP/Basic.lean,Mathlib/Algebra/CharP/Defs.lean,Mathlib/Algebra/Group/Basic.lean,lake-manifest.json,lean-toolchain 5 n/a ['YaelDillies', 'github-actions', 'kim-em', 'mathlib-bors'] nobody
11-73864
11 days ago
unknown
unknown

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
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
26-22531
26 days ago
29-2503
29 days ago
33-12121
33 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
24-1337
24 days ago
24-1337
24 days ago
37-67159
37 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
23-42493
23 days ago
23-42493
23 days ago
24-18025
24 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
22-79610
22 days ago
22-79610
22 days ago
23-5097
23 days
24669 qawbecrdtey
author:qawbecrdtey
feat(Analysis/Normed/Operator/LinearIsometry): added definition `LinearIsometryEquiv.prodComm` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) This commit defines a `LinearIsometryEquiv`, and states some trivial theorems about it. ```lean def prodComm [Module R E₂] : E × E₂ ≃ₗᵢ[R] E₂ × E ``` maintainer-merge t-analysis awaiting-author 8/1 Mathlib/Analysis/Normed/Operator/LinearIsometry.lean 1 10 ['Ruben-VandeVelde', 'eric-wieser', 'faenuccio', 'github-actions', 'j-loreaux', 'jcommelin', 'qawbecrdtey'] faenuccio
assignee:faenuccio
21-54995
21 days ago
21-54995
21 days ago
32-83569
32 days
23849 chrisflav
author:chrisflav
feat(Data/Set): add `Set.encard_iUnion` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) large-import t-data maintainer-merge 69/0 Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Data/Set/Card/Arithmetic.lean,Mathlib/Data/Set/Finite/Lattice.lean 3 25 ['YaelDillies', 'chrisflav', 'github-actions'] YaelDillies
assignee:YaelDillies
21-31058
21 days ago
21-31058
21 days ago
83-44848
83 days
25881 eric-wieser
author:eric-wieser
chore: extract an auxiliary function from `congr()` The motivation here is to make it easier to review #25851. This code is moved (and unindented) without changes. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip maintainer-merge t-meta 72/61 Mathlib/Tactic/TermCongr.lean 1 5 ['eric-wieser', 'github-actions', 'grunweg', 'kmill'] nobody
16-81345
16 days ago
16-81345
16 days ago
0-3293
54 minutes
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 11 ['eric-wieser', 'github-actions', 'jsm28', 'ocfnash'] nobody
4-86362
4 days ago
37-26553
1 month ago
37-67425
37 days
26405 euprunin
author:euprunin
chore: golf using `omega` maintainer-merge 23/68 Mathlib/Algebra/Polynomial/Module/Basic.lean,Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean,Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean,Mathlib/Combinatorics/Enumerative/Composition.lean,Mathlib/Computability/DFA.lean,Mathlib/Control/Fix.lean,Mathlib/Data/Nat/Choose/Basic.lean,Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean,Mathlib/Geometry/Euclidean/Circumcenter.lean,Mathlib/GroupTheory/Coxeter/Length.lean,Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean,Mathlib/MeasureTheory/Function/ConditionalExpectation/Unique.lean,Mathlib/NumberTheory/Dioph.lean,Mathlib/Order/Partition/Equipartition.lean,Mathlib/SetTheory/Game/State.lean,Mathlib/Tactic/NormNum/LegendreSymbol.lean,Mathlib/Topology/EMetricSpace/BoundedVariation.lean 17 10 ['euprunin', 'github-actions', 'grunweg', 'leanprover-bot'] nobody
4-73914
4 days ago
4-73914
4 days ago
6-24383
6 days
26004 vasnesterov
author:vasnesterov
feat(Algebra/Order/Floor): `⌊n * x⌋₊ / n = ⌊x⌋₊` Prove that `⌊n * x⌋₊ / n = ⌊x⌋₊` for natural `n`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-order t-algebra
label:t-algebra$
39/9 Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean,Mathlib/Algebra/Order/Floor/Ring.lean,Mathlib/Algebra/Order/Floor/Semiring.lean,Mathlib/Data/EReal/Inv.lean 4 21 ['Ruben-VandeVelde', 'YaelDillies', 'b-mehta', 'eric-wieser', 'github-actions', 'vasnesterov'] nobody
4-47191
4 days ago
unknown
unknown
26426 Komyyy
author:Komyyy
doc: remove `PartENat.card` in the module doc [`PartENat.card`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Deprecated/Cardinal/Finite.html#PartENat.card) is moved to the `Deprecated` directory and it's not in this file([`Mathlib.SetTheory.Cardinal.Finite`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/SetTheory/Cardinal/Finite.html)) anymore. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-set-theory maintainer-merge easy documentation 0/2 Mathlib/SetTheory/Cardinal/Finite.lean 1 2 ['github-actions', 'grunweg'] nobody
4-38831
4 days ago
4-38831
4 days ago
4-38844
4 days
26502 sgouezel
author:sgouezel
feat: monotonicity of `lineMap` Also remove one assumption in `differentiableOn_integral_of_continuous`, and expand docstrings around this theorem. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-analysis 49/10 Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/FundThmCalculus.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/IntegrationByParts.lean,Mathlib/Topology/Algebra/ContinuousAffineMap.lean 4 6 ['eric-wieser', 'github-actions', 'grunweg', 'sgouezel'] nobody
2-28650
2 days ago
2-47841
2 days ago
2-53440
2 days
26166 joelriou
author:joelriou
feat(AlgebraicTopology): application of the retract argument to model categories Basic consequences of the retract argument are obtained for model categories: cofibrations are exactly the morphisms that have the left lifting property with respect to trivial fibrations, etc. We deduce various properties of cofibrations, fibrations and weak equivalences in model categories (e.g. they are stable by composition). --- (I am sorry if this one is a little bit long. There are too many basic properties to state.) This PR continues the work from #20210. Original PR: https://github.com/leanprover-community/mathlib4/pull/20210 large-import maintainer-merge t-topology 450/4 Mathlib.lean,Mathlib/AlgebraicTopology/ModelCategory/Basic.lean,Mathlib/AlgebraicTopology/ModelCategory/Instances.lean 3 n/a ['github-actions', 'joelriou', 'robin-carlier'] robin-carlier
assignee:robin-carlier
1-49888
1 day ago
unknown
unknown
24361 Hagb
author:Hagb
feat(Data/Finsupp/MonomialOrder): `0 ≤ a` where `a : m.syn` `simp` would be able to solve it. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data maintainer-merge new-contributor easy 3/0 Mathlib/Data/Finsupp/MonomialOrder.lean 1 2 ['Ruben-VandeVelde', 'github-actions'] nobody
1-43784
1 day ago
1-43784
1 day ago
67-44546
67 days
24582 pechersky
author:pechersky
feat(GroupTheory/ArchimedeanDensely): Unique (ℤ ≃+o ℤ) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) - [x] depends on: #24580 maintainer-merge t-order t-algebra
label:t-algebra$
44/0 Mathlib/Data/Int/Cast/Lemmas.lean,Mathlib/GroupTheory/ArchimedeanDensely.lean 2 6 ['Ruben-VandeVelde', 'eric-wieser', 'github-actions', 'mathlib4-dependent-issues-bot', 'pechersky'] nobody
1-40675
1 day ago
1-40675
1 day ago
37-28881
37 days
25758 YaelDillies
author:YaelDillies
chore: shortcut instance `CompleteLattice α → PartialOrder α` This avoids using the path `CompleteLattice α → CompletePartialOrder α → PartialOrder α` that goes through `Order.CompletePartialOrder` and makes it appear used to our automation, such as `shake` or `#min_imports`. This is a followup to #25358. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-order 7/0 Mathlib/Order/CompleteLattice/Defs.lean 1 2 ['Ruben-VandeVelde', 'github-actions'] nobody
1-40566
1 day ago
1-40566
1 day ago
19-41054
19 days
25897 YaelDillies
author:YaelDillies
feat: `ofNat(n) • a = ofNat(n) * a` From Toric --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) toric t-data maintainer-merge t-algebra
label:t-algebra$
3/0 Mathlib/Data/Nat/Cast/Basic.lean 1 2 ['Ruben-VandeVelde', 'github-actions'] nobody
1-40445
1 day ago
1-40445
1 day ago
16-37955
16 days
26027 vasnesterov
author:vasnesterov
feat(Topology): every compact metric space can be embedded into the Hilbert cube Prove `exists_closed_embedding_to_hilbert_cube`: every compact metric space can be embedded into the Hilbert cube. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-topology 58/1 Mathlib.lean,Mathlib/Topology/Compactness/HilbertCubeEmbedding.lean,Mathlib/Topology/MetricSpace/Bounded.lean 3 9 ['ADedecker', 'github-actions', 'jcommelin', 'vasnesterov'] nobody
1-37703
1 day ago
1-37703
1 day ago
14-20262
14 days
26285 kckennylau
author:kckennylau
feat(RingTheory): resultant of two polynomials Co-authored-by: Anne Baanen --- Split from #26283. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-algebra
label:t-algebra$
87/0 Mathlib.lean,Mathlib/RingTheory/Polynomial/Resultant/Basic.lean 2 20 ['MichaelStollBayreuth', 'YaelDillies', 'eric-wieser', 'github-actions', 'kckennylau'] nobody
1-29210
1 day ago
1-31228
1 day ago
8-63393
8 days
25945 adomani
author:adomani
feat: the empty line in commands linter This linter flags empty lines within a command. It allows empty lines within doc-strings, module-docs and a couple of other "sensible" places. It also skips files that are likely to contain meta-code, since there the use of empty lines in definition is more widespread. This PR continues the work from #25236. large-import maintainer-merge 375/5 Mathlib.lean,Mathlib/CategoryTheory/Comma/StructuredArrow/CommaMap.lean,Mathlib/Init.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/EmptyLine.lean,MathlibTest/EmptyLine.lean 6 3 ['adomani', 'github-actions'] nobody
1-13946
1 day ago
15-46563
15 days ago
15-46618
15 days
25491 tannerduve
author:tannerduve
feat(Control/Monad/Free): define free monad, prove it lawful, and implement standard effects This PR introduces the `Free` monad. This implementation uses the "freer monad" approach as the traditional free monad (eg from [Haskell](https://hackage.haskell.org/package/free-5.2/docs/Control-Monad-Free.html)) is not safely definable in Lean due to termination checking (it's not strictly positive). The main contributions are: * Definition of the `Free` monad as an inductive type which generates a monad given any type constructor `F : Type -> Type`. * Functor and Monad instances for `Free F`, along with proofs of the `LawfulFunctor` and `LawfulMonad` laws. * Canonical instances of `Free` with standard effect signatures: * `FreeState s` for stateful computations, defined via a `StateF s` functor with `get` and `put` operations. * `FreeWriter w` for logging computations, defined via a `WriterF w` functor with a `tell` operation. * `FreeCont r` for continuation-passing computations, using the CPS functor `(α → r) → r`. In this construction, computations are represented as **trees of effects**. Each node (`liftBind`) represents a request to perform an effect, accompanied by a continuation specifying how the computation proceeds after the effect. The leaves (`pure`) represent completed computations with final results. A key insight is that `FreeM F` satisfies the **universal property of free monads**: for any monad `M` and effect handler `f : F → M`, there exists a unique way to interpret `FreeM F` computations in `M` that respects the effect semantics given by `f`. This unique interpreter is `mapM f`, which acts as the canonical **fold** for free monads. To execute or interpret these computations, we provide two approaches: 1. **Hand-written interpreters** (`FreeState.run`, `FreeWriter.run`, `FreeCont.run`) that directly pattern-match on the tree structure 2. **Canonical interpreters** (`FreeState.fold`, `FreeWriter.fold`, `FreeCont.fold`) derived from the universal property via `mapM` And then prove that these approaches are equivalent --- This PR adds new files and definitions; no breaking changes. **Tags:** free monad, freer monad, effect systems, state monad, writer monad, continuation monad, operational semantics, verified interpreters t-data maintainer-merge 717/0 Mathlib.lean,Mathlib/Control/Monad/Free.lean,MathlibTest/freemonad.lean,docs/references.bib 4 144 ['YaelDillies', 'copilot-pull-request-reviewer', 'eric-wieser', 'github-actions', 'plp127', 'quangvdao', 'tannerduve'] nobody
1-5802
1 day ago
14-18519
14 days ago
24-37603
24 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
55-80180
1 month ago
102-58807
3 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
28-63148
28 days ago
28-63149
28 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
24-47366
24 days ago
24-47366
24 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
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
26-22531
26 days ago
29-2503
29 days ago
33-12121
33 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
24-1337
24 days ago
24-1337
24 days ago
37-67159
37 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
23-42493
23 days ago
23-42493
23 days ago
24-18025
24 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
22-79610
22 days ago
22-79610
22 days ago
23-5097
23 days
24669 qawbecrdtey
author:qawbecrdtey
feat(Analysis/Normed/Operator/LinearIsometry): added definition `LinearIsometryEquiv.prodComm` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) This commit defines a `LinearIsometryEquiv`, and states some trivial theorems about it. ```lean def prodComm [Module R E₂] : E × E₂ ≃ₗᵢ[R] E₂ × E ``` maintainer-merge t-analysis awaiting-author 8/1 Mathlib/Analysis/Normed/Operator/LinearIsometry.lean 1 10 ['Ruben-VandeVelde', 'eric-wieser', 'faenuccio', 'github-actions', 'j-loreaux', 'jcommelin', 'qawbecrdtey'] faenuccio
assignee:faenuccio
21-54995
21 days ago
21-54995
21 days ago
32-83569
32 days
23849 chrisflav
author:chrisflav
feat(Data/Set): add `Set.encard_iUnion` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) large-import t-data maintainer-merge 69/0 Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Data/Set/Card/Arithmetic.lean,Mathlib/Data/Set/Finite/Lattice.lean 3 25 ['YaelDillies', 'chrisflav', 'github-actions'] YaelDillies
assignee:YaelDillies
21-31058
21 days ago
21-31058
21 days ago
83-44848
83 days
25881 eric-wieser
author:eric-wieser
chore: extract an auxiliary function from `congr()` The motivation here is to make it easier to review #25851. This code is moved (and unindented) without changes. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip maintainer-merge t-meta 72/61 Mathlib/Tactic/TermCongr.lean 1 5 ['eric-wieser', 'github-actions', 'grunweg', 'kmill'] nobody
16-81345
16 days ago
16-81345
16 days ago
0-3293
54 minutes
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 11 ['eric-wieser', 'github-actions', 'jsm28', 'ocfnash'] nobody
4-86362
4 days ago
37-26553
1 month ago
37-67425
37 days
26405 euprunin
author:euprunin
chore: golf using `omega` maintainer-merge 23/68 Mathlib/Algebra/Polynomial/Module/Basic.lean,Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean,Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean,Mathlib/Combinatorics/Enumerative/Composition.lean,Mathlib/Computability/DFA.lean,Mathlib/Control/Fix.lean,Mathlib/Data/Nat/Choose/Basic.lean,Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean,Mathlib/Geometry/Euclidean/Circumcenter.lean,Mathlib/GroupTheory/Coxeter/Length.lean,Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean,Mathlib/MeasureTheory/Function/ConditionalExpectation/Unique.lean,Mathlib/NumberTheory/Dioph.lean,Mathlib/Order/Partition/Equipartition.lean,Mathlib/SetTheory/Game/State.lean,Mathlib/Tactic/NormNum/LegendreSymbol.lean,Mathlib/Topology/EMetricSpace/BoundedVariation.lean 17 10 ['euprunin', 'github-actions', 'grunweg', 'leanprover-bot'] nobody
4-73914
4 days ago
4-73914
4 days ago
6-24383
6 days
26004 vasnesterov
author:vasnesterov
feat(Algebra/Order/Floor): `⌊n * x⌋₊ / n = ⌊x⌋₊` Prove that `⌊n * x⌋₊ / n = ⌊x⌋₊` for natural `n`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-order t-algebra
label:t-algebra$
39/9 Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean,Mathlib/Algebra/Order/Floor/Ring.lean,Mathlib/Algebra/Order/Floor/Semiring.lean,Mathlib/Data/EReal/Inv.lean 4 21 ['Ruben-VandeVelde', 'YaelDillies', 'b-mehta', 'eric-wieser', 'github-actions', 'vasnesterov'] nobody
4-47191
4 days ago
unknown
unknown
26426 Komyyy
author:Komyyy
doc: remove `PartENat.card` in the module doc [`PartENat.card`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Deprecated/Cardinal/Finite.html#PartENat.card) is moved to the `Deprecated` directory and it's not in this file([`Mathlib.SetTheory.Cardinal.Finite`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/SetTheory/Cardinal/Finite.html)) anymore. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-set-theory maintainer-merge easy documentation 0/2 Mathlib/SetTheory/Cardinal/Finite.lean 1 2 ['github-actions', 'grunweg'] nobody
4-38831
4 days ago
4-38831
4 days ago
4-38844
4 days
26502 sgouezel
author:sgouezel
feat: monotonicity of `lineMap` Also remove one assumption in `differentiableOn_integral_of_continuous`, and expand docstrings around this theorem. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-analysis 49/10 Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/FundThmCalculus.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/IntegrationByParts.lean,Mathlib/Topology/Algebra/ContinuousAffineMap.lean 4 6 ['eric-wieser', 'github-actions', 'grunweg', 'sgouezel'] nobody
2-28650
2 days ago
2-47841
2 days ago
2-53440
2 days
26166 joelriou
author:joelriou
feat(AlgebraicTopology): application of the retract argument to model categories Basic consequences of the retract argument are obtained for model categories: cofibrations are exactly the morphisms that have the left lifting property with respect to trivial fibrations, etc. We deduce various properties of cofibrations, fibrations and weak equivalences in model categories (e.g. they are stable by composition). --- (I am sorry if this one is a little bit long. There are too many basic properties to state.) This PR continues the work from #20210. Original PR: https://github.com/leanprover-community/mathlib4/pull/20210 large-import maintainer-merge t-topology 450/4 Mathlib.lean,Mathlib/AlgebraicTopology/ModelCategory/Basic.lean,Mathlib/AlgebraicTopology/ModelCategory/Instances.lean 3 n/a ['github-actions', 'joelriou', 'robin-carlier'] robin-carlier
assignee:robin-carlier
1-49888
1 day ago
unknown
unknown
24361 Hagb
author:Hagb
feat(Data/Finsupp/MonomialOrder): `0 ≤ a` where `a : m.syn` `simp` would be able to solve it. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data maintainer-merge new-contributor easy 3/0 Mathlib/Data/Finsupp/MonomialOrder.lean 1 2 ['Ruben-VandeVelde', 'github-actions'] nobody
1-43784
1 day ago
1-43784
1 day ago
67-44546
67 days
24582 pechersky
author:pechersky
feat(GroupTheory/ArchimedeanDensely): Unique (ℤ ≃+o ℤ) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) - [x] depends on: #24580 maintainer-merge t-order t-algebra
label:t-algebra$
44/0 Mathlib/Data/Int/Cast/Lemmas.lean,Mathlib/GroupTheory/ArchimedeanDensely.lean 2 6 ['Ruben-VandeVelde', 'eric-wieser', 'github-actions', 'mathlib4-dependent-issues-bot', 'pechersky'] nobody
1-40675
1 day ago
1-40675
1 day ago
37-28881
37 days
25758 YaelDillies
author:YaelDillies
chore: shortcut instance `CompleteLattice α → PartialOrder α` This avoids using the path `CompleteLattice α → CompletePartialOrder α → PartialOrder α` that goes through `Order.CompletePartialOrder` and makes it appear used to our automation, such as `shake` or `#min_imports`. This is a followup to #25358. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-order 7/0 Mathlib/Order/CompleteLattice/Defs.lean 1 2 ['Ruben-VandeVelde', 'github-actions'] nobody
1-40566
1 day ago
1-40566
1 day ago
19-41054
19 days
25897 YaelDillies
author:YaelDillies
feat: `ofNat(n) • a = ofNat(n) * a` From Toric --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) toric t-data maintainer-merge t-algebra
label:t-algebra$
3/0 Mathlib/Data/Nat/Cast/Basic.lean 1 2 ['Ruben-VandeVelde', 'github-actions'] nobody
1-40445
1 day ago
1-40445
1 day ago
16-37955
16 days
26027 vasnesterov
author:vasnesterov
feat(Topology): every compact metric space can be embedded into the Hilbert cube Prove `exists_closed_embedding_to_hilbert_cube`: every compact metric space can be embedded into the Hilbert cube. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-topology 58/1 Mathlib.lean,Mathlib/Topology/Compactness/HilbertCubeEmbedding.lean,Mathlib/Topology/MetricSpace/Bounded.lean 3 9 ['ADedecker', 'github-actions', 'jcommelin', 'vasnesterov'] nobody
1-37703
1 day ago
1-37703
1 day ago
14-20262
14 days
26285 kckennylau
author:kckennylau
feat(RingTheory): resultant of two polynomials Co-authored-by: Anne Baanen --- Split from #26283. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-algebra
label:t-algebra$
87/0 Mathlib.lean,Mathlib/RingTheory/Polynomial/Resultant/Basic.lean 2 20 ['MichaelStollBayreuth', 'YaelDillies', 'eric-wieser', 'github-actions', 'kckennylau'] nobody
1-29210
1 day ago
1-31228
1 day ago
8-63393
8 days
25945 adomani
author:adomani
feat: the empty line in commands linter This linter flags empty lines within a command. It allows empty lines within doc-strings, module-docs and a couple of other "sensible" places. It also skips files that are likely to contain meta-code, since there the use of empty lines in definition is more widespread. This PR continues the work from #25236. large-import maintainer-merge 375/5 Mathlib.lean,Mathlib/CategoryTheory/Comma/StructuredArrow/CommaMap.lean,Mathlib/Init.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/EmptyLine.lean,MathlibTest/EmptyLine.lean 6 3 ['adomani', 'github-actions'] nobody
1-13946
1 day ago
15-46563
15 days ago
15-46618
15 days
25491 tannerduve
author:tannerduve
feat(Control/Monad/Free): define free monad, prove it lawful, and implement standard effects This PR introduces the `Free` monad. This implementation uses the "freer monad" approach as the traditional free monad (eg from [Haskell](https://hackage.haskell.org/package/free-5.2/docs/Control-Monad-Free.html)) is not safely definable in Lean due to termination checking (it's not strictly positive). The main contributions are: * Definition of the `Free` monad as an inductive type which generates a monad given any type constructor `F : Type -> Type`. * Functor and Monad instances for `Free F`, along with proofs of the `LawfulFunctor` and `LawfulMonad` laws. * Canonical instances of `Free` with standard effect signatures: * `FreeState s` for stateful computations, defined via a `StateF s` functor with `get` and `put` operations. * `FreeWriter w` for logging computations, defined via a `WriterF w` functor with a `tell` operation. * `FreeCont r` for continuation-passing computations, using the CPS functor `(α → r) → r`. In this construction, computations are represented as **trees of effects**. Each node (`liftBind`) represents a request to perform an effect, accompanied by a continuation specifying how the computation proceeds after the effect. The leaves (`pure`) represent completed computations with final results. A key insight is that `FreeM F` satisfies the **universal property of free monads**: for any monad `M` and effect handler `f : F → M`, there exists a unique way to interpret `FreeM F` computations in `M` that respects the effect semantics given by `f`. This unique interpreter is `mapM f`, which acts as the canonical **fold** for free monads. To execute or interpret these computations, we provide two approaches: 1. **Hand-written interpreters** (`FreeState.run`, `FreeWriter.run`, `FreeCont.run`) that directly pattern-match on the tree structure 2. **Canonical interpreters** (`FreeState.fold`, `FreeWriter.fold`, `FreeCont.fold`) derived from the universal property via `mapM` And then prove that these approaches are equivalent --- This PR adds new files and definitions; no breaking changes. **Tags:** free monad, freer monad, effect systems, state monad, writer monad, continuation monad, operational semantics, verified interpreters t-data maintainer-merge 717/0 Mathlib.lean,Mathlib/Control/Monad/Free.lean,MathlibTest/freemonad.lean,docs/references.bib 4 144 ['YaelDillies', 'copilot-pull-request-reviewer', 'eric-wieser', 'github-actions', 'plp127', 'quangvdao', 'tannerduve'] nobody
1-5802
1 day ago
14-18519
14 days ago
24-37603
24 days
26543 vihdzp
author:vihdzp
feat(SetTheory/ZFC/VonNeumann): von Neumann hierarchy of sets Ported from #17027. For extra discussion on this PR, see [Zulip](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2317027.20.2C.20.2326518.20von.20Neumann.20hierarchy/with/526389347). --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-set-theory maintainer-merge 133/0 Mathlib.lean,Mathlib/SetTheory/Ordinal/Basic.lean,Mathlib/SetTheory/ZFC/Basic.lean,Mathlib/SetTheory/ZFC/VonNeumann.lean 4 55 ['alreadydone', 'github-actions', 'kckennylau', 'vihdzp'] nobody
0-81312
22 hours ago
0-81553
22 hours ago
1-24692
1 day
26411 sgouezel
author:sgouezel
feat: add `iInf` results on `ENNReal`, matching existing `iSup` ones --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data maintainer-merge 39/0 Mathlib/Data/ENNReal/Operations.lean 1 22 ['YaelDillies', 'github-actions', 'grunweg', 'sgouezel'] nobody
0-42526
11 hours ago
0-42526
11 hours ago
5-23310
5 days
26562 Ruben-VandeVelde
author:Ruben-VandeVelde
chore: deprecate Mathlib.Algebra.Ring.Hom.Basic It was emptied in #25447. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) large-import maintainer-merge t-algebra
label:t-algebra$
4/10 Mathlib/Algebra/Ring/Hom/Basic.lean 1 4 ['Ruben-VandeVelde', 'github-actions', 'grunweg'] nobody
0-41736
11 hours ago
0-41837
11 hours ago
0-81219
22 hours
26576 kim-em
author:kim-em
feat: use grind in Data/Nat/Hyperoperations Some nice interactions between `grind`'s ring handling, case splitting, and instantiation. maintainer-merge 35/57 Mathlib/Algebra/Group/Even.lean,Mathlib/Data/Nat/Hyperoperation.lean 2 7 ['dupuisf', 'github-actions', 'grunweg', 'leanprover-bot'] nobody
0-72
1 minute ago
0-49
33 seconds ago
0-47571
13 hours
26570 winstonyin
author:winstonyin
feat: version of `prod_range_induction` with weaker assumptions `prod_range_induction` currently requires ratios of adjacent terms to be checked for the entire sequence, but we only need to check terms up to `n`. I provide a parallel `prod_range_induction'` that relaxes this assumption. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-algebra
label:t-algebra$
13/0 Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean 1 3 ['github-actions', 'grunweg'] grunweg
assignee:grunweg
0-40006
11 hours ago
0-43160
11 hours ago
0-58322
16 hours
26365 joelriou
author:joelriou
feat(CategoryTheory/Localization): generalize results about adjunctions In this PR, results about adjunctions, localization of categories and calculus of fractions are slightly generalized. In particular, we show that under certain circumstances, adjoint functors are localization functors. (This shall be used in the proof of the fundamental lemma of homotopical algebra #26303.) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-category-theory 108/25 Mathlib/CategoryTheory/Localization/CalculusOfFractions/OfAdjunction.lean,Mathlib/CategoryTheory/Localization/Opposite.lean 2 7 ['github-actions', 'joelriou', 'robin-carlier'] robin-carlier
assignee:robin-carlier
0-35926
9 hours ago
0-36138
10 hours ago
7-15308
7 days
25919 BoltonBailey
author:BoltonBailey
doc: suggest !bench in `lake exe pole` This PR makes an error message on `lake exe pole` give some information which is often relevant. Original PR: https://github.com/leanprover-community/mathlib4/pull/12561 maintainer-merge 2/1 LongestPole/Main.lean 1 3 ['BoltonBailey', 'Ruben-VandeVelde', 'github-actions'] nobody
0-11431
3 hours ago
0-40247
11 hours ago
16-16136
16 days
25872 101damnations
author:101damnations
feat(RepresentationTheory/GroupCohomology): long exact sequences Given a commutative ring `k` and a group `G`, this PR shows that a short exact sequence of `k`-linear `G`-representations `0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0` induces a short exact sequence of complexes `0 ⟶ inhomogeneousCochains X₁ ⟶ inhomogeneousCochains X₂ ⟶ inhomogeneousCochains X₃ ⟶ 0`. Since the cohomology of `inhomogeneousCochains Xᵢ` is the group cohomology of `Xᵢ`, this allows us to specialize API about long exact sequences to group cohomology. --- - [x] depends on: #25815 - [x] depends on: #25870 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) --- *This PR continues the work from #25311.* *Original PR: https://github.com/leanprover-community/mathlib4/pull/25311* maintainer-merge t-algebra
label:t-algebra$
290/7 Mathlib.lean,Mathlib/Algebra/Homology/ConcreteCategory.lean,Mathlib/Algebra/Homology/HomologySequence.lean,Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean,Mathlib/LinearAlgebra/Pi.lean,Mathlib/RepresentationTheory/Homological/GroupCohomology/Basic.lean,Mathlib/RepresentationTheory/Homological/GroupCohomology/LongExactSequence.lean,Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean 8 10 ['101damnations', 'github-actions', 'kbuzzard', 'mathlib4-dependent-issues-bot'] nobody
0-10445
2 hours ago
1-79351
1 day ago
14-59748
14 days
26584 mariainesdff
author:mariainesdff
chore(Algebra.Order.Group.Cyclic): generalize Subgroup.genLTOne Generalize `Subgroup.genLTOne` so that it assumes that the subgroup itself is cyclic, rather than the ambient group. Co-authored-by: @faenuccio --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-algebra
label:t-algebra$
13/7 Mathlib/Algebra/Order/Group/Cyclic.lean 1 2 ['github-actions', 'grunweg'] nobody
0-9579
2 hours ago
0-9579
2 hours ago
0-27046
7 hours
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
55-80180
1 month ago
102-58807
3 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
28-63148
28 days ago
28-63149
28 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
24-47366
24 days ago
24-47366
24 days ago
17-72244
17 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
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
83-4410
2 months ago
83-4499
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
56-78287
1 month ago
56-78296
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
56-77598
1 month ago
56-78233
1 month ago
75-77754
75 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
43-64248
1 month ago
43-84675
1 month 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
27-44058
27 days ago
56-78197
1 month ago
48-67492
48 days
23929 meithecatte
author:meithecatte
feat(Computability/NFA): improve bound on pumping lemma --- - [x] depends on: #25321 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip t-computability new-contributor 101/10 Mathlib/Computability/EpsilonNFA.lean,Mathlib/Computability/NFA.lean 2 41 ['YaelDillies', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'meithecatte'] nobody
24-1449
24 days ago
24-1450
24 days ago
34-10595
34 days
25881 eric-wieser
author:eric-wieser
chore: extract an auxiliary function from `congr()` The motivation here is to make it easier to review #25851. This code is moved (and unindented) without changes. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-zulip maintainer-merge t-meta 72/61 Mathlib/Tactic/TermCongr.lean 1 5 ['eric-wieser', 'github-actions', 'grunweg', 'kmill'] nobody
16-81345
16 days ago
16-81345
16 days ago
0-3293
54 minutes
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 30 ['MichaelStollBayreuth', 'Multramate', 'acmepjz', 'github-actions', 'grunweg', 'kckennylau'] nobody
13-34673
13 days ago
29-32551
29 days ago
6-51040
6 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
288-55320
9 months ago
288-77295
9 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
241-9039
7 months ago
266-83961
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
223-28570
7 months ago
223-28570
7 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
67-70347
2 months ago
79-12577
2 months 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
56-78247
1 month ago
56-78252
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
43-14453
1 month ago
43-14454
1 month 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
43-13527
1 month ago
43-13529
1 month 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
29-49425
29 days ago
29-49425
29 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
29-11527
29 days ago
29-11529
29 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
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
22-66656
22 days ago
22-66678
22 days ago
28-60292
28 days
25776 Parcly-Taxel
author:Parcly-Taxel
chore: deprime `induction` in `Analysis` I think this is very marginally dependent on #25770. tech debt t-analysis 256/208 Mathlib/Analysis/Analytic/Composition.lean,Mathlib/Analysis/Analytic/Constructions.lean,Mathlib/Analysis/Analytic/Inverse.lean,Mathlib/Analysis/BoxIntegral/Basic.lean,Mathlib/Analysis/BoxIntegral/Box/SubboxInduction.lean,Mathlib/Analysis/BoxIntegral/Partition/Additive.lean,Mathlib/Analysis/BoxIntegral/Partition/Split.lean,Mathlib/Analysis/CStarAlgebra/Basic.lean,Mathlib/Analysis/CStarAlgebra/Multiplier.lean,Mathlib/Analysis/Calculus/ContDiff/Basic.lean,Mathlib/Analysis/Calculus/ContDiff/Bounds.lean,Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean,Mathlib/Analysis/Calculus/ContDiff/Operations.lean,Mathlib/Analysis/Calculus/Deriv/ZPow.lean,Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean,Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean,Mathlib/Analysis/Calculus/SmoothSeries.lean,Mathlib/Analysis/Convex/Combination.lean,Mathlib/Analysis/Convex/Radon.lean,Mathlib/Analysis/InnerProductSpace/Projection.lean,Mathlib/Analysis/Normed/Algebra/Exponential.lean,Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean,Mathlib/Analysis/Seminorm.lean,Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean,Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean,Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Deriv.lean,Mathlib/Analysis/SpecialFunctions/Integrals.lean,Mathlib/Analysis/SpecialFunctions/Log/Basic.lean,Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean,Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean,Mathlib/Analysis/SpecialFunctions/Pow/Real.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean 35 2 ['Parcly-Taxel', 'github-actions'] nobody
19-36981
19 days ago
19-37414
19 days ago
19-37458
19 days
25790 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
19-35657
19 days ago
19-35756
19 days ago
19-35744
19 days
25774 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 133/124 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
19-23626
19 days ago
19-37863
19 days ago
19-37848
19 days
25770 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 134/115 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/SuccPred/Archimedean.lean,Mathlib/Order/Synonym.lean 15 10 ['Parcly-Taxel', 'eric-wieser', 'github-actions'] nobody
16-44842
16 days ago
19-39688
19 days ago
19-39673
19 days
25915 BoltonBailey
author:BoltonBailey
chore(Algebra/Squarefree/Basic): fix erw This PR addresses an instance of the erw linter in Algebra/Squarefree/Basic. Original PR: https://github.com/leanprover-community/mathlib4/pull/25161 tech debt t-algebra easy
label:t-algebra$
1/1 Mathlib/Algebra/Squarefree/Basic.lean 1 1 ['github-actions'] nobody
4-63159
4 days ago
8-85081
8 days ago
16-16745
16 days
26404 grunweg
author:grunweg
chore: clean up and remove FunProp/Differentiable - one lemma in that file already exists, hence can be removed (We don't add a deprecation as I presume people will not have used it.) - move the three remaining lemmas in that file to their proper place, and use the now `fun_` naming convention (Omitting deprecations again.) - after this, `FunProp/Differentiable` is empty and need not be imported any more: add a module deprecation --- - [x] depends on: #26355 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) tech debt 23/49 Mathlib/Analysis/Calculus/FDeriv/Comp.lean,Mathlib/Tactic/FunProp/ContDiff.lean,Mathlib/Tactic/FunProp/Differentiable.lean,MathlibTest/fun_prop2.lean 4 3 ['github-actions', 'grunweg', 'mathlib4-dependent-issues-bot'] nobody
0-74461
20 hours ago
6-13827
6 days ago
6-13872
6 days