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: March 04, 2026 at 16:21 UTC

Stale ready-to-merge'd PRs

Number Author Title Description Labels +/- Modified files (first 100) 📝 💬 All users who commented or reviewed Assignee(s) Updated Last status change total time in review
33650 vihdzp
author:vihdzp
 refactor: deprecate bespoke `Hyperreal` machinery Currently, these six definitions are in the `Hyperreal` namespace: - `IsSt x r`: a predicate for `r` being a standard part of `x` - `st x`: the standard part of `x` - `Infinitesimal x`: predicate for infinitesimal elements - `InfinitePos x`: predicate for infinite and positive elements - `InfiniteNeg x`: predicate for infinite and negative elements - `Infinite x`: predicate for infinite (positive or negative) elements. We deprecate all six of these and all of their API, in favor of reasoning with [`ArchimedeanClass`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Order/Archimedean/Class.html#ArchimedeanClass) and [`ArchimedeanClass.stdPart`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Order/Ring/StandardPart.html#ArchimedeanClass.stdPart). The replacements are as follows: - `IsSt x r`: `0 ≀ ArchimedeanClass.mk x ∧ stdPart x = r` - `st x`: `stdPart x` - `Infinitesimal x`: `0 < ArchimedeanClass.mk x` - `InfinitePos x`: `0 < x ∧ ArchimedeanClass.mk x < 0` - `InfiniteNeg x`: `x < 0 ∧ ArchimedeanClass.mk x < 0` - `Infinite x`: `ArchimedeanClass.mk x < 0` All of these equivalences are proved within the PR, though these new theorems have also been insta-deprecated. Most of the existing API on these predicates was largely uninteresting boilerplate, and has been deprecated without replacement. For the few results of mathematical interest (those whose proofs are longer than a few lines), I've golfed their proofs as a stress test to ensure that this new API is capable of easily proving them. I've kept everything in the same file to minimize the diff. A future PR will move the obsolete material to `Deprecated.Hyperreal`. --- - [x] depends on: #33644 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) ready-to-merge t-algebra
label:t-algebra$
 387/96 Mathlib/Algebra/Order/Ring/StandardPart.lean,Mathlib/Analysis/Real/Hyperreal.lean 2 16 ['github-actions', 'j-loreaux', 'jcommelin', 'mathlib-bors', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'mathlib4-merge-conflict-bot', 'ocfnash', 'vihdzp', 'wwylele'] jcommelin
assignee:jcommelin
1-35027
1 day ago
1-39320
1 day ago
25-42656
25 days
35847 euprunin
author:euprunin
 chore: golf proofs This PR removes unused `have`/`haveI`/`let`/`letI` calls. The goal of this PR is to decrease the number of times lemmas are called explicitly (replacing calls to lemmas with calls to tactics). Any decrease in compilation time is a welcome side effect, although it is not a primary objective. Trace profiling results (differences <30 ms considered measurement noise): * `GenContFract.compExactValue_correctness_of_stream_eq_some`: unchanged πŸŽ‰ * `Finset.disjoint_range_addLeftEmbedding`: unchanged πŸŽ‰ * `CategoryTheory.ComposableArrows.IsComplex.epi_cokerToKer'`: unchanged πŸŽ‰ * `CategoryTheory.ComposableArrows.IsComplex.mono_cokerToKer'`: unchanged πŸŽ‰ * `ComplexShape.QFactorsThroughHomotopy_of_exists_prev`: unchanged πŸŽ‰ * `AlgebraicGeometry.IsAffineOpen.primeIdealOf_genericPoint`: unchanged πŸŽ‰ * `AlgebraicGeometry.functionField_isFractionRing_of_isAffineOpen`: unchanged πŸŽ‰ * `AlgebraicGeometry.smooth_of_grpObj_of_isAlgClosed`: 266 ms before, 232 ms after πŸŽ‰ * `AlgebraicGeometry.Scheme.ker_morphismRestrict_ideal`: 570 ms before, 538 ms after πŸŽ‰ * `AlgebraicGeometry.Scheme.IdealSheafData.isLocalization_away`: unchanged πŸŽ‰ * `AlgebraicGeometry.affineAnd_isLocal`: unchanged πŸŽ‰ * `AlgebraicGeometry.IsZariskiLocalAtTarget.of_iSup_eq_top`: unchanged πŸŽ‰ * `AlgebraicGeometry.HasAffineProperty.iff_of_isAffine`: unchanged πŸŽ‰ * `AlgebraicGeometry.isDominant_of_of_appTop_injective`: unchanged πŸŽ‰ * `AlgebraicGeometry.IsPreimmersion.SpecMap_iff`: unchanged πŸŽ‰ * `AlgebraicGeometry.quasiCompact_affineProperty_iff_quasiSeparatedSpace`: unchanged πŸŽ‰ Profiled using `set_option trace.profiler true in`. This PR is batched under the following guidelines: * Up to ~5 changed files per PR * Up to ~25 changed declarations per PR * Up to ~100 changed lines per PR --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) ready-to-merge 0/23 Mathlib/Algebra/ContinuedFractions/Computation/CorrectnessTerminating.lean,Mathlib/Algebra/Homology/ExactSequenceFour.lean,Mathlib/Algebra/Homology/Localization.lean,Mathlib/AlgebraicGeometry/FunctionField.lean,Mathlib/AlgebraicGeometry/Group/Smooth.lean,Mathlib/AlgebraicGeometry/IdealSheaf/Basic.lean,Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean,Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean,Mathlib/AlgebraicGeometry/Morphisms/Basic.lean,Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean,Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean,Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean 12 10 ['JovanGerb', 'euprunin', 'github-actions', 'leanprover-radar', 'mathlib-bors', 'riccardobrasca', 'vihdzp'] JovanGerb
assignee:JovanGerb
1-5200
1 day ago
1-7280
1 day ago
4-28700
4 days
34601 themathqueen
author:themathqueen
 feat(Combinatorics/SimpleGraph/AdjMatrix): adjacency matrix API --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-combinatorics large-import 117/19 Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean 1 21 ['b-mehta', 'eric-wieser', 'github-actions', 'mathlib-merge-conflicts', 'themathqueen'] kmill
assignee:kmill
15-72462
15 days ago
15-72522
15 days ago
33-26286
33 days
34624 homeowmorphism
author:homeowmorphism
 feat(GroupTheory/FreeGroup/Basic): surjection between types induces surjection between free groups on those types feat(GroupTheory/FreeGroup/Basic): adds the theorem that if `Ξ±` and `Ξ²` are arbitrary types and there is a surjection between them, then the induced FreeGroup.map is also surjective. This is a dependency of a larger PR to formalize finitely presented groups https://github.com/leanprover-community/mathlib4/pull/34236. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) new-contributor t-group-theory 14/3 Mathlib/GroupTheory/FreeGroup/Basic.lean 1 24 ['copilot-pull-request-reviewer', 'github-actions', 'homeowmorphism', 'mathlib-merge-conflicts', 'tb65536', 'vlad902'] riccardobrasca
assignee:riccardobrasca
2-14489
2 days ago
15-79415
15 days ago
26-75636
26 days
35974 justus-springer
author:justus-springer
 feat(Algebra/Polynomial/Bivariate): more API for swap --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebra maintainer-merge
label:t-algebra$
 10/0 Mathlib/Algebra/Polynomial/Bivariate.lean 1 2 ['github-actions', 'robin-carlier'] nobody
1-81496
1 day ago
1-81496
1 day ago
2-13491
2 days

Stale maintainer-merge'd PRs

Number Author Title Description Labels +/- Modified files (first 100) 📝 💬 All users who commented or reviewed Assignee(s) Updated Last status change total time in review
33832 alreadydone
author:alreadydone
 feat(Algebra): localization preserves unique factorization --- - [x] depends on: #33851 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-author t-algebra maintainer-merge
