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.

stale PRs ready-to-merge
stale PRs labelled "maintainer merge"
all PRs labelled 'maintainer merge'
all PRs waiting on finding consensus on zulip
just the PRs addressing technical debt

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 17:55 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-40679 1 day ago	1-44972 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-10852 1 day ago	1-12932 1 day ago	4-28700 4 days
26231	chrisflav author:chrisflav	feat(CategoryTheory/Sites): sheaf condition and coproducts	We show that under suitable conditions, checking that a presheaf is a sheaf for a covering is equivalent to checking it on the single object covering by the coproduct. --- - [x] depends on: #32578 - [x] depends on: #35901 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-category-theory	156/1	Mathlib.lean,Mathlib/CategoryTheory/Limits/Shapes/Products.lean,Mathlib/CategoryTheory/Sites/CoproductSheafCondition.lean,Mathlib/CategoryTheory/Sites/Hypercover/SheafOfTypes.lean,Mathlib/CategoryTheory/Sites/Hypercover/Zero.lean	5	6	['chrisflav', 'github-actions', 'joelriou', 'mathlib-dependent-issues']	nobody	1-4657 1 day ago	1-12643 1 day ago	2-75068 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	27-1667 27 days ago	27-1671 27 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-23495 21 days ago	21-23495 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-36361 13 days ago	20-1083 20 days ago	42-38512 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-69139 8 days ago	8-71801 8 days ago	9-5350 9 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-48465 7 days ago	8-6728 8 days ago	19-53542 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	6-3739 6 days ago	6-4847 6 days ago	62-19691 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-79223 5 days ago	5-79224 5 days ago	22-19362 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-60816 3 days ago	12-10492 12 days ago	12-14843 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-69935 2 days ago	2-69935 2 days ago	10-12874 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-37861 2 days ago	5-25809 5 days ago	61-24484 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-21200 2 days ago	2-21200 2 days ago	10-41212 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-68512 1 day ago	7-25471 7 days ago	8-44448 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-32619 2 days ago	2-39010 2 days ago	5-23831 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-31430 23 days ago	23-32446 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-82115 11 days ago	12-40792 12 days ago	33-48321 33 days
35922	MichaelStollBayreuth author:MichaelStollBayreuth	feat(NumberTheory/Height/Basic): {mul\|log}Height_{eq_one_of_subsingleton\|sumElim_zero_eq}	This adds the facts that the multiplicative/logarithmic height of a tuple indexed by a subsingleton is one/zero and that the height does not change when we add/remove zeros in the tuple. --- - [ ] depends on: #35408 - [ ] depends on: #35260 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	blocked-by-other-PR t-number-theory t-algebra large-import label:t-algebra$	329/37	Mathlib/Analysis/Normed/Unbundled/InvariantExtension.lean,Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean,Mathlib/Data/Fintype/Order.lean,Mathlib/Data/Real/Archimedean.lean,Mathlib/NumberTheory/Height/Basic.lean,Mathlib/Order/ConditionallyCompleteLattice/Finset.lean,Mathlib/Order/PartialSups.lean,Mathlib/RingTheory/Finiteness/Nilpotent.lean	8	2	['github-actions', 'mathlib-dependent-issues']	nobody	3-3772 3 days ago	3-4873 3 days ago	0-417 6 minutes
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-76361 3 days ago	3-78461 3 days ago	3-78519 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	27-1667 27 days ago	27-1671 27 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-23495 21 days ago	21-23495 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-36361 13 days ago	20-1083 20 days ago	42-38512 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-69139 8 days ago	8-71801 8 days ago	9-5350 9 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-48465 7 days ago	8-6728 8 days ago	19-53542 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	6-3739 6 days ago	6-4847 6 days ago	62-19691 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-79223 5 days ago	5-79224 5 days ago	22-19362 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-60816 3 days ago	12-10492 12 days ago	12-14843 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-69935 2 days ago	2-69935 2 days ago	10-12874 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-37861 2 days ago	5-25809 5 days ago	61-24484 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-21200 2 days ago	2-21200 2 days ago	10-41212 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-68512 1 day ago	7-25471 7 days ago	8-44448 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-85904 23 hours ago	5-16576 5 days ago	36-67921 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-77027 21 hours ago	1-9511 1 day ago	17-59010 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-28535 7 hours ago	1-28562 1 day ago	12-72016 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-32619 2 days ago	2-39010 2 days ago	5-23831 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-31430 23 days ago	23-32446 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-82115 11 days ago	12-40792 12 days ago	33-48321 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-29776 8 hours ago	1-28217 1 day ago	1-63958 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-15587 4 hours ago	0-22536 6 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-13077 3 hours ago	0-13077 3 hours ago	1-5393 1 day
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-8628 2 hours ago	0-9796 2 hours ago	0-18830 5 hours
35922	MichaelStollBayreuth author:MichaelStollBayreuth	feat(NumberTheory/Height/Basic): {mul\|log}Height_{eq_one_of_subsingleton\|sumElim_zero_eq}	This adds the facts that the multiplicative/logarithmic height of a tuple indexed by a subsingleton is one/zero and that the height does not change when we add/remove zeros in the tuple. --- - [ ] depends on: #35408 - [ ] depends on: #35260 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	blocked-by-other-PR t-number-theory t-algebra large-import label:t-algebra$	329/37	Mathlib/Analysis/Normed/Unbundled/InvariantExtension.lean,Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean,Mathlib/Data/Fintype/Order.lean,Mathlib/Data/Real/Archimedean.lean,Mathlib/NumberTheory/Height/Basic.lean,Mathlib/Order/ConditionallyCompleteLattice/Finset.lean,Mathlib/Order/PartialSups.lean,Mathlib/RingTheory/Finiteness/Nilpotent.lean	8	2	['github-actions', 'mathlib-dependent-issues']	nobody	3-3772 3 days ago	3-4873 3 days ago	0-417 6 minutes
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-76361 3 days ago	3-78461 3 days ago	3-78519 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-20317 1 year ago	469-20317 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-62094 10 months ago	325-4324 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-69994 9 months ago	302-69999 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-50343 7 months ago	242-50343 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-49181 7 months ago	242-49182 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-64826 6 months ago	182-64827 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-42036 4 months ago	139-42037 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-52910 3 months ago	111-52910 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-70042 3 months ago	289-6201 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-86283 3 months ago	105-86284 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-37051 3 months ago	105-37052 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-8917 3 months ago	534-69042 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-77163 2 months ago	84-22229 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-45476 1 month ago	56-45477 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-7911 1 month ago	41-7911 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-47342 1 month ago	38-47359 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-12729 1 month ago	34-12729 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-34795 1 month ago	31-34795 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-25334 1 month ago	31-25334 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-25139 1 month ago	31-25139 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-71148 22 days ago	22-71148 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-43487 14 days ago	14-43487 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-39153 14 days ago	14-39153 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-37238 14 days ago	14-37238 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-35913 14 days ago	14-36011 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-6532 12 days ago	13-28767 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-71446 11 days ago	11-71447 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	9-3692 9 days ago	9-5678 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-30285 6 days ago	105-85374 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-30269 6 days ago	289-5276 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-50298 5 days ago	5-50298 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-82237 2 days ago	14-42162 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-32499 1 day ago	1-32499 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-33484 5 days ago	5-33597 5 days ago	12-64027 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-45569 4 days ago	4-45601 4 days ago	4-45618 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-60746 2 days ago	4-33329 4 days ago	4-33313 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-42116 2 days ago	5-33617 5 days ago	5-33641 5 days