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: July 01, 2025 at 20:13 UTC

Stale ready-to-merge'd PRs

Number	Author	Title	Description	Labels	+/-	Modified files (first 100)	📝	💬	All users who commented or reviewed	Assignee(s)	Updated	Last status change	total time in review
26161	leanprover-community-mathlib4-bot author:leanprover-community-mathlib4-bot	chore: adaptations for nightly-2025-06-19		merge-conflict ready-to-merge	26/19	Mathlib/Algebra/CharP/Basic.lean,Mathlib/Algebra/CharP/Defs.lean,Mathlib/Algebra/Group/Basic.lean,lake-manifest.json,lean-toolchain	5	n/a	['YaelDillies', 'github-actions', 'kim-em', 'mathlib-bors']	nobody	11-73864 11 days ago	unknown	unknown

Stale maintainer-merge'd PRs

Number	Author	Title	Description	Labels	+/-	Modified files (first 100)	📝	💬	All users who commented or reviewed	Assignee(s)	Updated	Last status change	total time in review
25265	FMLJohn author:FMLJohn	feat(Order/SupClosed): `compl_image_latticeClosure` and `compl_image_latticeClosure_eq_of_compl_image_eq_self`	The main results in this pull request are: 1. `compl_image_latticeClosure`: given any Boolean algebra `α` and `s : Set α`, `compl '' latticeClosure s` is the same as `latticeClosure (compl '' s)`; 2. `compl_image_latticeClosure_eq_of_compl_image_eq_self`: given any Boolean algebra `α` and `s : Set α` such that `compl '' s = s`, we have `compl '' latticeClosure s = latticeClosure s`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge t-order	59/1	Mathlib/Order/SupClosed.lean	1	8	['FMLJohn', 'YaelDillies', 'github-actions']	bryangingechen assignee:bryangingechen	26-22531 26 days ago	29-2503 29 days ago	33-12121 33 days
25089	Bergschaf author:Bergschaf	feat(Order/Sublocale): definition of sublocales	There are several possible definition of sublocales. I used one from [nlab](https://ncatlab.org/nlab/show/sublocale) which states that a sublocale is a subset of a locale which is closed under all meets and for any ∈ S and x ∈ X, we have x ⇨ s ∈ S. This PR also includes an order isomorphism between (Nucleus)ᵒᵈ and Sublocale. --- I am open to better name suggestions for the order isomorphism. - [x] depends on: #24941 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge t-order	265/8	Mathlib.lean,Mathlib/Order/Hom/Lattice.lean,Mathlib/Order/Nucleus.lean,Mathlib/Order/Sublocale.lean,Mathlib/Order/Synonym.lean,docs/references.bib	6	71	['Bergschaf', 'YaelDillies', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'xhalo32']	nobody	24-1337 24 days ago	24-1337 24 days ago	37-67159 37 days
25563	Komyyy author:Komyyy	chore: move `Topology.StoneCech` into `Topology.Compactification` (1/2)	At present, the `Topology.Compactification` directory includes results on one-point compactifications, but results on Stone-Čech compactifications are currently located elsewhere. The removed file `Topology.Compactification` is deprecated in another PR (#25583) to leave a good git diff history. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	file-removed maintainer-merge t-topology	9/9	Mathlib.lean,Mathlib/Combinatorics/Hindman.lean,Mathlib/Topology/Category/CompHaus/Basic.lean,Mathlib/Topology/Category/CompHaus/Projective.lean,Mathlib/Topology/Category/Profinite/Projective.lean,Mathlib/Topology/Category/Stonean/Adjunctions.lean,Mathlib/Topology/Compactification/StoneCech.lean,Mathlib/Topology/ExtremallyDisconnected.lean,Mathlib/Topology/Maps/Proper/UniversallyClosed.lean,Mathlib/Topology/Separation/CompletelyRegular.lean	10	4	['Komyyy', 'github-actions', 'grunweg']	nobody	23-42493 23 days ago	23-42493 23 days ago	24-18025 24 days
25600	Komyyy author:Komyyy	refactor: lemma expressing `ContinuousAt` using a punctured neighbourhood	--- This lemma is used to prove that the Riemann zeta function is meromorphic in #25597. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge t-topology	4/0	Mathlib/Topology/ContinuousOn.lean	1	5	['Komyyy', 'github-actions', 'grunweg']	nobody	22-79610 22 days ago	22-79610 22 days ago	23-5097 23 days
24669	qawbecrdtey author:qawbecrdtey	feat(Analysis/Normed/Operator/LinearIsometry): added definition `LinearIsometryEquiv.prodComm`	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) This commit defines a `LinearIsometryEquiv`, and states some trivial theorems about it. ```lean def prodComm [Module R E₂] : E × E₂ ≃ₗᵢ[R] E₂ × E ```	maintainer-merge t-analysis awaiting-author	8/1	Mathlib/Analysis/Normed/Operator/LinearIsometry.lean	1	10	['Ruben-VandeVelde', 'eric-wieser', 'faenuccio', 'github-actions', 'j-loreaux', 'jcommelin', 'qawbecrdtey']	faenuccio assignee:faenuccio	21-54995 21 days ago	21-54995 21 days ago	32-83569 32 days
23849	chrisflav author:chrisflav	feat(Data/Set): add `Set.encard_iUnion`	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	large-import t-data maintainer-merge	69/0	Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Data/Set/Card/Arithmetic.lean,Mathlib/Data/Set/Finite/Lattice.lean	3	25	['YaelDillies', 'chrisflav', 'github-actions']	YaelDillies assignee:YaelDillies	21-31058 21 days ago	21-31058 21 days ago	83-44848 83 days
25881	eric-wieser author:eric-wieser	chore: extract an auxiliary function from `congr()`	The motivation here is to make it easier to review #25851. This code is moved (and unindented) without changes. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	awaiting-zulip maintainer-merge t-meta	72/61	Mathlib/Tactic/TermCongr.lean	1	5	['eric-wieser', 'github-actions', 'grunweg', 'kmill']	nobody	16-81345 16 days ago	16-81345 16 days ago	0-3293 54 minutes
25172	eric-wieser author:eric-wieser	feat: restricting `Affine.Simplex` to an affine subspace that contains it	Also removes a redundant `Nonempty` argument. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge t-euclidean-geometry	68/5	Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean,Mathlib/LinearAlgebra/AffineSpace/Independent.lean	2	11	['eric-wieser', 'github-actions', 'jsm28', 'ocfnash']	nobody	4-86362 4 days ago	37-26553 1 month ago	37-67425 37 days
26405	euprunin author:euprunin	chore: golf using `omega`		maintainer-merge	23/68	Mathlib/Algebra/Polynomial/Module/Basic.lean,Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean,Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean,Mathlib/Combinatorics/Enumerative/Composition.lean,Mathlib/Computability/DFA.lean,Mathlib/Control/Fix.lean,Mathlib/Data/Nat/Choose/Basic.lean,Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean,Mathlib/Geometry/Euclidean/Circumcenter.lean,Mathlib/GroupTheory/Coxeter/Length.lean,Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean,Mathlib/MeasureTheory/Function/ConditionalExpectation/Unique.lean,Mathlib/NumberTheory/Dioph.lean,Mathlib/Order/Partition/Equipartition.lean,Mathlib/SetTheory/Game/State.lean,Mathlib/Tactic/NormNum/LegendreSymbol.lean,Mathlib/Topology/EMetricSpace/BoundedVariation.lean	17	10	['euprunin', 'github-actions', 'grunweg', 'leanprover-bot']	nobody	4-73914 4 days ago	4-73914 4 days ago	6-24383 6 days
26004	vasnesterov author:vasnesterov	feat(Algebra/Order/Floor): `⌊n * x⌋₊ / n = ⌊x⌋₊`	Prove that `⌊n * x⌋₊ / n = ⌊x⌋₊` for natural `n`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge t-order t-algebra label:t-algebra$	39/9	Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean,Mathlib/Algebra/Order/Floor/Ring.lean,Mathlib/Algebra/Order/Floor/Semiring.lean,Mathlib/Data/EReal/Inv.lean	4	21	['Ruben-VandeVelde', 'YaelDillies', 'b-mehta', 'eric-wieser', 'github-actions', 'vasnesterov']	nobody	4-47191 4 days ago	unknown	unknown
26426	Komyyy author:Komyyy	doc: remove `PartENat.card` in the module doc	[`PartENat.card`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Deprecated/Cardinal/Finite.html#PartENat.card) is moved to the `Deprecated` directory and it's not in this file([`Mathlib.SetTheory.Cardinal.Finite`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/SetTheory/Cardinal/Finite.html)) anymore. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-set-theory maintainer-merge easy documentation	0/2	Mathlib/SetTheory/Cardinal/Finite.lean	1	2	['github-actions', 'grunweg']	nobody	4-38831 4 days ago	4-38831 4 days ago	4-38844 4 days
26502	sgouezel author:sgouezel	feat: monotonicity of `lineMap`	Also remove one assumption in `differentiableOn_integral_of_continuous`, and expand docstrings around this theorem. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge t-analysis	49/10	Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/FundThmCalculus.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/IntegrationByParts.lean,Mathlib/Topology/Algebra/ContinuousAffineMap.lean	4	6	['eric-wieser', 'github-actions', 'grunweg', 'sgouezel']	nobody	2-28650 2 days ago	2-47841 2 days ago	2-53440 2 days
26166	joelriou author:joelriou	feat(AlgebraicTopology): application of the retract argument to model categories	Basic consequences of the retract argument are obtained for model categories: cofibrations are exactly the morphisms that have the left lifting property with respect to trivial fibrations, etc. We deduce various properties of cofibrations, fibrations and weak equivalences in model categories (e.g. they are stable by composition). --- (I am sorry if this one is a little bit long. There are too many basic properties to state.) This PR continues the work from #20210. Original PR: https://github.com/leanprover-community/mathlib4/pull/20210	large-import maintainer-merge t-topology	450/4	Mathlib.lean,Mathlib/AlgebraicTopology/ModelCategory/Basic.lean,Mathlib/AlgebraicTopology/ModelCategory/Instances.lean	3	n/a	['github-actions', 'joelriou', 'robin-carlier']	robin-carlier assignee:robin-carlier	1-49888 1 day ago	unknown	unknown
24361	Hagb author:Hagb	feat(Data/Finsupp/MonomialOrder): `0 ≤ a` where `a : m.syn`	`simp` would be able to solve it. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-data maintainer-merge new-contributor easy	3/0	Mathlib/Data/Finsupp/MonomialOrder.lean	1	2	['Ruben-VandeVelde', 'github-actions']	nobody	1-43784 1 day ago	1-43784 1 day ago	67-44546 67 days
24582	pechersky author:pechersky	feat(GroupTheory/ArchimedeanDensely): Unique (ℤ ≃+o ℤ)	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) - [x] depends on: #24580	maintainer-merge t-order t-algebra label:t-algebra$	44/0	Mathlib/Data/Int/Cast/Lemmas.lean,Mathlib/GroupTheory/ArchimedeanDensely.lean	2	6	['Ruben-VandeVelde', 'eric-wieser', 'github-actions', 'mathlib4-dependent-issues-bot', 'pechersky']	nobody	1-40675 1 day ago	1-40675 1 day ago	37-28881 37 days
25758	YaelDillies author:YaelDillies	chore: shortcut instance `CompleteLattice α → PartialOrder α`	This avoids using the path `CompleteLattice α → CompletePartialOrder α → PartialOrder α` that goes through `Order.CompletePartialOrder` and makes it appear used to our automation, such as `shake` or `#min_imports`. This is a followup to #25358. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge t-order	7/0	Mathlib/Order/CompleteLattice/Defs.lean	1	2	['Ruben-VandeVelde', 'github-actions']	nobody	1-40566 1 day ago	1-40566 1 day ago	19-41054 19 days
25897	YaelDillies author:YaelDillies	feat: `ofNat(n) • a = ofNat(n) * a`	From Toric --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	toric t-data maintainer-merge t-algebra label:t-algebra$	3/0	Mathlib/Data/Nat/Cast/Basic.lean	1	2	['Ruben-VandeVelde', 'github-actions']	nobody	1-40445 1 day ago	1-40445 1 day ago	16-37955 16 days
26027	vasnesterov author:vasnesterov	feat(Topology): every compact metric space can be embedded into the Hilbert cube	Prove `exists_closed_embedding_to_hilbert_cube`: every compact metric space can be embedded into the Hilbert cube. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge t-topology	58/1	Mathlib.lean,Mathlib/Topology/Compactness/HilbertCubeEmbedding.lean,Mathlib/Topology/MetricSpace/Bounded.lean	3	9	['ADedecker', 'github-actions', 'jcommelin', 'vasnesterov']	nobody	1-37703 1 day ago	1-37703 1 day ago	14-20262 14 days
26285	kckennylau author:kckennylau	feat(RingTheory): resultant of two polynomials	Co-authored-by: Anne Baanen --- Split from #26283. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge t-algebra label:t-algebra$	87/0	Mathlib.lean,Mathlib/RingTheory/Polynomial/Resultant/Basic.lean	2	20	['MichaelStollBayreuth', 'YaelDillies', 'eric-wieser', 'github-actions', 'kckennylau']	nobody	1-29210 1 day ago	1-31228 1 day ago	8-63393 8 days
25945	adomani author:adomani	feat: the empty line in commands linter	This linter flags empty lines within a command. It allows empty lines within doc-strings, module-docs and a couple of other "sensible" places. It also skips files that are likely to contain meta-code, since there the use of empty lines in definition is more widespread. This PR continues the work from #25236.	large-import maintainer-merge	375/5	Mathlib.lean,Mathlib/CategoryTheory/Comma/StructuredArrow/CommaMap.lean,Mathlib/Init.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/EmptyLine.lean,MathlibTest/EmptyLine.lean	6	3	['adomani', 'github-actions']	nobody	1-13946 1 day ago	15-46563 15 days ago	15-46618 15 days
25491	tannerduve author:tannerduve	feat(Control/Monad/Free): define free monad, prove it lawful, and implement standard effects	This PR introduces the `Free` monad. This implementation uses the "freer monad" approach as the traditional free monad (eg from [Haskell](https://hackage.haskell.org/package/free-5.2/docs/Control-Monad-Free.html)) is not safely definable in Lean due to termination checking (it's not strictly positive). The main contributions are: * Definition of the `Free` monad as an inductive type which generates a monad given any type constructor `F : Type -> Type`. * Functor and Monad instances for `Free F`, along with proofs of the `LawfulFunctor` and `LawfulMonad` laws. * Canonical instances of `Free` with standard effect signatures: * `FreeState s` for stateful computations, defined via a `StateF s` functor with `get` and `put` operations. * `FreeWriter w` for logging computations, defined via a `WriterF w` functor with a `tell` operation. * `FreeCont r` for continuation-passing computations, using the CPS functor `(α → r) → r`. In this construction, computations are represented as trees of effects. Each node (`liftBind`) represents a request to perform an effect, accompanied by a continuation specifying how the computation proceeds after the effect. The leaves (`pure`) represent completed computations with final results. A key insight is that `FreeM F` satisfies the universal property of free monads: for any monad `M` and effect handler `f : F → M`, there exists a unique way to interpret `FreeM F` computations in `M` that respects the effect semantics given by `f`. This unique interpreter is `mapM f`, which acts as the canonical fold for free monads. To execute or interpret these computations, we provide two approaches: 1. Hand-written interpreters (`FreeState.run`, `FreeWriter.run`, `FreeCont.run`) that directly pattern-match on the tree structure 2. Canonical interpreters (`FreeState.fold`, `FreeWriter.fold`, `FreeCont.fold`) derived from the universal property via `mapM` And then prove that these approaches are equivalent --- This PR adds new files and definitions; no breaking changes. Tags: free monad, freer monad, effect systems, state monad, writer monad, continuation monad, operational semantics, verified interpreters	t-data maintainer-merge	717/0	Mathlib.lean,Mathlib/Control/Monad/Free.lean,MathlibTest/freemonad.lean,docs/references.bib	4	144	['YaelDillies', 'copilot-pull-request-reviewer', 'eric-wieser', 'github-actions', 'plp127', 'quangvdao', 'tannerduve']	nobody	1-5802 1 day ago	14-18519 14 days ago	24-37603 24 days
21751	vihdzp author:vihdzp	refactor(SetTheory/Ordinal/Arithmetic): rework `Ordinal.pred` API	This PR does the following: - give a simpler definition of `Ordinal.pred` - replace `¬ ∃ a, o = succ a` and `∀ a, o ≠ succ a` by `IsSuccPrelimit o` throughout - improve theorem names --- There's a legitimate question of whether we even want `Ordinal.pred` (see [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Ordinal.2Epred)) but this should be a good change in the meanwhile regardless. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-set-theory maintainer-merge merge-conflict	102/67	Mathlib/SetTheory/Ordinal/Arithmetic.lean,Mathlib/SetTheory/Ordinal/Exponential.lean	2	13	['YaelDillies', 'github-actions', 'grunweg', 'vihdzp']	nobody	55-80180 1 month ago	102-58807 3 months ago	36-50134 36 days
24965	erdOne author:erdOne	refactor: Make `IsLocalHom` take unbundled map	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge t-algebra merge-conflict awaiting-author label:t-algebra$	16/7	Mathlib/Algebra/Group/Units/Hom.lean,Mathlib/AlgebraicGeometry/Scheme.lean,Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean,Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean,Mathlib/Geometry/RingedSpace/OpenImmersion.lean	5	6	['alreadydone', 'erdOne', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant']	nobody	28-63148 28 days ago	28-63149 28 days ago	10-26015 10 days
23961	FR-vdash-bot author:FR-vdash-bot	refactor: unbundle algebra from `ENormed*`	Further speed up the search in the algebraic typeclass hierarchy by avoiding searching for `TopologicalSpace`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	slow-typeclass-synthesis maintainer-merge t-algebra t-analysis merge-conflict awaiting-author label:t-algebra$	32/25	Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/Analysis/Normed/Group/Continuity.lean,Mathlib/Analysis/NormedSpace/IndicatorFunction.lean,Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean	5	12	['FR-vdash-bot', 'github-actions', 'grunweg', 'jcommelin', 'leanprover-bot', 'leanprover-community-bot-assistant']	nobody	24-47366 24 days ago	24-47366 24 days ago	17-72244 17 days

All maintainer merge'd PRs

Number	Author	Title	Description	Labels	+/-	Modified files (first 100)	📝	💬	All users who commented or reviewed	Assignee(s)	Updated	Last status change	total time in review
25265	FMLJohn author:FMLJohn	feat(Order/SupClosed): `compl_image_latticeClosure` and `compl_image_latticeClosure_eq_of_compl_image_eq_self`	The main results in this pull request are: 1. `compl_image_latticeClosure`: given any Boolean algebra `α` and `s : Set α`, `compl '' latticeClosure s` is the same as `latticeClosure (compl '' s)`; 2. `compl_image_latticeClosure_eq_of_compl_image_eq_self`: given any Boolean algebra `α` and `s : Set α` such that `compl '' s = s`, we have `compl '' latticeClosure s = latticeClosure s`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge t-order	59/1	Mathlib/Order/SupClosed.lean	1	8	['FMLJohn', 'YaelDillies', 'github-actions']	bryangingechen assignee:bryangingechen	26-22531 26 days ago	29-2503 29 days ago	33-12121 33 days
25089	Bergschaf author:Bergschaf	feat(Order/Sublocale): definition of sublocales	There are several possible definition of sublocales. I used one from [nlab](https://ncatlab.org/nlab/show/sublocale) which states that a sublocale is a subset of a locale which is closed under all meets and for any ∈ S and x ∈ X, we have x ⇨ s ∈ S. This PR also includes an order isomorphism between (Nucleus)ᵒᵈ and Sublocale. --- I am open to better name suggestions for the order isomorphism. - [x] depends on: #24941 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge t-order	265/8	Mathlib.lean,Mathlib/Order/Hom/Lattice.lean,Mathlib/Order/Nucleus.lean,Mathlib/Order/Sublocale.lean,Mathlib/Order/Synonym.lean,docs/references.bib	6	71	['Bergschaf', 'YaelDillies', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'xhalo32']	nobody	24-1337 24 days ago	24-1337 24 days ago	37-67159 37 days
25563	Komyyy author:Komyyy	chore: move `Topology.StoneCech` into `Topology.Compactification` (1/2)	At present, the `Topology.Compactification` directory includes results on one-point compactifications, but results on Stone-Čech compactifications are currently located elsewhere. The removed file `Topology.Compactification` is deprecated in another PR (#25583) to leave a good git diff history. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	file-removed maintainer-merge t-topology	9/9	Mathlib.lean,Mathlib/Combinatorics/Hindman.lean,Mathlib/Topology/Category/CompHaus/Basic.lean,Mathlib/Topology/Category/CompHaus/Projective.lean,Mathlib/Topology/Category/Profinite/Projective.lean,Mathlib/Topology/Category/Stonean/Adjunctions.lean,Mathlib/Topology/Compactification/StoneCech.lean,Mathlib/Topology/ExtremallyDisconnected.lean,Mathlib/Topology/Maps/Proper/UniversallyClosed.lean,Mathlib/Topology/Separation/CompletelyRegular.lean	10	4	['Komyyy', 'github-actions', 'grunweg']	nobody	23-42493 23 days ago	23-42493 23 days ago	24-18025 24 days
25600	Komyyy author:Komyyy	refactor: lemma expressing `ContinuousAt` using a punctured neighbourhood	--- This lemma is used to prove that the Riemann zeta function is meromorphic in #25597. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge t-topology	4/0	Mathlib/Topology/ContinuousOn.lean	1	5	['Komyyy', 'github-actions', 'grunweg']	nobody	22-79610 22 days ago	22-79610 22 days ago	23-5097 23 days
24669	qawbecrdtey author:qawbecrdtey	feat(Analysis/Normed/Operator/LinearIsometry): added definition `LinearIsometryEquiv.prodComm`	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) This commit defines a `LinearIsometryEquiv`, and states some trivial theorems about it. ```lean def prodComm [Module R E₂] : E × E₂ ≃ₗᵢ[R] E₂ × E ```	maintainer-merge t-analysis awaiting-author	8/1	Mathlib/Analysis/Normed/Operator/LinearIsometry.lean	1	10	['Ruben-VandeVelde', 'eric-wieser', 'faenuccio', 'github-actions', 'j-loreaux', 'jcommelin', 'qawbecrdtey']	faenuccio assignee:faenuccio	21-54995 21 days ago	21-54995 21 days ago	32-83569 32 days
23849	chrisflav author:chrisflav	feat(Data/Set): add `Set.encard_iUnion`	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	large-import t-data maintainer-merge	69/0	Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Data/Set/Card/Arithmetic.lean,Mathlib/Data/Set/Finite/Lattice.lean	3	25	['YaelDillies', 'chrisflav', 'github-actions']	YaelDillies assignee:YaelDillies	21-31058 21 days ago	21-31058 21 days ago	83-44848 83 days
25881	eric-wieser author:eric-wieser	chore: extract an auxiliary function from `congr()`	The motivation here is to make it easier to review #25851. This code is moved (and unindented) without changes. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	awaiting-zulip maintainer-merge t-meta	72/61	Mathlib/Tactic/TermCongr.lean	1	5	['eric-wieser', 'github-actions', 'grunweg', 'kmill']	nobody	16-81345 16 days ago	16-81345 16 days ago	0-3293 54 minutes
25172	eric-wieser author:eric-wieser	feat: restricting `Affine.Simplex` to an affine subspace that contains it	Also removes a redundant `Nonempty` argument. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge t-euclidean-geometry	68/5	Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean,Mathlib/LinearAlgebra/AffineSpace/Independent.lean	2	11	['eric-wieser', 'github-actions', 'jsm28', 'ocfnash']	nobody	4-86362 4 days ago	37-26553 1 month ago	37-67425 37 days
26405	euprunin author:euprunin	chore: golf using `omega`		maintainer-merge	23/68	Mathlib/Algebra/Polynomial/Module/Basic.lean,Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean,Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean,Mathlib/Combinatorics/Enumerative/Composition.lean,Mathlib/Computability/DFA.lean,Mathlib/Control/Fix.lean,Mathlib/Data/Nat/Choose/Basic.lean,Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean,Mathlib/Geometry/Euclidean/Circumcenter.lean,Mathlib/GroupTheory/Coxeter/Length.lean,Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean,Mathlib/MeasureTheory/Function/ConditionalExpectation/Unique.lean,Mathlib/NumberTheory/Dioph.lean,Mathlib/Order/Partition/Equipartition.lean,Mathlib/SetTheory/Game/State.lean,Mathlib/Tactic/NormNum/LegendreSymbol.lean,Mathlib/Topology/EMetricSpace/BoundedVariation.lean	17	10	['euprunin', 'github-actions', 'grunweg', 'leanprover-bot']	nobody	4-73914 4 days ago	4-73914 4 days ago	6-24383 6 days
26004	vasnesterov author:vasnesterov	feat(Algebra/Order/Floor): `⌊n * x⌋₊ / n = ⌊x⌋₊`	Prove that `⌊n * x⌋₊ / n = ⌊x⌋₊` for natural `n`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge t-order t-algebra label:t-algebra$	39/9	Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean,Mathlib/Algebra/Order/Floor/Ring.lean,Mathlib/Algebra/Order/Floor/Semiring.lean,Mathlib/Data/EReal/Inv.lean	4	21	['Ruben-VandeVelde', 'YaelDillies', 'b-mehta', 'eric-wieser', 'github-actions', 'vasnesterov']	nobody	4-47191 4 days ago	unknown	unknown
26426	Komyyy author:Komyyy	doc: remove `PartENat.card` in the module doc	[`PartENat.card`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Deprecated/Cardinal/Finite.html#PartENat.card) is moved to the `Deprecated` directory and it's not in this file([`Mathlib.SetTheory.Cardinal.Finite`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/SetTheory/Cardinal/Finite.html)) anymore. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-set-theory maintainer-merge easy documentation	0/2	Mathlib/SetTheory/Cardinal/Finite.lean	1	2	['github-actions', 'grunweg']	nobody	4-38831 4 days ago	4-38831 4 days ago	4-38844 4 days
26502	sgouezel author:sgouezel	feat: monotonicity of `lineMap`	Also remove one assumption in `differentiableOn_integral_of_continuous`, and expand docstrings around this theorem. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge t-analysis	49/10	Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/FundThmCalculus.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/IntegrationByParts.lean,Mathlib/Topology/Algebra/ContinuousAffineMap.lean	4	6	['eric-wieser', 'github-actions', 'grunweg', 'sgouezel']	nobody	2-28650 2 days ago	2-47841 2 days ago	2-53440 2 days
26166	joelriou author:joelriou	feat(AlgebraicTopology): application of the retract argument to model categories	Basic consequences of the retract argument are obtained for model categories: cofibrations are exactly the morphisms that have the left lifting property with respect to trivial fibrations, etc. We deduce various properties of cofibrations, fibrations and weak equivalences in model categories (e.g. they are stable by composition). --- (I am sorry if this one is a little bit long. There are too many basic properties to state.) This PR continues the work from #20210. Original PR: https://github.com/leanprover-community/mathlib4/pull/20210	large-import maintainer-merge t-topology	450/4	Mathlib.lean,Mathlib/AlgebraicTopology/ModelCategory/Basic.lean,Mathlib/AlgebraicTopology/ModelCategory/Instances.lean	3	n/a	['github-actions', 'joelriou', 'robin-carlier']	robin-carlier assignee:robin-carlier	1-49888 1 day ago	unknown	unknown
24361	Hagb author:Hagb	feat(Data/Finsupp/MonomialOrder): `0 ≤ a` where `a : m.syn`	`simp` would be able to solve it. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-data maintainer-merge new-contributor easy	3/0	Mathlib/Data/Finsupp/MonomialOrder.lean	1	2	['Ruben-VandeVelde', 'github-actions']	nobody	1-43784 1 day ago	1-43784 1 day ago	67-44546 67 days
24582	pechersky author:pechersky	feat(GroupTheory/ArchimedeanDensely): Unique (ℤ ≃+o ℤ)	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) - [x] depends on: #24580	maintainer-merge t-order t-algebra label:t-algebra$	44/0	Mathlib/Data/Int/Cast/Lemmas.lean,Mathlib/GroupTheory/ArchimedeanDensely.lean	2	6	['Ruben-VandeVelde', 'eric-wieser', 'github-actions', 'mathlib4-dependent-issues-bot', 'pechersky']	nobody	1-40675 1 day ago	1-40675 1 day ago	37-28881 37 days
25758	YaelDillies author:YaelDillies	chore: shortcut instance `CompleteLattice α → PartialOrder α`	This avoids using the path `CompleteLattice α → CompletePartialOrder α → PartialOrder α` that goes through `Order.CompletePartialOrder` and makes it appear used to our automation, such as `shake` or `#min_imports`. This is a followup to #25358. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge t-order	7/0	Mathlib/Order/CompleteLattice/Defs.lean	1	2	['Ruben-VandeVelde', 'github-actions']	nobody	1-40566 1 day ago	1-40566 1 day ago	19-41054 19 days
25897	YaelDillies author:YaelDillies	feat: `ofNat(n) • a = ofNat(n) * a`	From Toric --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	toric t-data maintainer-merge t-algebra label:t-algebra$	3/0	Mathlib/Data/Nat/Cast/Basic.lean	1	2	['Ruben-VandeVelde', 'github-actions']	nobody	1-40445 1 day ago	1-40445 1 day ago	16-37955 16 days
26027	vasnesterov author:vasnesterov	feat(Topology): every compact metric space can be embedded into the Hilbert cube	Prove `exists_closed_embedding_to_hilbert_cube`: every compact metric space can be embedded into the Hilbert cube. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge t-topology	58/1	Mathlib.lean,Mathlib/Topology/Compactness/HilbertCubeEmbedding.lean,Mathlib/Topology/MetricSpace/Bounded.lean	3	9	['ADedecker', 'github-actions', 'jcommelin', 'vasnesterov']	nobody	1-37703 1 day ago	1-37703 1 day ago	14-20262 14 days
26285	kckennylau author:kckennylau	feat(RingTheory): resultant of two polynomials	Co-authored-by: Anne Baanen --- Split from #26283. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge t-algebra label:t-algebra$	87/0	Mathlib.lean,Mathlib/RingTheory/Polynomial/Resultant/Basic.lean	2	20	['MichaelStollBayreuth', 'YaelDillies', 'eric-wieser', 'github-actions', 'kckennylau']	nobody	1-29210 1 day ago	1-31228 1 day ago	8-63393 8 days
25945	adomani author:adomani	feat: the empty line in commands linter	This linter flags empty lines within a command. It allows empty lines within doc-strings, module-docs and a couple of other "sensible" places. It also skips files that are likely to contain meta-code, since there the use of empty lines in definition is more widespread. This PR continues the work from #25236.	large-import maintainer-merge	375/5	Mathlib.lean,Mathlib/CategoryTheory/Comma/StructuredArrow/CommaMap.lean,Mathlib/Init.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/EmptyLine.lean,MathlibTest/EmptyLine.lean	6	3	['adomani', 'github-actions']	nobody	1-13946 1 day ago	15-46563 15 days ago	15-46618 15 days
25491	tannerduve author:tannerduve	feat(Control/Monad/Free): define free monad, prove it lawful, and implement standard effects	This PR introduces the `Free` monad. This implementation uses the "freer monad" approach as the traditional free monad (eg from [Haskell](https://hackage.haskell.org/package/free-5.2/docs/Control-Monad-Free.html)) is not safely definable in Lean due to termination checking (it's not strictly positive). The main contributions are: * Definition of the `Free` monad as an inductive type which generates a monad given any type constructor `F : Type -> Type`. * Functor and Monad instances for `Free F`, along with proofs of the `LawfulFunctor` and `LawfulMonad` laws. * Canonical instances of `Free` with standard effect signatures: * `FreeState s` for stateful computations, defined via a `StateF s` functor with `get` and `put` operations. * `FreeWriter w` for logging computations, defined via a `WriterF w` functor with a `tell` operation. * `FreeCont r` for continuation-passing computations, using the CPS functor `(α → r) → r`. In this construction, computations are represented as trees of effects. Each node (`liftBind`) represents a request to perform an effect, accompanied by a continuation specifying how the computation proceeds after the effect. The leaves (`pure`) represent completed computations with final results. A key insight is that `FreeM F` satisfies the universal property of free monads: for any monad `M` and effect handler `f : F → M`, there exists a unique way to interpret `FreeM F` computations in `M` that respects the effect semantics given by `f`. This unique interpreter is `mapM f`, which acts as the canonical fold for free monads. To execute or interpret these computations, we provide two approaches: 1. Hand-written interpreters (`FreeState.run`, `FreeWriter.run`, `FreeCont.run`) that directly pattern-match on the tree structure 2. Canonical interpreters (`FreeState.fold`, `FreeWriter.fold`, `FreeCont.fold`) derived from the universal property via `mapM` And then prove that these approaches are equivalent --- This PR adds new files and definitions; no breaking changes. Tags: free monad, freer monad, effect systems, state monad, writer monad, continuation monad, operational semantics, verified interpreters	t-data maintainer-merge	717/0	Mathlib.lean,Mathlib/Control/Monad/Free.lean,MathlibTest/freemonad.lean,docs/references.bib	4	144	['YaelDillies', 'copilot-pull-request-reviewer', 'eric-wieser', 'github-actions', 'plp127', 'quangvdao', 'tannerduve']	nobody	1-5802 1 day ago	14-18519 14 days ago	24-37603 24 days
26543	vihdzp author:vihdzp	feat(SetTheory/ZFC/VonNeumann): von Neumann hierarchy of sets	Ported from #17027. For extra discussion on this PR, see [Zulip](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2317027.20.2C.20.2326518.20von.20Neumann.20hierarchy/with/526389347). --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-set-theory maintainer-merge	133/0	Mathlib.lean,Mathlib/SetTheory/Ordinal/Basic.lean,Mathlib/SetTheory/ZFC/Basic.lean,Mathlib/SetTheory/ZFC/VonNeumann.lean	4	55	['alreadydone', 'github-actions', 'kckennylau', 'vihdzp']	nobody	0-81312 22 hours ago	0-81553 22 hours ago	1-24692 1 day
26411	sgouezel author:sgouezel	feat: add `iInf` results on `ENNReal`, matching existing `iSup` ones	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-data maintainer-merge	39/0	Mathlib/Data/ENNReal/Operations.lean	1	22	['YaelDillies', 'github-actions', 'grunweg', 'sgouezel']	nobody	0-42526 11 hours ago	0-42526 11 hours ago	5-23310 5 days
26562	Ruben-VandeVelde author:Ruben-VandeVelde	chore: deprecate Mathlib.Algebra.Ring.Hom.Basic	It was emptied in #25447. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	large-import maintainer-merge t-algebra label:t-algebra$	4/10	Mathlib/Algebra/Ring/Hom/Basic.lean	1	4	['Ruben-VandeVelde', 'github-actions', 'grunweg']	nobody	0-41736 11 hours ago	0-41837 11 hours ago	0-81219 22 hours
26576	kim-em author:kim-em	feat: use grind in Data/Nat/Hyperoperations	Some nice interactions between `grind`'s ring handling, case splitting, and instantiation.	maintainer-merge	35/57	Mathlib/Algebra/Group/Even.lean,Mathlib/Data/Nat/Hyperoperation.lean	2	7	['dupuisf', 'github-actions', 'grunweg', 'leanprover-bot']	nobody	0-72 1 minute ago	0-49 33 seconds ago	0-47571 13 hours
26570	winstonyin author:winstonyin	feat: version of `prod_range_induction` with weaker assumptions	`prod_range_induction` currently requires ratios of adjacent terms to be checked for the entire sequence, but we only need to check terms up to `n`. I provide a parallel `prod_range_induction'` that relaxes this assumption. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge t-algebra label:t-algebra$	13/0	Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean	1	3	['github-actions', 'grunweg']	grunweg assignee:grunweg	0-40006 11 hours ago	0-43160 11 hours ago	0-58322 16 hours
26365	joelriou author:joelriou	feat(CategoryTheory/Localization): generalize results about adjunctions	In this PR, results about adjunctions, localization of categories and calculus of fractions are slightly generalized. In particular, we show that under certain circumstances, adjoint functors are localization functors. (This shall be used in the proof of the fundamental lemma of homotopical algebra #26303.) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge t-category-theory	108/25	Mathlib/CategoryTheory/Localization/CalculusOfFractions/OfAdjunction.lean,Mathlib/CategoryTheory/Localization/Opposite.lean	2	7	['github-actions', 'joelriou', 'robin-carlier']	robin-carlier assignee:robin-carlier	0-35926 9 hours ago	0-36138 10 hours ago	7-15308 7 days
25919	BoltonBailey author:BoltonBailey	doc: suggest !bench in `lake exe pole`	This PR makes an error message on `lake exe pole` give some information which is often relevant. Original PR: https://github.com/leanprover-community/mathlib4/pull/12561	maintainer-merge	2/1	LongestPole/Main.lean	1	3	['BoltonBailey', 'Ruben-VandeVelde', 'github-actions']	nobody	0-11431 3 hours ago	0-40247 11 hours ago	16-16136 16 days
25872	101damnations author:101damnations	feat(RepresentationTheory/GroupCohomology): long exact sequences	Given a commutative ring `k` and a group `G`, this PR shows that a short exact sequence of `k`-linear `G`-representations `0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0` induces a short exact sequence of complexes `0 ⟶ inhomogeneousCochains X₁ ⟶ inhomogeneousCochains X₂ ⟶ inhomogeneousCochains X₃ ⟶ 0`. Since the cohomology of `inhomogeneousCochains Xᵢ` is the group cohomology of `Xᵢ`, this allows us to specialize API about long exact sequences to group cohomology. --- - [x] depends on: #25815 - [x] depends on: #25870 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) --- This PR continues the work from #25311. Original PR: https://github.com/leanprover-community/mathlib4/pull/25311	maintainer-merge t-algebra label:t-algebra$	290/7	Mathlib.lean,Mathlib/Algebra/Homology/ConcreteCategory.lean,Mathlib/Algebra/Homology/HomologySequence.lean,Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean,Mathlib/LinearAlgebra/Pi.lean,Mathlib/RepresentationTheory/Homological/GroupCohomology/Basic.lean,Mathlib/RepresentationTheory/Homological/GroupCohomology/LongExactSequence.lean,Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean	8	10	['101damnations', 'github-actions', 'kbuzzard', 'mathlib4-dependent-issues-bot']	nobody	0-10445 2 hours ago	1-79351 1 day ago	14-59748 14 days
26584	mariainesdff author:mariainesdff	chore(Algebra.Order.Group.Cyclic): generalize Subgroup.genLTOne	Generalize `Subgroup.genLTOne` so that it assumes that the subgroup itself is cyclic, rather than the ambient group. Co-authored-by: @faenuccio --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge t-algebra label:t-algebra$	13/7	Mathlib/Algebra/Order/Group/Cyclic.lean	1	2	['github-actions', 'grunweg']	nobody	0-9579 2 hours ago	0-9579 2 hours ago	0-27046 7 hours
21751	vihdzp author:vihdzp	refactor(SetTheory/Ordinal/Arithmetic): rework `Ordinal.pred` API	This PR does the following: - give a simpler definition of `Ordinal.pred` - replace `¬ ∃ a, o = succ a` and `∀ a, o ≠ succ a` by `IsSuccPrelimit o` throughout - improve theorem names --- There's a legitimate question of whether we even want `Ordinal.pred` (see [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Ordinal.2Epred)) but this should be a good change in the meanwhile regardless. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-set-theory maintainer-merge merge-conflict	102/67	Mathlib/SetTheory/Ordinal/Arithmetic.lean,Mathlib/SetTheory/Ordinal/Exponential.lean	2	13	['YaelDillies', 'github-actions', 'grunweg', 'vihdzp']	nobody	55-80180 1 month ago	102-58807 3 months ago	36-50134 36 days
24965	erdOne author:erdOne	refactor: Make `IsLocalHom` take unbundled map	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge t-algebra merge-conflict awaiting-author label:t-algebra$	16/7	Mathlib/Algebra/Group/Units/Hom.lean,Mathlib/AlgebraicGeometry/Scheme.lean,Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean,Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean,Mathlib/Geometry/RingedSpace/OpenImmersion.lean	5	6	['alreadydone', 'erdOne', 'eric-wieser', 'github-actions', 'leanprover-community-bot-assistant']	nobody	28-63148 28 days ago	28-63149 28 days ago	10-26015 10 days
23961	FR-vdash-bot author:FR-vdash-bot	refactor: unbundle algebra from `ENormed*`	Further speed up the search in the algebraic typeclass hierarchy by avoiding searching for `TopologicalSpace`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	slow-typeclass-synthesis maintainer-merge t-algebra t-analysis merge-conflict awaiting-author label:t-algebra$	32/25	Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/Analysis/Normed/Group/Continuity.lean,Mathlib/Analysis/NormedSpace/IndicatorFunction.lean,Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean	5	12	['FR-vdash-bot', 'github-actions', 'grunweg', 'jcommelin', 'leanprover-bot', 'leanprover-community-bot-assistant']	nobody	24-47366 24 days ago	24-47366 24 days ago	17-72244 17 days

PRs blocked on a zulip discussion

Number	Author	Title	Description	Labels	+/-	Modified files (first 100)	📝	💬	All users who commented or reviewed	Assignee(s)	Updated	Last status change	total time in review
23866	kim-em author:kim-em	chore: remove `[AtLeastTwo n]` hypothesis from the `NatCast` to `OfNat` instance	This PR observes that we can change ``` instance (priority := 100) instOfNatAtLeastTwo {n : ℕ} [NatCast R] [Nat.AtLeastTwo n] : OfNat R n ``` to ``` instance (priority := 100) instOfNatAtLeastTwo {n : ℕ} [NatCast R] : OfNat R n ``` with minimal fall-out. A follow-up PR #23867 then observes that we can remove nearly all the `[Nat.AtLeastTwo n]` hypotheses in Mathlib. This is slightly dangerous -- it does make it more likely that we'll generate non-defeq instances, but it appears to happen very rarely. However, it will make life slightly easier for something Leo and I are trying to do with `grind` and Grobner bases (we'd like to be able to assume types we consume have `[∀ n, OfNat α n]`, which is possible with this change, but not without...). Zulip thread: [#PR reviews > #23866 and #23867, removing most `[Nat.AtLeastTwo n]` @ 💬](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2323866.20and.20.2323867.2C.20removing.20most.20.60.5BNat.2EAtLeastTwo.20n.5D.60/near/511157297)	awaiting-zulip	21/26	Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean,Mathlib/Data/Nat/Cast/Defs.lean,Mathlib/Data/Nat/Cast/Order/Basic.lean	3	3	['eric-wieser', 'github-actions', 'urkud']	nobody	83-4410 2 months ago	83-4499 2 months ago	0-23929 6 hours
15649	TpmKranz author:TpmKranz	feat(Computability): introduce Generalised NFA as bridge to Regular Expression	Lays the groundwork for a proof of equivalence of NFA and RE, w.r.t. described language. Actual connection to NFA comes later, after the groundwork for the opposite direction has been laid. Second chunk of #12648 --- - [x] depends on: #15647 [Data.FinEnum.Option unchanged since then] [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	awaiting-zulip t-computability new-contributor awaiting-author	298/0	Mathlib.lean,Mathlib/Computability/GNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/RegularExpressions.lean,docs/references.bib	5	6	['github-actions', 'mathlib4-dependent-issues-bot', 'meithecatte', 'trivial1711']	nobody	56-78287 1 month ago	56-78296 1 month ago	23-54870 23 days
20648	anthonyde author:anthonyde	feat: formalize regular expression -> εNFA	The file `Computability/RegularExpressionsToEpsilonNFA.lean` contains a formal definition of Thompson's method for constructing an `εNFA` from a `RegularExpression` and a proof of its correctness. --- - [x] depends on: #20644 - [x] depends on: #20645 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	awaiting-zulip t-computability new-contributor	490/0	Mathlib.lean,Mathlib/Computability/RegularExpressionsToEpsilonNFA.lean,docs/references.bib	3	5	['github-actions', 'mathlib4-dependent-issues-bot', 'meithecatte', 'qawbecrdtey']	nobody	56-77598 1 month ago	56-78233 1 month ago	75-77754 75 days
17458	urkud author:urkud	refactor(Algebra/Group): make `IsUnit` a typeclass	Also change some lemmas to assume `[IsUnit _]` instead of `[Invertible _]`. Motivated by potential non-defeq diamonds in #14986, see also [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Invertible.20and.20data) I no longer plan to merge this PR, but I'm going to cherry-pick some changes to a new PR before closing this one. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	awaiting-zulip t-algebra label:t-algebra$	82/72	Mathlib/Algebra/CharP/Invertible.lean,Mathlib/Algebra/Group/Invertible/Basic.lean,Mathlib/Algebra/Group/Units/Defs.lean,Mathlib/Algebra/GroupWithZero/Invertible.lean,Mathlib/Algebra/GroupWithZero/Units/Basic.lean,Mathlib/Algebra/Polynomial/Degree/Units.lean,Mathlib/Algebra/Polynomial/Splits.lean,Mathlib/Analysis/Convex/Segment.lean,Mathlib/Analysis/Normed/Affine/Isometry.lean,Mathlib/Analysis/Normed/Ring/Units.lean,Mathlib/CategoryTheory/Linear/Basic.lean,Mathlib/FieldTheory/Finite/Basic.lean,Mathlib/FieldTheory/Separable.lean,Mathlib/FieldTheory/SeparableDegree.lean,Mathlib/GroupTheory/Submonoid/Inverses.lean,Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean,Mathlib/LinearAlgebra/AffineSpace/Combination.lean,Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean,Mathlib/LinearAlgebra/CliffordAlgebra/Inversion.lean,Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean,Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean,Mathlib/NumberTheory/MulChar/Basic.lean,Mathlib/RingTheory/Localization/NumDen.lean,Mathlib/RingTheory/Polynomial/Content.lean,Mathlib/RingTheory/Polynomial/GaussLemma.lean,Mathlib/RingTheory/Valuation/Basic.lean	26	11	['MichaelStollBayreuth', 'acmepjz', 'eric-wieser', 'github-actions', 'leanprover-bot', 'urkud']	nobody	43-64248 1 month ago	43-84675 1 month ago	0-66650 18 hours
20238	maemre author:maemre	feat(Computability/DFA): Closure of regular languages under some set operations	This shows that regular languages are closed under complement and intersection by constructing DFAs for them. --- Closure under all other operations will be proved when someone adds the proof for DFA<->regular expression equivalence, so they are not part of this PR. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	awaiting-zulip t-computability new-contributor awaiting-author	159/0	Mathlib/Computability/DFA.lean,Mathlib/Computability/Language.lean	2	59	['EtienneC30', 'YaelDillies', 'github-actions', 'maemre', 'meithecatte', 'urkud']	EtienneC30 assignee:EtienneC30	27-44058 27 days ago	56-78197 1 month ago	48-67492 48 days
23929	meithecatte author:meithecatte	feat(Computability/NFA): improve bound on pumping lemma	--- - [x] depends on: #25321 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	awaiting-zulip t-computability new-contributor	101/10	Mathlib/Computability/EpsilonNFA.lean,Mathlib/Computability/NFA.lean	2	41	['YaelDillies', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'meithecatte']	nobody	24-1449 24 days ago	24-1450 24 days ago	34-10595 34 days
25881	eric-wieser author:eric-wieser	chore: extract an auxiliary function from `congr()`	The motivation here is to make it easier to review #25851. This code is moved (and unindented) without changes. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	awaiting-zulip maintainer-merge t-meta	72/61	Mathlib/Tactic/TermCongr.lean	1	5	['eric-wieser', 'github-actions', 'grunweg', 'kmill']	nobody	16-81345 16 days ago	16-81345 16 days ago	0-3293 54 minutes
25218	kckennylau author:kckennylau	feat(AlgebraicGeometry): Tate normal form of elliptic curves	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	awaiting-zulip new-contributor t-algebraic-geometry	291/26	Mathlib.lean,Mathlib/AlgebraicGeometry/EllipticCurve/IsomOfJ.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Modular/TateNormalForm.lean,Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean,Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean	5	30	['MichaelStollBayreuth', 'Multramate', 'acmepjz', 'github-actions', 'grunweg', 'kckennylau']	nobody	13-34673 13 days ago	29-32551 29 days ago	6-51040 6 days
11800	JADekker author:JADekker	feat : Define KappaLindelöf spaces	Define KappaLindelöf spaces by following the first one-third of the API for Lindelöf spaces. The remainder will be added in a future PR. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	awaiting-zulip t-topology merge-conflict please-adopt	301/2	Mathlib.lean,Mathlib/Topology/Compactness/KappaLindelof.lean,Mathlib/Topology/Compactness/Lindelof.lean	3	38	['ADedecker', 'JADekker', 'PatrickMassot', 'StevenClontz', 'adomani', 'github-actions', 'grunweg', 'kim-em', 'urkud']	nobody	288-55320 9 months ago	288-77295 9 months ago	119-10687 119 days
17518	grunweg author:grunweg	feat: lint on declarations mentioning `Invertible` or `Unique`	Using the same infrastructure as for #10235. Depends on that PR to land first, and also (for the first lint) a zulip discussion if that change is desired/about the best way to enact it. --- - [ ] depends on: #10235	awaiting-zulip t-linter merge-conflict blocked-by-other-PR	149/7	Mathlib.lean,Mathlib/Algebra/MvPolynomial/PDeriv.lean,Mathlib/Computability/Halting.lean,Mathlib/Computability/TuringMachine.lean,Mathlib/Data/Fintype/Card.lean,Mathlib/GroupTheory/Perm/DomMulAct.lean,Mathlib/Logic/Basic.lean,Mathlib/Logic/Encodable/Basic.lean,Mathlib/NumberTheory/JacobiSum/Basic.lean,Mathlib/Order/Heyting/Regular.lean,Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Linter/UnusedAssumptionInType.lean	13	3	['github-actions', 'mathlib4-dependent-issues-bot', 'mergify']	nobody	241-9039 7 months ago	266-83961 8 months ago *	0-0 0 seconds *
17623	FR-vdash-bot author:FR-vdash-bot	feat(Algebra/Order/GroupWithZero/Unbundled): add some lemmas	Some lemmas in `Algebra.Order.GroupWithZero.Unbundled` have incorrect or unsatisfactory names, or assumptions that can be omitted using `ZeroLEOneClass`. The lemmas added in this PR are versions of existing lemmas that use the correct or better name or `ZeroLEOneClass` to omit an assumption. The original lemmas will be deprecated in #17593. \| New name \| Old name \| \|-------------------------\|-------------------------\| \| `mul_le_one_left₀` \| `Left.mul_le_one_of_le_of_le` \| \| `mul_lt_one_of_le_of_lt_left₀` (`0 ≤ ·` version) / `mul_lt_one_of_le_of_lt_of_pos_left` \| `Left.mul_lt_of_le_of_lt_one_of_pos` \| \| `mul_lt_one_of_lt_of_le_left₀` \| `Left.mul_lt_of_lt_of_le_one_of_nonneg` \| \| `mul_le_one_right₀` \| `Right.mul_le_one_of_le_of_le` \| \| `mul_lt_one_of_lt_of_le_right₀` (`0 ≤ ·` version) / `mul_lt_one_of_lt_of_le_of_pos_right` \| `Right.mul_lt_one_of_lt_of_le_of_pos` \| \| `mul_lt_one_of_le_of_lt_right₀` \| `Right.mul_lt_one_of_le_of_lt_of_nonneg` \| The following lemmas use `ZeroLEOneClass`. \| New name \| Old name \| \|-------------------------\|-------------------------\| \| `(Left.)one_le_mul₀` \| `Left.one_le_mul_of_le_of_le` \| \| `Left.one_lt_mul_of_le_of_lt₀` \| `Left.one_lt_mul_of_le_of_lt_of_pos` \| \| `Left.one_lt_mul_of_lt_of_le₀` \| `Left.lt_mul_of_lt_of_one_le_of_nonneg` / `one_lt_mul_of_lt_of_le` (still there) \| \| `(Left.)one_lt_mul₀` \| \| \| `Right.one_le_mul₀` \| `Right.one_le_mul_of_le_of_le` \| \| `Right.one_lt_mul_of_lt_of_le₀` \| `Right.one_lt_mul_of_lt_of_le_of_pos` \| \| `Right.one_lt_mul_of_le_of_lt₀` \| `Right.one_lt_mul_of_le_of_lt_of_nonneg` / `one_lt_mul_of_le_of_lt` (still there) / `one_lt_mul` (still there) \| \| `Right.one_lt_mul₀` \| `Right.one_lt_mul_of_lt_of_lt` \| --- Split from #17593. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	awaiting-zulip t-order t-algebra merge-conflict label:t-algebra$	146/44	Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean	2	11	['FR-vdash-bot', 'YaelDillies', 'github-actions', 'j-loreaux']	nobody	223-28570 7 months ago	223-28570 7 months ago	33-64877 33 days
8370	eric-wieser author:eric-wieser	refactor(Analysis/NormedSpace/Exponential): remove the `𝕂` argument from `exp`	This argument is still needed for almost all the lemmas, which means it can longer be found by unification. We keep around `expSeries 𝕂 A`, as it's needed for talking about the radius of convergence over different base fields. This is a prerequisite for #8372, as we can't merge the functions until they have the same interface.\ Zulip thread: [#mathlib4 > Real.exp @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Real.2Eexp/near/401602245) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) This is started from the mathport output on https://github.com/leanprover-community/mathlib/pull/19244	awaiting-zulip t-analysis merge-conflict	432/387	Mathlib/Analysis/CStarAlgebra/Exponential.lean,Mathlib/Analysis/CStarAlgebra/Spectrum.lean,Mathlib/Analysis/Normed/Algebra/Exponential.lean,Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean,Mathlib/Analysis/Normed/Algebra/QuaternionExponential.lean,Mathlib/Analysis/Normed/Algebra/Spectrum.lean,Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean,Mathlib/Analysis/NormedSpace/DualNumber.lean,Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean,Mathlib/Analysis/SpecialFunctions/Exponential.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Series.lean	11	29	['YaelDillies', 'eric-wieser', 'girving', 'github-actions', 'j-loreaux', 'kbuzzard', 'leanprover-community-bot-assistant', 'urkud']	nobody	67-70347 2 months ago	79-12577 2 months ago	29-60989 29 days
15654	TpmKranz author:TpmKranz	feat(Computability): language-preserving maps between NFA and RE	Map REs to NFAs via Thompson's construction and NFAs to REs using GNFAs Last chunk of #12648 --- - [ ] depends on: #15651 - [ ] depends on: #15649 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	awaiting-zulip t-computability new-contributor merge-conflict blocked-by-other-PR	985/2	Mathlib.lean,Mathlib/Computability/GNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean,Mathlib/Computability/RegularExpressions.lean,Mathlib/Data/FinEnum/Option.lean,docs/references.bib	7	3	['github-actions', 'leanprover-community-mathlib4-bot', 'meithecatte']	nobody	56-78247 1 month ago	56-78252 1 month ago	0-179 2 minutes
15651	TpmKranz author:TpmKranz	feat(Computability/NFA): operations for Thompson's construction	Lays the groundwork for a proof of equivalence of RE and NFA, w.r.t. described language. Actual connection to REs comes later, after the groundwork for the opposite direction has been laid. Third chunk of #12648 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	awaiting-zulip t-computability new-contributor merge-conflict awaiting-author	307/5	Mathlib/Computability/NFA.lean	1	15	['TpmKranz', 'YaelDillies', 'dupuisf', 'github-actions', 'leanprover-community-bot-assistant', 'meithecatte']	nobody	43-14453 1 month ago	43-14454 1 month ago	45-84611 45 days
22361	rudynicolop author:rudynicolop	feat(Computability/NFA): nfa closure properties	Add the closure properties union, intersection and reversal for NFA. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	awaiting-zulip t-computability new-contributor merge-conflict awaiting-author	218/2	Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean	2	90	['EtienneC30', 'b-mehta', 'github-actions', 'leanprover-community-bot-assistant', 'meithecatte', 'rudynicolop']	EtienneC30 assignee:EtienneC30	43-13527 1 month ago	43-13529 1 month ago	39-67601 39 days
24409	urkud author:urkud	chore(*): fix `nmem` vs `not_mem` names	--- There are some missing/buggy deprecations, I'm going to fix them later today or tomorrow. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	awaiting-zulip tech debt merge-conflict delegated awaiting-author	317/176	Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Algebra/BigOperators/Group/Finset/Lemmas.lean,Mathlib/Algebra/Group/Indicator.lean,Mathlib/Algebra/Group/Support.lean,Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean,Mathlib/Algebra/Order/Group/Indicator.lean,Mathlib/Algebra/Polynomial/AlgebraMap.lean,Mathlib/Algebra/Polynomial/Degree/Operations.lean,Mathlib/Analysis/Calculus/BumpFunction/Basic.lean,Mathlib/Analysis/Calculus/DSlope.lean,Mathlib/Analysis/Calculus/Deriv/Basic.lean,Mathlib/Analysis/Calculus/Deriv/Support.lean,Mathlib/Analysis/Calculus/FDeriv/Basic.lean,Mathlib/Analysis/Calculus/Rademacher.lean,Mathlib/Analysis/Complex/RemovableSingularity.lean,Mathlib/Analysis/Convex/Cone/InnerDual.lean,Mathlib/Analysis/Convex/Cone/Proper.lean,Mathlib/Analysis/Convolution.lean,Mathlib/Analysis/Distribution/AEEqOfIntegralContDiff.lean,Mathlib/Data/LocallyFinsupp.lean,Mathlib/Data/Set/Basic.lean,Mathlib/Data/Set/Insert.lean,Mathlib/Dynamics/Ergodic/Conservative.lean,Mathlib/Dynamics/Ergodic/Ergodic.lean,Mathlib/Dynamics/Ergodic/Function.lean,Mathlib/Dynamics/PeriodicPts/Defs.lean,Mathlib/Geometry/Manifold/ContMDiff/Basic.lean,Mathlib/Geometry/Manifold/PartitionOfUnity.lean,Mathlib/GroupTheory/CosetCover.lean,Mathlib/LinearAlgebra/Dual/Lemmas.lean,Mathlib/LinearAlgebra/FreeModule/PID.lean,Mathlib/LinearAlgebra/PID.lean,Mathlib/LinearAlgebra/RootSystem/Base.lean,Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean,Mathlib/MeasureTheory/Function/ContinuousMapDense.lean,Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean,Mathlib/MeasureTheory/Function/L2Space.lean,Mathlib/MeasureTheory/Function/LocallyIntegrable.lean,Mathlib/MeasureTheory/Function/LpSpace/Indicator.lean,Mathlib/MeasureTheory/Integral/Average.lean,Mathlib/MeasureTheory/Integral/Bochner/Set.lean,Mathlib/MeasureTheory/Integral/Layercake.lean,Mathlib/MeasureTheory/Integral/Lebesgue/Add.lean,Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean,Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Basic.lean,Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Real.lean,Mathlib/MeasureTheory/Measure/AbsolutelyContinuous.lean,Mathlib/MeasureTheory/Measure/AddContent.lean,Mathlib/MeasureTheory/Measure/DiracProba.lean,Mathlib/MeasureTheory/Measure/Haar/Unique.lean,Mathlib/MeasureTheory/Measure/Restrict.lean,Mathlib/MeasureTheory/Measure/WithDensity.lean,Mathlib/MeasureTheory/OuterMeasure/AE.lean,Mathlib/MeasureTheory/SetSemiring.lean,Mathlib/Order/Filter/AtTopBot/CountablyGenerated.lean,Mathlib/Order/Filter/Cocardinal.lean,Mathlib/Order/Filter/Cofinite.lean,Mathlib/Order/Filter/Tendsto.lean,Mathlib/Order/Filter/Ultrafilter/Basic.lean,Mathlib/Probability/Distributions/Uniform.lean,Mathlib/Probability/Kernel/Basic.lean,Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean,Mathlib/RingTheory/AdicCompletion/LocalRing.lean,Mathlib/RingTheory/Ideal/Maximal.lean,Mathlib/RingTheory/LaurentSeries.lean,Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean,Mathlib/RingTheory/MvPowerSeries/NoZeroDivisors.lean,Mathlib/RingTheory/Spectrum/Maximal/Localization.lean,Mathlib/RingTheory/Spectrum/Prime/RingHom.lean,Mathlib/RingTheory/Spectrum/Prime/Topology.lean,Mathlib/Topology/Algebra/InfiniteSum/Group.lean,Mathlib/Topology/Algebra/Module/Cardinality.lean,Mathlib/Topology/Algebra/Support.lean,Mathlib/Topology/Bases.lean,Mathlib/Topology/ContinuousMap/BoundedCompactlySupported.lean,Mathlib/Topology/Order/Basic.lean,Mathlib/Topology/UrysohnsLemma.lean	77	4	['b-mehta', 'github-actions', 'jcommelin', 'leanprover-community-bot-assistant', 'mathlib-bors']	nobody	29-49425 29 days ago	29-49425 29 days ago	0-55045 15 hours
24396	JovanGerb author:JovanGerb	feat(Order/Defs): refactor in preparation of `to_dual` attribute	When the `to_dual` attribute lands in Mathlib, we will tag many lemmas about order with this tag, which will automatically give us the dual statements. This PR prepares for this by - moving dual declarations closer together - replacing occurrences of `>` and `≥` with `<` and `≤` - consistently applying a new naming convention that helps us to name dual lemmas: we use the keywords `ge` and `gt` in place of `le` and `lt` to indicate that the same pair `a, b` in `a < b` is in the opposite order to the order in which it appeared the first time. - when we have to disambiguate the order of the argument to `<` or `≤`, we sometimes use `gt` or `ge` instead of `lt` or `le`. We also use this to get rid of many primed lemma names. This is a copy of #24376, but it doesn't remove the old lemma names, so doesn't require making changes in >500 files. deprecating these lemmas will be left to a future PR. [#mathlib4 > naming convention for ≤ and <](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/naming.20convention.20for.20.E2.89.A4.20and.20.3C) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	awaiting-zulip t-order merge-conflict	248/230	Mathlib/Algebra/Order/CauSeq/Basic.lean,Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean,Mathlib/Algebra/Polynomial/Degree/Domain.lean,Mathlib/Algebra/Tropical/Basic.lean,Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean,Mathlib/Computability/TuringMachine.lean,Mathlib/Data/Bool/Basic.lean,Mathlib/Data/Char.lean,Mathlib/Data/Complex/Order.lean,Mathlib/Data/ENat/Basic.lean,Mathlib/Data/Int/Order/Basic.lean,Mathlib/Data/Nat/Basic.lean,Mathlib/Data/Nat/Factorization/Defs.lean,Mathlib/Data/Nat/Find.lean,Mathlib/Data/Nat/PartENat.lean,Mathlib/Data/Num/Lemmas.lean,Mathlib/Data/Num/ZNum.lean,Mathlib/Data/PSigma/Order.lean,Mathlib/Data/Prod/Lex.lean,Mathlib/Data/Real/Basic.lean,Mathlib/Data/Setoid/Basic.lean,Mathlib/Data/Setoid/Partition.lean,Mathlib/Data/Sigma/Order.lean,Mathlib/Data/String/Basic.lean,Mathlib/Data/Sum/Order.lean,Mathlib/GroupTheory/MonoidLocalization/Order.lean,Mathlib/NumberTheory/Zsqrtd/Basic.lean,Mathlib/Order/Antisymmetrization.lean,Mathlib/Order/Basic.lean,Mathlib/Order/Booleanisation.lean,Mathlib/Order/Defs/LinearOrder.lean,Mathlib/Order/Defs/PartialOrder.lean,Mathlib/Order/RelClasses.lean,Mathlib/Order/WithBot.lean,Mathlib/Probability/Martingale/Upcrossing.lean,Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicity.lean,Mathlib/SetTheory/Game/Basic.lean,Mathlib/SetTheory/Ordinal/Basic.lean,Mathlib/SetTheory/Ordinal/Notation.lean,Mathlib/SetTheory/Surreal/Basic.lean,Mathlib/Tactic/Linarith/Frontend.lean,MathlibTest/linarith.lean	43	5	['JovanGerb', 'bryangingechen', 'github-actions', 'leanprover-community-bot-assistant']	bryangingechen assignee:bryangingechen	29-11527 29 days ago	29-11529 29 days ago	5-75236 5 days

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

Number	Author	Title	Description	Labels	+/-	Modified files (first 100)	📝	💬	All users who commented or reviewed	Assignee(s)	Updated	Last status change	total time in review
22603	pechersky author:pechersky	chore(Topology): rename pi family from π to X	Only in files that mentioned such a family, via a script: ``` git grep -e "π : . → Type" --name-only \| rg Topology \| xargs -I{} sed -i -e 's/π/X/g' {} ``` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	tech debt t-topology	238/238	Mathlib/Topology/AlexandrovDiscrete.lean,Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean,Mathlib/Topology/Algebra/Module/Equiv.lean,Mathlib/Topology/Algebra/Order/LiminfLimsup.lean,Mathlib/Topology/Bases.lean,Mathlib/Topology/Bornology/Constructions.lean,Mathlib/Topology/Connected/Basic.lean,Mathlib/Topology/Connected/Clopen.lean,Mathlib/Topology/Connected/LocallyConnected.lean,Mathlib/Topology/Connected/TotallyDisconnected.lean,Mathlib/Topology/Constructions.lean,Mathlib/Topology/ContinuousOn.lean,Mathlib/Topology/EMetricSpace/Diam.lean,Mathlib/Topology/EMetricSpace/Pi.lean,Mathlib/Topology/ExtremallyDisconnected.lean,Mathlib/Topology/Inseparable.lean,Mathlib/Topology/MetricSpace/Basic.lean,Mathlib/Topology/MetricSpace/Infsep.lean,Mathlib/Topology/MetricSpace/ProperSpace.lean,Mathlib/Topology/MetricSpace/Pseudo/Pi.lean,Mathlib/Topology/Metrizable/Basic.lean,Mathlib/Topology/Order/Basic.lean,Mathlib/Topology/Separation/Hausdorff.lean,Mathlib/Topology/UniformSpace/Ascoli.lean	24	1	['github-actions']	nobody	22-66656 22 days ago	22-66678 22 days ago	28-60292 28 days
25776	Parcly-Taxel author:Parcly-Taxel	chore: deprime `induction` in `Analysis`	I think this is very marginally dependent on #25770.	tech debt t-analysis	256/208	Mathlib/Analysis/Analytic/Composition.lean,Mathlib/Analysis/Analytic/Constructions.lean,Mathlib/Analysis/Analytic/Inverse.lean,Mathlib/Analysis/BoxIntegral/Basic.lean,Mathlib/Analysis/BoxIntegral/Box/SubboxInduction.lean,Mathlib/Analysis/BoxIntegral/Partition/Additive.lean,Mathlib/Analysis/BoxIntegral/Partition/Split.lean,Mathlib/Analysis/CStarAlgebra/Basic.lean,Mathlib/Analysis/CStarAlgebra/Multiplier.lean,Mathlib/Analysis/Calculus/ContDiff/Basic.lean,Mathlib/Analysis/Calculus/ContDiff/Bounds.lean,Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean,Mathlib/Analysis/Calculus/ContDiff/Operations.lean,Mathlib/Analysis/Calculus/Deriv/ZPow.lean,Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean,Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean,Mathlib/Analysis/Calculus/SmoothSeries.lean,Mathlib/Analysis/Convex/Combination.lean,Mathlib/Analysis/Convex/Radon.lean,Mathlib/Analysis/InnerProductSpace/Projection.lean,Mathlib/Analysis/Normed/Algebra/Exponential.lean,Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean,Mathlib/Analysis/Seminorm.lean,Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean,Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean,Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Deriv.lean,Mathlib/Analysis/SpecialFunctions/Integrals.lean,Mathlib/Analysis/SpecialFunctions/Log/Basic.lean,Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean,Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean,Mathlib/Analysis/SpecialFunctions/Pow/Real.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/EulerSineProd.lean	35	2	['Parcly-Taxel', 'github-actions']	nobody	19-36981 19 days ago	19-37414 19 days ago	19-37458 19 days
25790	Parcly-Taxel author:Parcly-Taxel	chore: remove >6 month old material in `Deprecated`		file-removed tech debt	0/250	Mathlib.lean,Mathlib/Deprecated/Cardinal/Continuum.lean,Mathlib/Deprecated/Cardinal/Finite.lean,Mathlib/Deprecated/Cardinal/PartENat.lean,Mathlib/Deprecated/Order.lean	5	1	['github-actions']	nobody	19-35657 19 days ago	19-35756 19 days ago	19-35744 19 days
25774	Parcly-Taxel author:Parcly-Taxel	chore: deprime `induction` in `AlgebraicTopology/CategoryTheory`	Most replacements that are also in #23676 have been copied over, but some have been optimised further.	tech debt	133/124	Mathlib/AlgebraicTopology/DoldKan/Decomposition.lean,Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean,Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean,Mathlib/AlgebraicTopology/DoldKan/Projections.lean,Mathlib/AlgebraicTopology/SimplexCategory/MorphismProperty.lean,Mathlib/AlgebraicTopology/SimplicialObject/Split.lean,Mathlib/AlgebraicTopology/SimplicialSet/Degenerate.lean,Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean,Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean,Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean,Mathlib/CategoryTheory/Abelian/GrothendieckCategory/Subobject.lean,Mathlib/CategoryTheory/Action/Concrete.lean,Mathlib/CategoryTheory/Action/Monoidal.lean,Mathlib/CategoryTheory/ComposableArrows.lean,Mathlib/CategoryTheory/Extensive.lean,Mathlib/CategoryTheory/Filtered/Basic.lean,Mathlib/CategoryTheory/Galois/Decomposition.lean,Mathlib/CategoryTheory/Galois/EssSurj.lean,Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean,Mathlib/CategoryTheory/Limits/Shapes/SequentialProduct.lean,Mathlib/CategoryTheory/Limits/Types/Colimits.lean,Mathlib/CategoryTheory/Limits/VanKampen.lean,Mathlib/CategoryTheory/Quotient.lean,Mathlib/CategoryTheory/Sites/Sheaf.lean,Mathlib/CategoryTheory/Subobject/Basic.lean,Mathlib/CategoryTheory/Subobject/FactorThru.lean,Mathlib/CategoryTheory/Subobject/Lattice.lean,Mathlib/CategoryTheory/Triangulated/TStructure/Basic.lean	28	3	['Parcly-Taxel', 'eric-wieser', 'github-actions']	nobody	19-23626 19 days ago	19-37863 19 days ago	19-37848 19 days
25770	Parcly-Taxel author:Parcly-Taxel	chore: fix more induction/recursor branch names	These were found using the regex `\\| h. =>` and `def.rec.\(h. :`.	tech debt	134/115	Mathlib/Analysis/Convolution.lean,Mathlib/Data/ENat/Basic.lean,Mathlib/Data/Fin/Tuple/Basic.lean,Mathlib/Data/Fin/Tuple/NatAntidiagonal.lean,Mathlib/Data/Nat/Factorization/Induction.lean,Mathlib/Data/Seq/Computation.lean,Mathlib/Data/Set/Card.lean,Mathlib/Data/WSeq/Basic.lean,Mathlib/FieldTheory/KummerExtension.lean,Mathlib/Logic/Function/Iterate.lean,Mathlib/NumberTheory/ArithmeticFunction.lean,Mathlib/NumberTheory/SumFourSquares.lean,Mathlib/NumberTheory/SumTwoSquares.lean,Mathlib/Order/SuccPred/Archimedean.lean,Mathlib/Order/Synonym.lean	15	10	['Parcly-Taxel', 'eric-wieser', 'github-actions']	nobody	16-44842 16 days ago	19-39688 19 days ago	19-39673 19 days
25915	BoltonBailey author:BoltonBailey	chore(Algebra/Squarefree/Basic): fix erw	This PR addresses an instance of the erw linter in Algebra/Squarefree/Basic. Original PR: https://github.com/leanprover-community/mathlib4/pull/25161	tech debt t-algebra easy label:t-algebra$	1/1	Mathlib/Algebra/Squarefree/Basic.lean	1	1	['github-actions']	nobody	4-63159 4 days ago	8-85081 8 days ago	16-16745 16 days
26404	grunweg author:grunweg	chore: clean up and remove FunProp/Differentiable	- one lemma in that file already exists, hence can be removed (We don't add a deprecation as I presume people will not have used it.) - move the three remaining lemmas in that file to their proper place, and use the now `fun_` naming convention (Omitting deprecations again.) - after this, `FunProp/Differentiable` is empty and need not be imported any more: add a module deprecation --- - [x] depends on: #26355 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	tech debt	23/49	Mathlib/Analysis/Calculus/FDeriv/Comp.lean,Mathlib/Tactic/FunProp/ContDiff.lean,Mathlib/Tactic/FunProp/Differentiable.lean,MathlibTest/fun_prop2.lean	4	3	['github-actions', 'grunweg', 'mathlib4-dependent-issues-bot']	nobody	0-74461 20 hours ago	6-13827 6 days ago	6-13872 6 days