label:t-algebra$
 143/12 Mathlib.lean,Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean,Mathlib/Algebra/GroupWithZero/Associated.lean,Mathlib/GroupTheory/MonoidLocalization/Basic.lean,Mathlib/GroupTheory/MonoidLocalization/UniqueFactorization.lean,Mathlib/RingTheory/Localization/Defs.lean 6 11 ['Vierkantor', 'dagurtomas', 'github-actions', 'mathlib4-dependent-issues-bot'] Vierkantor
assignee:Vierkantor
26-82415
26 days ago
26-82419
26 days ago
17-27113
17 days
31141 peabrainiac
author:peabrainiac
 feat(Analysis/Calculus): parametric integrals over smooth functions are smooth Show that for any smooth function `f : H Γ— ℝ β†’ E`, the parametric integral `fun x ↦ ∫ t in a..b, f (x, t) βˆ‚ΞΌ` is smooth too. The argument proceeds inductively, using the fact that derivatives of parametric integrals can themselves be computed as parametric integrals. The necessary lemmas on derivatives of parametric integrals already existed, but took some work to apply due to their generality; we state some convenient special cases. --- - [x] depends on: #31077 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-author t-analysis maintainer-merge 470/12 Mathlib/Analysis/Calculus/ParametricIntegral.lean,Mathlib/Analysis/Calculus/ParametricIntervalIntegral.lean,Mathlib/MeasureTheory/Integral/DominatedConvergence.lean,Mathlib/Topology/NhdsWithin.lean,Mathlib/Topology/Separation/Regular.lean 5 36 ['fpvandoorn', 'github-actions', 'j-loreaux', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'peabrainiac', 'sgouezel'] j-loreaux
assignee:j-loreaux
21-17843
21 days ago
21-17843
21 days ago
33-85043
33 days
34193 bwangpj
author:bwangpj
 feat(Topology/Algebra/Ring): ContinuousAddEquiv.mulLeft, mulRight The additive homeomorphism from a topological ring to itself, induced by left/right multiplication by a unit. From FLT. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-topology maintainer-merge FLT 25/0 Mathlib/Topology/Algebra/Ring/Basic.lean 1 10 ['bwangpj', 'dagurtomas', 'eric-wieser', 'github-actions', 'riccardobrasca'] dagurtomas
assignee:dagurtomas
13-30709
13 days ago
19-81831
19 days ago
42-32857
42 days
35682 chenson2018
author:chenson2018
 chore(Computability/Partrec): remove `linter.flexible` exceptions This removes all `set_option linter.flexible false` from this module. Some proofs simply required moving around the usage of `simp`. For others I used `grind`, which is permitted to follow flexible tactics. In all cases I prioritized leaving the structure of the proof either mostly as-is or slightly improving readability. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-computability maintainer-merge 23/41 Mathlib/Computability/Partrec.lean 1 6 ['chenson2018', 'github-actions', 'grunweg'] nobody
8-63487
8 days ago
8-66149
8 days ago
8-86095
8 days
33364 BoltonBailey
author:BoltonBailey
 feat(Analysis/Convex/SimplicialComplex): add AbstractSimplicialComplex + constructions This adds the concept of [abstract simplicial complex](https://en.wikipedia.org/wiki/Abstract_simplicial_complex) (and refactors SimplicialComplex in terms of it). It also adds constructions that makes it easy to define a simplicial complex for any index family of points which is downward closed and which is affinely independent. I also include a construction of (abstract and geometric) simplicial complexes associated with a SimpleGraph, where vertices become 0-faces and edges become 1-faces, which could be useful later in defining the topological notion of a graph embedding. Co-authored-by: Claude Opus 4.5 --- - [x] depends on: #35115 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-analysis maintainer-merge t-algebraic-topology 440/16 Mathlib.lean,Mathlib/AlgebraicTopology/SimplicialComplex/Basic.lean,Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean,Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean,Mathlib/Data/Sym/Sym2.lean,Mathlib/LinearAlgebra/AffineSpace/Independent.lean,Mathlib/Order/UpperLower/Relative.lean,Mathlib/Tactic/Linter/DirectoryDependency.lean 8 30 ['BoltonBailey', 'denisgorod', 'eric-wieser', 'github-actions', 'j-loreaux', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'peabrainiac'] j-loreaux
assignee:j-loreaux
7-42813
7 days ago
8-1076
8 days ago
19-47887
19 days
33449 yuanyi-350
author:yuanyi-350
 feat(ProbabilityTheory): Add Poisson limit theorem --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-measure-probability maintainer-merge file-removed 127/3 Mathlib.lean,Mathlib/Probability/Distributions/Poisson/Basic.lean,Mathlib/Probability/Distributions/Poisson/PoissonLimitThm.lean,Mathlib/Probability/ProbabilityMassFunction/Binomial.lean,docs/1000.yaml 5 24 ['EtienneC30', 'github-actions', 'vihdzp'] EtienneC30
assignee:EtienneC30
5-84487
5 days ago
5-85595
5 days ago
62-14036
62 days
35081 tb65536
author:tb65536
 feat(Topology/Algebra/Group/Extension): define short exact sequence of topological groups This PR defines a short exact sequence of topological groups to be a closed embedding followed by an open quotient map (extracted from #32672). --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-topology maintainer-merge 57/0 Mathlib.lean,Mathlib/Topology/Algebra/Group/Extension.lean 2 3 ['dagurtomas', 'github-actions'] dagurtomas
assignee:dagurtomas
5-73571
5 days ago
5-73572
5 days ago
22-13708
22 days
35567 goliath-klein
author:goliath-klein
 refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): Golfs This PR cleans up the proofs in Analysis/Normed/Module/PiTensorProduct/{InjectiveSeminorm.lean, ProjectiveSeminorm.lean} In addition, it performs the following minor structural changes: * Weaken assumptions from `NontriviallyNormedField π•œ` to `NormedField π•œ` where possible * The proofs showing that `projectiveSeminorm` actually defines a `Seminorm` are split off into separate lemmas. This mimics the idiom used e.g. in `Analysis.Normed.Modula.Operator.Basic` to define the operator norm. * Register a `Nonempty x.lifts` instance in PiTensorProduct.lean, to avoid creating a half-dozen local instances. This is the first in a series of three PRs with the goal to [deprecate `PiTensorProuduct.injectiveSeminorm`](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/injectiveSeminorm/with/568798633). --- Co-authored-by: Davood H. T. Tehrani [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) new-contributor maintainer-merge 101/158 Mathlib/Analysis/Normed/Module/PiTensorProduct/InjectiveSeminorm.lean,Mathlib/Analysis/Normed/Module/PiTensorProduct/ProjectiveSeminorm.lean,Mathlib/LinearAlgebra/PiTensorProduct.lean 3 10 ['github-actions', 'goliath-klein', 'leanprover-radar', 'tb65536'] sgouezel
assignee:sgouezel
3-55164
3 days ago
12-4840
12 days ago
12-9188
12 days
35639 vihdzp
author:vihdzp
 chore(Order/SuccPred/Limit): use `to_dual` on everything that was missing --- - [x] depends on: #34882 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge 36/135 Mathlib/Data/Fintype/Card.lean,Mathlib/Order/Bounds/Basic.lean,Mathlib/Order/SuccPred/Limit.lean 3 4 ['JovanGerb', 'github-actions', 'mathlib-dependent-issues'] adamtopaz
assignee:adamtopaz
2-64283
2 days ago
2-64283
2 days ago
10-7219
10 days
32987 kim-em
author:kim-em
 feat: pipeline downloads and decompression in `cache get` This PR modifies `lake exe cache get` to decompress files as they download, rather than waiting for all downloads to complete first. Previously the cache system had two sequential phases: download all files using `curl --parallel`, then decompress all files using a single `leantar` call. Now a background task spawns sequential batched `leantar` calls to decompress files as downloads complete, pipelining network I/O and disk I/O. πŸ€– Prepared with Claude Code - [x] depends on: #34667 t-meta maintainer-merge 190/35 Cache/IO.lean,Cache/Requests.lean 2 65 ['Vierkantor', 'eric-wieser', 'github-actions', 'joneugster', 'kim-em', 'mathlib-dependent-issues', 'mathlib-merge-conflicts'] joneugster
assignee:joneugster
2-32209
2 days ago
5-20157
5 days ago
61-18829
61 days
35637 vihdzp
author:vihdzp
 chore(Topology/Order/LeftRight): use `to_dual` This overlaps with #35635, but the overlap is small (and that PR still needs some work, so I'd rather get this out of the way first). --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge 32/26 Mathlib/Order/Interval/Set/LinearOrder.lean,Mathlib/Tactic/Translate/ToDual.lean,Mathlib/Topology/Order/LeftRight.lean 3 8 ['JovanGerb', 'github-actions', 'vihdzp'] jcommelin
assignee:jcommelin
2-15548
2 days ago
2-15548
2 days ago
10-35557
10 days
35513 vihdzp
author:vihdzp
 refactor: redefine `Order.cof` for a preorder ... instead of using an unbundled relation. This makes it easier to work with, and avoids some `swap rᢜ` incantations. There are still a bunch of lemmas that make use of unbundled order relations; these will get fixed in follow-up PRs. --- - [x] depends on: #35517 - [x] depends on: #35519 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-order maintainer-merge t-set-theory 220/241 Mathlib/CategoryTheory/Presentable/IsCardinalFiltered.lean,Mathlib/Order/Cofinal.lean,Mathlib/SetTheory/Cardinal/Cofinality.lean 3 9 ['SnirBroshi', 'YaelDillies', 'github-actions', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'vihdzp'] b-mehta
assignee:b-mehta
1-62860
1 day ago
7-19819
7 days ago
8-38793
8 days
35850 vihdzp
author:vihdzp
 refactor: nicer definition for ordinal logarithm By leveraging the API on `Order.IsNormal`, we can define the ordinal logarithm in a way that more immediately proves the characterizing Galois connection. Note that this removes `Ordinal.log_def` and `Ordinal.succ_log_def` without deprecation - these are auxiliary results that should have been private and are tedious to re-prove. --- - [x] depends on: #35849 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-set-theory 40/69 Mathlib/SetTheory/Ordinal/Exponential.lean 1 8 ['YaelDillies', 'github-actions', 'mathlib-dependent-issues', 'vihdzp'] nobody
2-26967
2 days ago
2-33358
2 days ago
5-18176
5 days
26293 RemyDegenne
author:RemyDegenne
 feat: tightness from convergence of characteristic functions If the characteristic functions of a sequence of measures `ΞΌ : β„• β†’ Measure E` on a finite dimensional inner product space converge pointwise to a function which is continuous at 0, then `{ΞΌ n | n}` is tight. --- - [x] depends on: #24846 - [ ] depends on: #26292 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) --- *This PR continues the work from #24949.* *Original PR: https://github.com/leanprover-community/mathlib4/pull/24949* blocked-by-other-PR t-measure-probability 352/2 Mathlib.lean,Mathlib/MeasureTheory/Measure/TightCharFun.lean,Mathlib/MeasureTheory/Measure/TightNormed.lean 3 3 ['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] nobody
23-25778
23 days ago
23-26794
23 days ago
0-2
2 seconds
29996 vihdzp
author:vihdzp
 chore(Order/Concept): `IsIntent` and `IsExtent` We define predicates for a set to be an intent/extent, and use them to define alternate constructors for a concept. Using these, we golf the complete lattice instances. The fields `Concept.intent` and `Concept.extent` already existed, and these serve as unbundled versions of them. --- - [x] depends on: #30484 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-order maintainer-merge 161/114 Mathlib/Order/Concept.lean 1 50 ['Vierkantor', 'YaelDillies', 'github-actions', 'linesthatinterlace', 'mathlib-dependent-issues', 'mathlib4-merge-conflict-bot', 'plp127', 'vihdzp'] YaelDillies
assignee:YaelDillies
11-76463
11 days ago
12-35140
12 days ago
33-42666
33 days
28582 Thmoas-Guan
author:Thmoas-Guan
 feat(Data): some lemmas about WithBot ENat Add some lemma about withBot ENat discovered when dealing with `ringKrullDim` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-author t-data 58/10 Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean,Mathlib/Data/ENat/Basic.lean 2 37 ['Ruben-VandeVelde', 'Thmoas-Guan', 'YaelDillies', 'alreadydone', 'erdOne', 'github-actions', 'pechersky', 'urkud'] pechersky
assignee:pechersky
14-13719
14 days ago
25-18000
25 days ago
68-1211
68 days
35895 edegeltje
author:edegeltje
 feat(CategoryTheory/Topos/Classifier): subobject classifiers, isos and equivalences this PR adds `Classifier.ofEquivalence`, `Classifier.ofIso` and `Classifier.uniqueUpToIso`, as well as accompanying lemmas --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-category-theory 106/3 Mathlib/CategoryTheory/Topos/Classifier.lean 1 1 ['github-actions'] nobody
3-70709
3 days ago
3-72809
3 days ago
3-72864
3 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
33832 alreadydone
author:alreadydone
 feat(Algebra): localization preserves unique factorization --- - [x] depends on: #33851 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-author t-algebra maintainer-merge
label:t-algebra$
 143/12 Mathlib.lean,Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean,Mathlib/Algebra/GroupWithZero/Associated.lean,Mathlib/GroupTheory/MonoidLocalization/Basic.lean,Mathlib/GroupTheory/MonoidLocalization/UniqueFactorization.lean,Mathlib/RingTheory/Localization/Defs.lean 6 11 ['Vierkantor', 'dagurtomas', 'github-actions', 'mathlib4-dependent-issues-bot'] Vierkantor
assignee:Vierkantor
26-82415
26 days ago
26-82419
26 days ago
17-27113
17 days
31141 peabrainiac
author:peabrainiac
 feat(Analysis/Calculus): parametric integrals over smooth functions are smooth Show that for any smooth function `f : H Γ— ℝ β†’ E`, the parametric integral `fun x ↦ ∫ t in a..b, f (x, t) βˆ‚ΞΌ` is smooth too. The argument proceeds inductively, using the fact that derivatives of parametric integrals can themselves be computed as parametric integrals. The necessary lemmas on derivatives of parametric integrals already existed, but took some work to apply due to their generality; we state some convenient special cases. --- - [x] depends on: #31077 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-author t-analysis maintainer-merge 470/12 Mathlib/Analysis/Calculus/ParametricIntegral.lean,Mathlib/Analysis/Calculus/ParametricIntervalIntegral.lean,Mathlib/MeasureTheory/Integral/DominatedConvergence.lean,Mathlib/Topology/NhdsWithin.lean,Mathlib/Topology/Separation/Regular.lean 5 36 ['fpvandoorn', 'github-actions', 'j-loreaux', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'peabrainiac', 'sgouezel'] j-loreaux
assignee:j-loreaux
21-17843
21 days ago
21-17843
21 days ago
33-85043
33 days
34193 bwangpj
author:bwangpj
 feat(Topology/Algebra/Ring): ContinuousAddEquiv.mulLeft, mulRight The additive homeomorphism from a topological ring to itself, induced by left/right multiplication by a unit. From FLT. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-topology maintainer-merge FLT 25/0 Mathlib/Topology/Algebra/Ring/Basic.lean 1 10 ['bwangpj', 'dagurtomas', 'eric-wieser', 'github-actions', 'riccardobrasca'] dagurtomas
assignee:dagurtomas
13-30709
13 days ago
19-81831
19 days ago
42-32857
42 days
35682 chenson2018
author:chenson2018
 chore(Computability/Partrec): remove `linter.flexible` exceptions This removes all `set_option linter.flexible false` from this module. Some proofs simply required moving around the usage of `simp`. For others I used `grind`, which is permitted to follow flexible tactics. In all cases I prioritized leaving the structure of the proof either mostly as-is or slightly improving readability. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-computability maintainer-merge 23/41 Mathlib/Computability/Partrec.lean 1 6 ['chenson2018', 'github-actions', 'grunweg'] nobody
8-63487
8 days ago
8-66149
8 days ago
8-86095
8 days
33364 BoltonBailey
author:BoltonBailey
 feat(Analysis/Convex/SimplicialComplex): add AbstractSimplicialComplex + constructions This adds the concept of [abstract simplicial complex](https://en.wikipedia.org/wiki/Abstract_simplicial_complex) (and refactors SimplicialComplex in terms of it). It also adds constructions that makes it easy to define a simplicial complex for any index family of points which is downward closed and which is affinely independent. I also include a construction of (abstract and geometric) simplicial complexes associated with a SimpleGraph, where vertices become 0-faces and edges become 1-faces, which could be useful later in defining the topological notion of a graph embedding. Co-authored-by: Claude Opus 4.5 --- - [x] depends on: #35115 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-analysis maintainer-merge t-algebraic-topology 440/16 Mathlib.lean,Mathlib/AlgebraicTopology/SimplicialComplex/Basic.lean,Mathlib/Analysis/Convex/SimplicialComplex/AffineIndependentUnion.lean,Mathlib/Analysis/Convex/SimplicialComplex/Basic.lean,Mathlib/Data/Sym/Sym2.lean,Mathlib/LinearAlgebra/AffineSpace/Independent.lean,Mathlib/Order/UpperLower/Relative.lean,Mathlib/Tactic/Linter/DirectoryDependency.lean 8 30 ['BoltonBailey', 'denisgorod', 'eric-wieser', 'github-actions', 'j-loreaux', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'peabrainiac'] j-loreaux
assignee:j-loreaux
7-42813
7 days ago
8-1076
8 days ago
19-47887
19 days
33449 yuanyi-350
author:yuanyi-350
 feat(ProbabilityTheory): Add Poisson limit theorem --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-measure-probability maintainer-merge file-removed 127/3 Mathlib.lean,Mathlib/Probability/Distributions/Poisson/Basic.lean,Mathlib/Probability/Distributions/Poisson/PoissonLimitThm.lean,Mathlib/Probability/ProbabilityMassFunction/Binomial.lean,docs/1000.yaml 5 24 ['EtienneC30', 'github-actions', 'vihdzp'] EtienneC30
assignee:EtienneC30
5-84487
5 days ago
5-85595
5 days ago
62-14036
62 days
35081 tb65536
author:tb65536
 feat(Topology/Algebra/Group/Extension): define short exact sequence of topological groups This PR defines a short exact sequence of topological groups to be a closed embedding followed by an open quotient map (extracted from #32672). --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-topology maintainer-merge 57/0 Mathlib.lean,Mathlib/Topology/Algebra/Group/Extension.lean 2 3 ['dagurtomas', 'github-actions'] dagurtomas
assignee:dagurtomas
5-73571
5 days ago
5-73572
5 days ago
22-13708
22 days
35567 goliath-klein
author:goliath-klein
 refactor(PiTensorProduct/{InjectiveNorm, ProjectiveNorm}): Golfs This PR cleans up the proofs in Analysis/Normed/Module/PiTensorProduct/{InjectiveSeminorm.lean, ProjectiveSeminorm.lean} In addition, it performs the following minor structural changes: * Weaken assumptions from `NontriviallyNormedField π•œ` to `NormedField π•œ` where possible * The proofs showing that `projectiveSeminorm` actually defines a `Seminorm` are split off into separate lemmas. This mimics the idiom used e.g. in `Analysis.Normed.Modula.Operator.Basic` to define the operator norm. * Register a `Nonempty x.lifts` instance in PiTensorProduct.lean, to avoid creating a half-dozen local instances. This is the first in a series of three PRs with the goal to [deprecate `PiTensorProuduct.injectiveSeminorm`](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/injectiveSeminorm/with/568798633). --- Co-authored-by: Davood H. T. Tehrani [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) new-contributor maintainer-merge 101/158 Mathlib/Analysis/Normed/Module/PiTensorProduct/InjectiveSeminorm.lean,Mathlib/Analysis/Normed/Module/PiTensorProduct/ProjectiveSeminorm.lean,Mathlib/LinearAlgebra/PiTensorProduct.lean 3 10 ['github-actions', 'goliath-klein', 'leanprover-radar', 'tb65536'] sgouezel
assignee:sgouezel
3-55164
3 days ago
12-4840
12 days ago
12-9188
12 days
35639 vihdzp
author:vihdzp
 chore(Order/SuccPred/Limit): use `to_dual` on everything that was missing --- - [x] depends on: #34882 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge 36/135 Mathlib/Data/Fintype/Card.lean,Mathlib/Order/Bounds/Basic.lean,Mathlib/Order/SuccPred/Limit.lean 3 4 ['JovanGerb', 'github-actions', 'mathlib-dependent-issues'] adamtopaz
assignee:adamtopaz
2-64283
2 days ago
2-64283
2 days ago
10-7219
10 days
32987 kim-em
author:kim-em
 feat: pipeline downloads and decompression in `cache get` This PR modifies `lake exe cache get` to decompress files as they download, rather than waiting for all downloads to complete first. Previously the cache system had two sequential phases: download all files using `curl --parallel`, then decompress all files using a single `leantar` call. Now a background task spawns sequential batched `leantar` calls to decompress files as downloads complete, pipelining network I/O and disk I/O. πŸ€– Prepared with Claude Code - [x] depends on: #34667 t-meta maintainer-merge 190/35 Cache/IO.lean,Cache/Requests.lean 2 65 ['Vierkantor', 'eric-wieser', 'github-actions', 'joneugster', 'kim-em', 'mathlib-dependent-issues', 'mathlib-merge-conflicts'] joneugster
assignee:joneugster
2-32209
2 days ago
5-20157
5 days ago
61-18829
61 days
35637 vihdzp
author:vihdzp
 chore(Topology/Order/LeftRight): use `to_dual` This overlaps with #35635, but the overlap is small (and that PR still needs some work, so I'd rather get this out of the way first). --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge 32/26 Mathlib/Order/Interval/Set/LinearOrder.lean,Mathlib/Tactic/Translate/ToDual.lean,Mathlib/Topology/Order/LeftRight.lean 3 8 ['JovanGerb', 'github-actions', 'vihdzp'] jcommelin
assignee:jcommelin
2-15548
2 days ago
2-15548
2 days ago
10-35557
10 days
35513 vihdzp
author:vihdzp
 refactor: redefine `Order.cof` for a preorder ... instead of using an unbundled relation. This makes it easier to work with, and avoids some `swap rᢜ` incantations. There are still a bunch of lemmas that make use of unbundled order relations; these will get fixed in follow-up PRs. --- - [x] depends on: #35517 - [x] depends on: #35519 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-order maintainer-merge t-set-theory 220/241 Mathlib/CategoryTheory/Presentable/IsCardinalFiltered.lean,Mathlib/Order/Cofinal.lean,Mathlib/SetTheory/Cardinal/Cofinality.lean 3 9 ['SnirBroshi', 'YaelDillies', 'github-actions', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'vihdzp'] b-mehta
assignee:b-mehta
1-62860
1 day ago
7-19819
7 days ago
8-38793
8 days
32245 erdOne
author:erdOne
 feat(RingTheory): the `coassoc_simps` simp set From Toric Co-authored-by: YaΓ«l Dillies --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-meta maintainer-merge toric t-ring-theory 815/0 Mathlib.lean,Mathlib/RingTheory/Coalgebra/CoassocSimps.lean,Mathlib/Tactic/Attr/Register.lean,MathlibTest/RingTheory/CoassocSimps.lean 4 22 ['erdOne', 'github-actions', 'joneugster', 'riccardobrasca'] b-mehta, joneugster, mattrobball
assignee:joneugster assignee:b-mehta assignee:mattrobball
0-80252
22 hours ago
5-10924
5 days ago
36-62266
36 days
35331 SnirBroshi
author:SnirBroshi
 feat(SimpleGraph/Subgraph): small things about `spanningCoe` and a small golf --- Three unrelated things in the same file, each too small to be its own PR. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-combinatorics maintainer-merge 13/4 Mathlib/Combinatorics/SimpleGraph/Subgraph.lean 1 3 ['YaelDillies', 'github-actions'] YaelDillies
assignee:YaelDillies
0-71375
19 hours ago
1-3859
1 day ago
17-53355
17 days
34881 CBirkbeck
author:CBirkbeck
 feat(ModularForm/NumberTheory/Delta): Define the delta function We define the Delta function on the upper half plane and show how it transforms under the slash operator, this is in preparation to proving it is a modular form. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-number-theory maintainer-merge 251/0 Mathlib.lean,Mathlib/Analysis/Complex/SqrtDeriv.lean,Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean,Mathlib/Analysis/RCLike/Sqrt.lean,Mathlib/NumberTheory/ModularForms/Delta.lean,Mathlib/Topology/Algebra/InfiniteSum/Basic.lean 6 50 ['CBirkbeck', 'faenuccio', 'github-actions', 'joneugster', 'loefflerd'] faenuccio and loefflerd
assignee:loefflerd assignee:faenuccio
0-22883
6 hours ago
1-22910
1 day ago
12-66361
12 days
35850 vihdzp
author:vihdzp
 refactor: nicer definition for ordinal logarithm By leveraging the API on `Order.IsNormal`, we can define the ordinal logarithm in a way that more immediately proves the characterizing Galois connection. Note that this removes `Ordinal.log_def` and `Ordinal.succ_log_def` without deprecation - these are auxiliary results that should have been private and are tedious to re-prove. --- - [x] depends on: #35849 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-set-theory 40/69 Mathlib/SetTheory/Ordinal/Exponential.lean 1 8 ['YaelDillies', 'github-actions', 'mathlib-dependent-issues', 'vihdzp'] nobody
2-26967
2 days ago
2-33358
2 days ago
5-18176
5 days
26293 RemyDegenne
author:RemyDegenne
 feat: tightness from convergence of characteristic functions If the characteristic functions of a sequence of measures `ΞΌ : β„• β†’ Measure E` on a finite dimensional inner product space converge pointwise to a function which is continuous at 0, then `{ΞΌ n | n}` is tight. --- - [x] depends on: #24846 - [ ] depends on: #26292 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) --- *This PR continues the work from #24949.* *Original PR: https://github.com/leanprover-community/mathlib4/pull/24949* blocked-by-other-PR t-measure-probability 352/2 Mathlib.lean,Mathlib/MeasureTheory/Measure/TightCharFun.lean,Mathlib/MeasureTheory/Measure/TightNormed.lean 3 3 ['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] nobody
23-25778
23 days ago
23-26794
23 days ago
0-2
2 seconds
29996 vihdzp
author:vihdzp
 chore(Order/Concept): `IsIntent` and `IsExtent` We define predicates for a set to be an intent/extent, and use them to define alternate constructors for a concept. Using these, we golf the complete lattice instances. The fields `Concept.intent` and `Concept.extent` already existed, and these serve as unbundled versions of them. --- - [x] depends on: #30484 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-order maintainer-merge 161/114 Mathlib/Order/Concept.lean 1 50 ['Vierkantor', 'YaelDillies', 'github-actions', 'linesthatinterlace', 'mathlib-dependent-issues', 'mathlib4-merge-conflict-bot', 'plp127', 'vihdzp'] YaelDillies
assignee:YaelDillies
11-76463
11 days ago
12-35140
12 days ago
33-42666
33 days
36013 pfaffelh
author:pfaffelh
 feat(Topology/Compactness/CompactSystem): introduce compact Systems A compact system is a set systems with the property that, whenever a countable intersections of sets in the set system is empty, there is a finite subset of sets with empty intersection. These are needed e.g. in measure theory if one wants to show sigma-additivity of a set function on a ring. Main result: The set of sets which are either compact and closed, or univ, is a compact system. Co-authored-by: RΓ©my Degenne [remydegenne@gmail.com](mailto:remydegenne@gmail.com) --- Continues work from #25899 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) 238/0 Mathlib.lean,Mathlib/Data/Set/Dissipate.lean,Mathlib/MeasureTheory/PiSystem.lean,Mathlib/Topology/Compactness/CompactSystem.lean 4 1 ['github-actions'] nobody
0-24124
6 hours ago
1-22565
1 day ago
1-58304
1 day
35233 kim-em
author:kim-em
 chore: lake shake --add-public --keep-implied --keep-prefix --fix This PR runs `lake shake --add-public --keep-implied --keep-prefix --fix` again after https://github.com/leanprover-community/mathlib4/pull/34511, picking up the remaining 28 files that now have suggestions. πŸ€– Prepared with Claude Code awaiting-author maintainer-merge large-import 13/12 Mathlib/Algebra/Category/ModuleCat/Sheaf/Quasicoherent.lean,Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean,Mathlib/Data/Nat/Init.lean,Mathlib/LinearAlgebra/Matrix/Kronecker.lean,Mathlib/LinearAlgebra/TensorProduct/Basic.lean,Mathlib/LinearAlgebra/TensorProduct/Defs.lean,Mathlib/LinearAlgebra/TensorProduct/Map.lean,Mathlib/Logic/Basic.lean,Mathlib/Logic/Relation.lean,Mathlib/RingTheory/MatrixAlgebra.lean,Mathlib/Tactic/Hint.lean,Mathlib/Tactic/Linter/FindDeprecations.lean,Mathlib/Tactic/Nontriviality/Core.lean,Mathlib/Tactic/NormNum/Result.lean,Mathlib/Tactic/Order/CollectFacts.lean,Mathlib/Tactic/Tauto.lean 16 16 ['TwoFX', 'Vierkantor', 'adomani', 'bryangingechen', 'github-actions', 'joneugster', 'kim-em', 'mathlib-merge-conflicts', 'mathlib-splicebot'] nobody
0-9935
2 hours ago
0-16884
4 hours ago
11-83992
11 days
36068 justus-springer
author:justus-springer
 feat(RingTheory/Polynomial/GaussLemma): `mem_lifts` lemma for primitive polynomials A lemma that's needed for the proof of LΓΌroth's theorem. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-ring-theory 24/0 Mathlib/RingTheory/Polynomial/GaussLemma.lean 1 6 ['erdOne', 'github-actions', 'robin-carlier'] nobody
0-7425
2 hours ago
0-7425
2 hours ago
0-86139
23 hours
28582 Thmoas-Guan
author:Thmoas-Guan
 feat(Data): some lemmas about WithBot ENat Add some lemma about withBot ENat discovered when dealing with `ringKrullDim` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-author t-data 58/10 Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean,Mathlib/Data/ENat/Basic.lean 2 37 ['Ruben-VandeVelde', 'Thmoas-Guan', 'YaelDillies', 'alreadydone', 'erdOne', 'github-actions', 'pechersky', 'urkud'] pechersky
assignee:pechersky
14-13719
14 days ago
25-18000
25 days ago
68-1211
68 days
36130 vbeffara
author:vbeffara
 feat(Combinatorics/SimpleGraphs): generalize SimpleGraph.map to any function The point is to be able to use map to define graph contractions. Added the injectivity assumption where needed. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) easy t-combinatorics new-contributor maintainer-merge 40/32 Mathlib/Combinatorics/SimpleGraph/Clique.lean,Mathlib/Combinatorics/SimpleGraph/Coloring.lean,Mathlib/Combinatorics/SimpleGraph/Maps.lean,Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean 4 7 ['YaelDillies', 'b-mehta', 'github-actions', 'vbeffara'] nobody
0-2976
49 minutes ago
0-4144
1 hour ago
0-13176
3 hours
35895 edegeltje
author:edegeltje
 feat(CategoryTheory/Topos/Classifier): subobject classifiers, isos and equivalences this PR adds `Classifier.ofEquivalence`, `Classifier.ofIso` and `Classifier.uniqueUpToIso`, as well as accompanying lemmas --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-category-theory 106/3 Mathlib/CategoryTheory/Topos/Classifier.lean 1 1 ['github-actions'] nobody
3-70709
3 days ago
3-72809
3 days ago
3-72864
3 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 FR-vdash-bot
author:FR-vdash-bot
 feat(Algebra/Order/GroupWithZero/Unbundled): add some lemmas Some lemmas in `Algebra.Order.GroupWithZero.Unbundled` have incorrect or unsatisfactory names, or assumptions that can be omitted using `ZeroLEOneClass`. The lemmas added in this PR are versions of existing lemmas that use the correct or better name or `ZeroLEOneClass` to omit an assumption. The original lemmas will be deprecated in #17593. | New name | Old name | |-------------------------|-------------------------| | `mul_le_one_leftβ‚€` | `Left.mul_le_one_of_le_of_le` | | `mul_lt_one_of_le_of_lt_leftβ‚€` (`0 ≀ Β·` version) / `mul_lt_one_of_le_of_lt_of_pos_left` | `Left.mul_lt_of_le_of_lt_one_of_pos` | | `mul_lt_one_of_lt_of_le_leftβ‚€` | `Left.mul_lt_of_lt_of_le_one_of_nonneg` | | `mul_le_one_rightβ‚€` | `Right.mul_le_one_of_le_of_le` | | `mul_lt_one_of_lt_of_le_rightβ‚€` (`0 ≀ Β·` version) / `mul_lt_one_of_lt_of_le_of_pos_right` | `Right.mul_lt_one_of_lt_of_le_of_pos` | | `mul_lt_one_of_le_of_lt_rightβ‚€` | `Right.mul_lt_one_of_le_of_lt_of_nonneg` | The following lemmas use `ZeroLEOneClass`. | New name | Old name | |-------------------------|-------------------------| | `(Left.)one_le_mulβ‚€` | `Left.one_le_mul_of_le_of_le` | | `Left.one_lt_mul_of_le_of_ltβ‚€` | `Left.one_lt_mul_of_le_of_lt_of_pos` | | `Left.one_lt_mul_of_lt_of_leβ‚€` | `Left.lt_mul_of_lt_of_one_le_of_nonneg` / `one_lt_mul_of_lt_of_le` (still there) | | `(Left.)one_lt_mulβ‚€` | | | `Right.one_le_mulβ‚€` | `Right.one_le_mul_of_le_of_le` | | `Right.one_lt_mul_of_lt_of_leβ‚€` | `Right.one_lt_mul_of_lt_of_le_of_pos` | | `Right.one_lt_mul_of_le_of_ltβ‚€` | `Right.one_lt_mul_of_le_of_lt_of_nonneg` / `one_lt_mul_of_le_of_lt` (still there) / `one_lt_mul` (still there) | | `Right.one_lt_mulβ‚€` | `Right.one_lt_mul_of_lt_of_lt` | --- Split from #17593. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) merge-conflict t-algebra t-order awaiting-zulip
label:t-algebra$
 146/44 Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean 2 11 ['FR-vdash-bot', 'YaelDillies', 'github-actions', 'j-loreaux'] nobody
469-14665
1 year ago
469-14665
1 year ago
0-0
0 seconds
8370 eric-wieser
author:eric-wieser
 refactor(Analysis/NormedSpace/Exponential): remove the `𝕂` argument from `exp` This argument is still needed for almost all the lemmas, which means it can longer be found by unification. We keep around `expSeries 𝕂 A`, as it's needed for talking about the radius of convergence over different base fields. This is a prerequisite for #8372, as we can't merge the functions until they have the same interface.\ Zulip thread: [#mathlib4 > Real.exp @ πŸ’¬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Real.2Eexp/near/401602245) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) This is started from the mathport output on https://github.com/leanprover-community/mathlib/pull/19244 merge-conflict t-analysis awaiting-zulip 432/387 Mathlib/Analysis/CStarAlgebra/Exponential.lean,Mathlib/Analysis/CStarAlgebra/Spectrum.lean,Mathlib/Analysis/Normed/Algebra/Exponential.lean,Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean,Mathlib/Analysis/Normed/Algebra/QuaternionExponential.lean,Mathlib/Analysis/Normed/Algebra/Spectrum.lean,Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean,Mathlib/Analysis/NormedSpace/DualNumber.lean,Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean,Mathlib/Analysis/SpecialFunctions/Exponential.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Series.lean 11 29 ['YaelDillies', 'eric-wieser', 'girving', 'github-actions', 'j-loreaux', 'kbuzzard', 'leanprover-community-bot-assistant', 'urkud'] nobody
313-56442
10 months ago
324-85072
10 months ago
0-0
0 seconds
15654 TpmKranz
author:TpmKranz
 feat(Computability): language-preserving maps between NFA and RE Map REs to NFAs via Thompson's construction and NFAs to REs using GNFAs Last chunk of #12648 --- - [ ] depends on: #15651 - [ ] depends on: #15649 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) blocked-by-other-PR merge-conflict new-contributor t-computability awaiting-zulip 985/2 Mathlib.lean,Mathlib/Computability/GNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean,Mathlib/Computability/RegularExpressions.lean,Mathlib/Data/FinEnum/Option.lean,docs/references.bib 7 3 ['github-actions', 'leanprover-community-mathlib4-bot', 'meithecatte'] nobody
302-64342
9 months ago
302-64347
9 months ago
0-0
0 seconds
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
242-44691
7 months ago
242-44691
7 months ago
0-0
0 seconds
25218 kckennylau
author:kckennylau
 feat(AlgebraicGeometry): Tate normal form of elliptic curves --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) merge-conflict t-algebraic-geometry new-contributor awaiting-zulip 291/26 Mathlib.lean,Mathlib/AlgebraicGeometry/EllipticCurve/IsomOfJ.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Modular/TateNormalForm.lean,Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean,Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean 5 31 ['MichaelStollBayreuth', 'Multramate', 'acmepjz', 'github-actions', 'grunweg', 'kckennylau', 'leanprover-community-bot-assistant'] nobody
242-43529
7 months ago
242-43530
7 months ago
0-0
0 seconds
28803 astrainfinita
author:astrainfinita
 refactor: unbundle algebra from `ENormed*` Further speed up the search in the algebraic typeclass hierarchy by avoiding searching for `TopologicalSpace`. This PR continues the work from #23961. - Change `ESeminormed(Add)Monoid` and `ENormed(Add)Monoid` so they no longer carry algebraic data. - Deprecate `ESeminormed(Add)CommMonoid` and `ENormed(Add)CommMonoid` in favor of `ESeminormed(Add)Monoid` and `ENormed(Add)Monoid` with a commutative algebraic typeclass. |Old|New| |---|---| | `[ESeminormed(Add)(Comm)Monoid E]` | `[(Add)(Comm)Monoid E] [ESeminormed(Add)Monoid E]` | | `[ENormed(Add)(Comm)Monoid]` | `[(Add)(Comm)Monoid E] [ENormed(Add)Monoid]` | See [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2328803.20refactor.3A.20unbundle.20algebra.20from.20.60ENormed*.60/with/536024350) ------------ - [x] depends on: #28813 merge-conflict t-analysis t-algebra slow-typeclass-synthesis awaiting-zulip
label:t-algebra$
 80/63 Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/Analysis/Normed/Group/Continuity.lean,Mathlib/Analysis/Normed/Group/InfiniteSum.lean,Mathlib/Analysis/NormedSpace/IndicatorFunction.lean,Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean,Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean,Mathlib/MeasureTheory/Function/L1Space/Integrable.lean,Mathlib/MeasureTheory/Function/LocallyIntegrable.lean,Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean,Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean,Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean,Mathlib/MeasureTheory/Integral/IntegrableOn.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean 14 28 ['astrainfinita', 'bryangingechen', 'github-actions', 'grunweg', 'kbuzzard', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib-bors', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'sgouezel'] grunweg
assignee:grunweg
182-59174
6 months ago
182-59175
6 months ago
0-20585
5 hours
28925 grunweg
author:grunweg
 chore: remove `linear_combination'` tactic When `linear_combination` was refactored in #15899, the old code was kept as the `linear_combination'` tactic, for easier migration. The consensus of the zulip discussion ([#mathlib4 > Narrowing the scope of `linear_combination` @ πŸ’¬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Narrowing.20the.20scope.20of.20.60linear_combination.60/near/470237816)) was to wait, and "revisit this once people have experienced the various tactics in practice". One year later, the old tactic has almost no uses: it is unused in mathlib; [searching on github](https://github.com/search?q=linear_combination%27%20path%3A*.lean&type=code) yields 37 hits --- all of which are in various forks of mathlib. Thus, removing this tactic seems appropriate. --- Do not merge before the zulip discussion has concluded! [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) merge-conflict awaiting-zulip file-removed 0/564 Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/LinearCombination'.lean,Mathlib/Tactic/Linter/UnusedTactic.lean,MathlibTest/linear_combination'.lean 5 4 ['euprunin', 'github-actions', 'grunweg', 'mathlib4-merge-conflict-bot'] nobody
139-36384
4 months ago
139-36385
4 months 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/) merge-conflict t-meta t-category-theory new-contributor awaiting-zulip large-import 444/125 Mathlib/CategoryTheory/Monoidal/Category.lean,Mathlib/CategoryTheory/Monoidal/Discrete.lean,Mathlib/Tactic/ToAdditive/GuessName.lean 3 22 ['JovanGerb', 'YaelDillies', 'github-actions', 'imbrem', 'mathlib4-merge-conflict-bot'] nobody
111-47258
3 months ago
111-47258
3 months ago
1-18384
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/) awaiting-author merge-conflict new-contributor t-computability awaiting-zulip 307/5 Mathlib/Computability/NFA.lean 1 27 ['TpmKranz', 'YaelDillies', 'dupuisf', 'github-actions', 'leanprover-community-bot-assistant', 'meithecatte', 'rudynicolop'] nobody
106-64390
3 months ago
289-549
9 months ago
0-0
0 seconds
15649 TpmKranz
author:TpmKranz
 feat(Computability): introduce Generalised NFA as bridge to Regular Expression Lays the groundwork for a proof of equivalence of NFA and RE, w.r.t. described language. Actual connection to NFA comes later, after the groundwork for the opposite direction has been laid. Second chunk of #12648 --- - [x] depends on: #15647 [Data.FinEnum.Option unchanged since then] [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-author merge-conflict new-contributor t-computability awaiting-zulip 298/0 Mathlib.lean,Mathlib/Computability/GNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/RegularExpressions.lean,docs/references.bib 5 7 ['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'meithecatte', 'trivial1711'] nobody
105-80631
3 months ago
105-80632
3 months ago
0-0
0 seconds
20648 anthonyde
author:anthonyde
 feat: formalize regular expression -> Ξ΅NFA The file `Computability/RegularExpressionsToEpsilonNFA.lean` contains a formal definition of Thompson's method for constructing an `Ξ΅NFA` from a `RegularExpression` and a proof of its correctness. --- - [x] depends on: #20644 - [x] depends on: #20645 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) merge-conflict new-contributor t-computability awaiting-zulip 490/0 Mathlib.lean,Mathlib/Computability/RegularExpressionsToEpsilonNFA.lean,docs/references.bib 3 7 ['anthonyde', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'meithecatte', 'qawbecrdtey'] nobody
105-31399
3 months ago
105-31400
3 months ago
0-0
0 seconds
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
105-3265
3 months ago
534-63390
1 year ago
0-0
0 seconds
30668 astrainfinita
author:astrainfinita
 feat: `QuotType` This typeclass is primarily for use by type synonyms of `Quot` and `Quotient`. Using `QuotType` API for type synonyms of `Quot` and `Quotient` will avoid defeq abuse caused by directly using `Quot` and `Quotient` APIs. This PR also adds some typeclasses to support different ways to find the quotient map that should be used. See the documentation comments of these typeclasses for examples of usage. --- It's not a typical design to use these auxiliary typeclasses and term elaborators, but I haven't found a better way to support these notations. Some of the naming may need to be discussed. For example: - `⟦·⟧` is currently called `mkQ` in names. This distinguishes it from other `.mk`s and makes it possible to write the quotient map as `mkQ` `mkQ'` ~~`mkQ_ h`~~. But this will also require changing the old lemma names. - It would be helpful if the names of new type classes explained their functionality better. [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/migrate.20to.20.60QuotLike.60.20API) This PR continues the work from #16421. Original PR: https://github.com/leanprover-community/mathlib4/pull/16421 RFC awaiting-zulip t-data 629/0 Mathlib.lean,Mathlib/Data/QuotType.lean,MathlibTest/QuotType.lean 3 20 ['YaelDillies', 'astrainfinita', 'github-actions', 'mathlib4-merge-conflict-bot', 'plp127', 'vihdzp'] nobody
83-71511
2 months ago
84-16577
2 months 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/) merge-conflict t-analysis awaiting-zulip 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
56-39824
1 month ago
56-39825
1 month ago
8-31111
8 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/) t-algebra awaiting-zulip
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
41-2259
1 month ago
41-2259
1 month ago
40-42357
40 days
34396 dupuisf
author:dupuisf
 feat: notation for `Ring.inverse` This PR adds the global notation `x⁻¹ʳ` for `Ring.inverse x`, and a few extra API lemmas about it. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebra awaiting-zulip
label:t-algebra$
 58/19 Mathlib/Algebra/GroupWithZero/Units/Basic.lean 1 1 ['github-actions'] nobody
38-41690
1 month ago
38-41707
1 month ago
0-1
1 second
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
34-7077
1 month ago
34-7077
1 month ago
42-25715
42 days
34656 vihdzp
author:vihdzp
 refactor: review `exists_irreducible_of_degree_pos` theorems This PR does the following: - Rename `exists_irreducible_of_degree_pos` to `exists_irreducible_dvd_of_degree_pos`. The previous name reads as if this were proving that an irreducible polynomial of any positive degree exists. - Deprecate variants which differ only in the spelling of `0 < f.degree`. We already have quite a lot of API for converting between `natDegree` and `degree`, and we should just use that instead. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebra awaiting-zulip t-ring-theory
label:t-algebra$
 9/4 Mathlib/RingTheory/Polynomial/UniqueFactorization.lean 1 4 ['github-actions', 'tb65536', 'vihdzp'] nobody
31-29143
1 month ago
31-29143
1 month ago
0-49595
13 hours
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/) t-algebra new-contributor awaiting-zulip
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'] dagurtomas
assignee:dagurtomas
31-19682
1 month ago
31-19682
1 month ago
10-66980
10 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/) t-measure-probability new-contributor awaiting-zulip 4/0 Mathlib/MeasureTheory/Constructions/Polish/Basic.lean 1 9 ['ADedecker', 'LTolDe', 'dupuisf', 'github-actions', 'jcommelin'] PatrickMassot
assignee:PatrickMassot
31-19487
1 month ago
31-19487
1 month ago
25-83455
25 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/) awaiting-zulip t-ring-theory 844/0 Mathlib.lean,Mathlib/RingTheory/PowerSeries/Composition.lean 2 3 ['Paul-Lez', 'github-actions', 'vihdzp'] nobody
22-65496
22 days ago
22-65496
22 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/) merge-conflict t-algebra awaiting-zulip
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
14-37835
14 days ago
14-37835
14 days ago
7-54145
7 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/) awaiting-zulip t-data 82/4 Mathlib/Analysis/Real/Cardinality.lean,Mathlib/Data/Set/Countable.lean,Mathlib/SetTheory/Cardinal/Basic.lean 3 16 ['github-actions', 'joneugster', 'staroperator', 'vihdzp'] joneugster
assignee:joneugster
14-33501
14 days ago
14-33501
14 days ago
12-21583
12 days
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 25 ['alreadydone', 'github-actions', 'kbuzzard', 'leanprover-radar'] jcommelin
assignee:jcommelin
14-31586
14 days ago
14-31586
14 days ago
4-19293
4 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/) awaiting-author t-linter awaiting-zulip 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
14-30261
14 days ago
14-30359
14 days ago
66-73556
66 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 23/2 Mathlib/Tactic/Linter/TextBased.lean 1 4 ['github-actions', 'grunweg', 'joneugster', 'vihdzp'] nobody
12-880
12 days ago
13-23115
13 days ago
0-3845
1 hour
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/) awaiting-zulip t-data 10/10 Mathlib/Control/Monad/Cont.lean,Mathlib/Control/Monad/Writer.lean 2 4 ['Shreyas4991', 'eric-wieser', 'github-actions'] nobody
11-65794
11 days ago
11-65795
11 days ago
0-18707
5 hours
33972 YuvalFilmus
author:YuvalFilmus
 feat(Analysis/Polynomial/Order): polynomial has fixed sign beyond largest root We prove that a polynomial has fixed sign beyond its largest root. One could also prove similar results about the smallest root, but they will be more awkward since they will depend on the parity of the (natural) degree;Β suggestions welcome (perhaps for a future PR). --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-analysis awaiting-zulip 134/0 Mathlib.lean,Mathlib/Analysis/Polynomial/Order.lean 2 13 ['YuvalFilmus', 'artie2000', 'github-actions', 'mathlib-merge-conflicts', 'urkud', 'vihdzp'] ADedecker and urkud
assignee:urkud assignee:ADedecker
8-84440
8 days ago
9-26
9 days ago
39-75082
39 days
20238 maemre
author:maemre
 feat(Computability/DFA): Closure of regular languages under some set operations This shows that regular languages are closed under complement and intersection by constructing DFAs for them. --- Closure under all other operations will be proved when someone adds the proof for DFA<->regular expression equivalence, so they are not part of this PR. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-author merge-conflict new-contributor t-computability awaiting-zulip 159/0 Mathlib/Computability/DFA.lean,Mathlib/Computability/Language.lean 2 60 ['EtienneC30', 'YaelDillies', 'github-actions', 'maemre', 'mathlib4-merge-conflict-bot', 'meithecatte', 'urkud'] nobody
6-24633
6 days ago
105-79722
3 months ago
0-0
0 seconds
22361 rudynicolop
author:rudynicolop
 feat(Computability/NFA): nfa closure properties Add the closure properties union, intersection and reversal for NFA. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-author merge-conflict new-contributor t-computability awaiting-zulip 218/2 Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean 2 91 ['EtienneC30', 'b-mehta', 'ctchou', 'github-actions', 'leanprover-community-bot-assistant', 'meithecatte', 'rudynicolop'] nobody
6-24617
6 days ago
288-86024
9 months ago
0-0
0 seconds
23929 meithecatte
author:meithecatte
 feat(Computability/NFA): improve bound on pumping lemma --- - [x] depends on: #25321 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) awaiting-author new-contributor t-computability awaiting-zulip 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
5-44646
5 days ago
5-44646
5 days ago
0-0
0 seconds
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/) awaiting-author merge-conflict t-differential-geometry t-analysis awaiting-zulip 221/218 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/VectorField.lean,Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean,Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/InverseDeriv.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/Instances/Sphere.lean,Mathlib/Geometry/Manifold/Instances/UnitsOfNormedAlgebra.lean,Mathlib/Geometry/Manifold/IsManifold/Basic.lean,Mathlib/Geometry/Manifold/VectorBundle/Basic.lean,Mathlib/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean 28 5 ['github-actions', 'j-loreaux', 'mathlib-merge-conflicts', 'peabrainiac'] sgouezel
assignee:sgouezel
2-76585
2 days ago
14-36510
14 days ago
8-6287
8 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/) awaiting-author awaiting-zulip t-data 162/0 Mathlib/Data/Quot.lean,Mathlib/Data/Set/Image.lean,Mathlib/Data/SetLike/Basic.lean,Mathlib/Data/Setoid/Basic.lean 4 5 ['SnirBroshi', 'TwoFX', 'eric-wieser', 'github-actions', 'mathlib-merge-conflicts'] TwoFX
assignee:TwoFX
1-26847
1 day ago
1-26847
1 day ago
36-69524
36 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
35552 vihdzp
author:vihdzp
 chore(SetTheory/Ordinal/Basic): remove `backward.privateInPublic` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) tech debt t-set-theory 7/27 Mathlib/SetTheory/Ordinal/Basic.lean 1 1 ['github-actions'] nobody
5-27832
5 days ago
5-27945
5 days ago
12-58372
12 days
35878 Parcly-Taxel
author:Parcly-Taxel
 chore: use `induction` for `Quotient.induction` invocations Found through the regex `(refine|apply|exact).*Quotient.induction`. Includes the multiple-argument variants. tech debt 93/102 Mathlib/Algebra/GroupWithZero/Associated.lean,Mathlib/Algebra/Lie/Quotient.lean,Mathlib/Algebra/Module/ZLattice/Basic.lean,Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/Basic.lean,Mathlib/CategoryTheory/Abelian/Pseudoelements.lean,Mathlib/CategoryTheory/Monoidal/Free/Basic.lean,Mathlib/CategoryTheory/Subobject/Basic.lean,Mathlib/Combinatorics/Tiling/Tile.lean,Mathlib/Computability/Tape.lean,Mathlib/Data/Multiset/Functor.lean,Mathlib/Data/Multiset/Sym.lean,Mathlib/Data/Setoid/Basic.lean,Mathlib/FieldTheory/Fixed.lean,Mathlib/GroupTheory/Perm/Cycle/Concrete.lean,Mathlib/LinearAlgebra/Alternating/DomCoprod.lean,Mathlib/LinearAlgebra/Quotient/Pi.lean,Mathlib/Logic/Equiv/Basic.lean,Mathlib/NumberTheory/Padics/PadicNumbers.lean,Mathlib/NumberTheory/RamificationInertia/Basic.lean,Mathlib/Order/Category/PartOrd.lean,Mathlib/Order/RelIso/Basic.lean,Mathlib/RingTheory/AdicCompletion/Algebra.lean,Mathlib/RingTheory/AdicCompletion/Basic.lean,Mathlib/RingTheory/AdicCompletion/Functoriality.lean,Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean,Mathlib/SetTheory/Cardinal/Cofinality.lean,Mathlib/SetTheory/Ordinal/Arithmetic.lean,Mathlib/Topology/Algebra/InfiniteSum/Module.lean 28 1 ['github-actions'] nobody
4-39917
4 days ago
4-39949
4 days ago
4-39963
4 days
35884 Parcly-Taxel
author:Parcly-Taxel
 chore: fix induction and recursor names * `Finset.induction_on_{min,max}`, `Finset.induction_on_{min,max}_value` * `FreeAbelianGroup.induction_on`, `FreeAbelianGroup.induction_on'` Applications of these induction principles are also fixed. tech debt 109/112 Mathlib/Algebra/Order/Rearrangement.lean,Mathlib/Combinatorics/Additive/SubsetSum.lean,Mathlib/Data/Finset/Max.lean,Mathlib/GroupTheory/FreeAbelianGroup.lean,Mathlib/LinearAlgebra/Multilinear/Basic.lean 5 6 ['Parcly-Taxel', 'chenson2018', 'github-actions'] nobody
2-55094
2 days ago
4-27677
4 days ago
4-27658
4 days
35851 vihdzp
author:vihdzp
 chore(SetTheory/Ordinal/Arithmetic): remove `backward.privateInPublic` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) tech debt t-set-theory 12/17 Mathlib/SetTheory/Ordinal/Arithmetic.lean 1 5 ['github-actions', 'plp127', 'vihdzp'] nobody
2-36464
2 days ago
5-27965
5 days ago
5-27986
5 days