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 14, 2026 at 20:58 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
36395	JovanGerb author:JovanGerb	chore: mark `toSubfield`, `toSubmodule`, `toSubring` as `reducible`	This PR marks `IntermediateField.toSubfield`, `Subalgebra.toSubring` and `Subalgebra.toSubmodule` as `implicit_reducible`, because these are all used to construct instances on substructures, and hence need to be reducible when unifying type classes. This allows removing at least 100 backwards compatability flags (possibly more because I haven't checked these exhaustively) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	ready-to-merge	11/115	Mathlib/Algebra/Algebra/Subalgebra/Basic.lean,Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean,Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean,Mathlib/FieldTheory/IntermediateField/Basic.lean,Mathlib/FieldTheory/LinearDisjoint.lean,Mathlib/RingTheory/DedekindDomain/LinearDisjoint.lean,Mathlib/RingTheory/Ideal/Quotient/HasFiniteQuotients.lean,Mathlib/RingTheory/LinearDisjoint.lean,Mathlib/RingTheory/TensorProduct/Basic.lean	9	15	['JovanGerb', 'eric-wieser', 'github-actions', 'kim-em', 'leanprover-radar', 'mathlib-bors', 'riccardobrasca']	nobody	2-8136 2 days ago	2-56807 2 days ago	2-15970 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/)	t-algebra maintainer-merge awaiting-author 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 and dagurtomas assignee:Vierkantor assignee:dagurtomas	37-12668 1 month ago	37-12672 37 days ago	15-81158 15 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/)	t-analysis maintainer-merge awaiting-author	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	31-34496 1 month ago	31-34496 31 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 FLT maintainer-merge	25/0	Mathlib/Topology/Algebra/Ring/Basic.lean	1	10	['bwangpj', 'dagurtomas', 'eric-wieser', 'github-actions', 'riccardobrasca']	dagurtomas assignee:dagurtomas	23-47362 23 days ago	52-42261 52 days ago	52-49181 52 days
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	large-import maintainer-merge awaiting-author	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	10-26588 10 days ago	10-51604 10 days ago	22-29706 22 days
35760	astrainfinita author:astrainfinita	chore: deprecate `ConditionallyCompleteLinearOrderedField`	Use the new mixin typeclass instead. Also, move the API for conditionally complete linear ordered fields into the `ConditionallyCompleteLinearOrderedField` namespace, and make instances scoped to this namespace. We should usually use `ℝ` instead. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra t-order maintainer-merge label:t-algebra$	124/52	Mathlib.lean,Mathlib/Algebra/Order/CompleteField.lean,Mathlib/Algebra/Order/Ring/StandardPart.lean,Mathlib/Data/Real/CompleteField.lean,Mathlib/Data/Real/Hom.lean	5	6	['Vierkantor', 'astrainfinita', 'github-actions', 'leanprover-radar']	Vierkantor assignee:Vierkantor	7-43870 7 days ago	9-23591 9 days ago	17-16360 17 days
36024	euprunin author:euprunin	chore: golf proofs	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): * `Fin.coe_sub_one`: unchanged 🎉 * `LieAlgebra.engel_isBot_of_isMin.lieCharpoly_coeff_natDegree`: 66 ms before, 35 ms after 🎉 * `WithTop.mul_lt_mul`: unchanged 🎉 * `CFC.spectrum_nonempty`: unchanged 🎉 * `ODE.hasDerivWithinAt_picard_Icc`: unchanged 🎉 * `Matrix.vecMul_injective_iff_isUnit`: 240 ms before, 68 ms after 🎉 * `MeasureTheory.SimpleFunc.measure_preimage_lt_top_of_memLp`: unchanged 🎉 * `Polynomial.content_eq_gcd_range_of_lt`: unchanged 🎉 * `RingHom.finiteType_isStableUnderBaseChange`: 163 ms before, 49 ms after 🎉 * `RingHom.Flat.holdsForLocalizationAway`: 91 ms before, <30 ms after 🎉 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/)	maintainer-merge	20/46	Mathlib/Algebra/Group/Fin/Basic.lean,Mathlib/Algebra/Lie/CartanExists.lean,Mathlib/Algebra/Order/Ring/WithTop.lean,Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean,Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean,Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean,Mathlib/Analysis/ODE/PicardLindelof.lean,Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean,Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean,Mathlib/RingTheory/Polynomial/Content.lean,Mathlib/RingTheory/RingHom/FiniteType.lean,Mathlib/RingTheory/RingHom/Flat.lean	12	14	['euprunin', 'github-actions', 'mathlib-merge-conflicts', 'tb65536', 'vihdzp']	tb65536 assignee:tb65536	5-37407 5 days ago	6-602 6 days ago	9-76682 9 days
36244	kim-em author:kim-em	chore(ci): add continue-on-error to non-critical workflow steps	This PR adds `continue-on-error: true` to non-critical workflow steps that interact with Zulip or perform cosmetic actions (emoji reactions, PR comments, label additions). These should never cause CI failures. Affected workflows: - `zulip_emoji_ci_status.yaml` — emoji update step - `zulip_emoji_closed_pr.yaml` — emoji update step - `zulip_emoji_labelling.yaml` — emoji update step (already had it) - `zulip_emoji_merge_delegate.yaml` — emoji update step (already had it) - `maintainer_bors.yml` / `maintainer_bors_wf_run.yml` — Zulip emoji reaction step - `maintainer_merge.yml` / `maintainer_merge_wf_run.yml` — Zulip message, PR comment, and label steps 🤖 Prepared with Claude Code	CI maintainer-merge merge-conflict	12/0	.github/workflows/maintainer_bors.yml,.github/workflows/maintainer_bors_wf_run.yml,.github/workflows/maintainer_merge.yml,.github/workflows/maintainer_merge_wf_run.yml,.github/workflows/zulip_emoji_ci_status.yaml,.github/workflows/zulip_emoji_closed_pr.yaml,.github/workflows/zulip_emoji_labelling.yaml,.github/workflows/zulip_emoji_merge_delegate.yaml	8	10	['bryangingechen', 'github-actions', 'grunweg', 'joneugster', 'kim-em']	nobody	4-67092 4 days ago	4-68614 4 days ago	3-76773 3 days
30112	gaetanserre author:gaetanserre	feat(Probability.Kernel): add representation of kernel as a map of a uniform measure	Add results about isolation of kernels randomness. In particular, it shows that one can write a Markov kernel as the map by a deterministic of a uniform measure on `[0, 1]`. It corresponds to Lemma 4.22 in "[Foundations of Modern Probability](https://link.springer.com/book/10.1007/978-3-030-61871-1)" by Olav Kallenberg, 2021. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-measure-probability maintainer-merge	129/0	Mathlib.lean,Mathlib/Probability/Kernel/Representation.lean	2	51	['DavidLedvinka', 'EtienneC30', 'RemyDegenne', 'gaetanserre', 'github-actions', 'mathlib4-merge-conflict-bot']	nobody	2-83969 2 days ago	3-811 3 days ago	92-14783 92 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-set-theory t-order maintainer-merge	222/241	Mathlib/CategoryTheory/Presentable/IsCardinalFiltered.lean,Mathlib/Order/Cofinal.lean,Mathlib/SetTheory/Cardinal/Cofinality.lean	3	16	['SnirBroshi', 'YaelDillies', 'b-mehta', 'github-actions', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'vihdzp']	b-mehta assignee:b-mehta	2-71556 2 days ago	15-51376 15 days ago	18-54055 18 days
36457	joelriou author:joelriou	feat(Algebra/Category/ModuleCat/Presheaf): the pushforward by a functor is monoidal	If `F : C ⥤ D` is a functor and `R : Dᵒᵖ ⥤ CommRingCat` is a presheaf of commutative rings, then the pushforward functor from the category of presheaves of modules on `R` to the category of presheaves of modules on `F.op ⋙ R` is monoidal. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-category-theory t-algebra maintainer-merge label:t-algebra$	50/0	Mathlib.lean,Mathlib/Algebra/Category/ModuleCat/Presheaf/Pushforward.lean,Mathlib/Algebra/Category/ModuleCat/Presheaf/PushforwardZeroMonoidal.lean	3	5	['chrisflav', 'github-actions', 'joelriou']	nobody	2-44593 2 days ago	2-46431 2 days ago	3-44448 3 days
36166	wwylele author:wwylele	feat(Data/Nat): formula for cardinal of finsuppAntidiag on Nat	Co-authored-by: Bingyu Xia --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge	82/0	Mathlib.lean,Mathlib/Algebra/Order/Antidiag/FinsuppEquiv.lean	2	16	['BryceT233', 'copilot-pull-request-reviewer', 'github-actions', 'tb65536', 'wwylele']	tb65536 assignee:tb65536	2-33937 2 days ago	2-79053 2 days ago	8-55349 8 days
35400	vlad902 author:vlad902	feat(SimpleGraph): `IsEdgeReachable` lemmas	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics maintainer-merge	19/0	Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean	1	10	['SnirBroshi', 'YaelDillies', 'github-actions', 'vlad902']	YaelDillies assignee:YaelDillies	2-26919 2 days ago	26-31039 26 days ago	26-30692 26 days
26770	Jun2M author:Jun2M	feat(Combinatorics/Graph): subgraph relations on `Graph`	This PR creates a new file `Combinatorics/Graph/Subgraph.lean`. In it, the PR introduces a partial order on graphs by subgraph relation, defines relations `IsInducedSubgraph`, `IsSpanningSubgraph` and `IsClosedSubgraph`. Co-authored-by: Peter Nelson --- - [x] depends on: #34783 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics maintainer-merge	362/0	Mathlib.lean,Mathlib/Combinatorics/Graph/Subgraph.lean	2	81	['Jun2M', 'YaelDillies', 'github-actions', 'lauramonk', 'mathlib-dependent-issues', 'mathlib4-merge-conflict-bot']	YaelDillies assignee:YaelDillies	2-14206 2 days ago	8-13416 8 days ago	166-61118 166 days
36316	JovanGerb author:JovanGerb	chore: import `Type*` in `Mathlib.Init`	The implementation of `Type*` is very short, so I've put its minimal dependencies in the same file, `Mathlib.Tactic.TypeStar`, and imported this in `Mathlib.Init`. This allows us to get rid of many explicit imports of this file, and lets it be available everywhere in mathlib. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	large-import maintainer-merge	58/87	Mathlib/Algebra/Notation.lean,Mathlib/Algebra/Notation/Defs.lean,Mathlib/Algebra/Notation/Lemmas.lean,Mathlib/Control/Functor.lean,Mathlib/Data/Bool/AllAny.lean,Mathlib/Data/Bracket.lean,Mathlib/Data/Int/Cast/Pi.lean,Mathlib/Data/Int/Init.lean,Mathlib/Data/List/Lookmap.lean,Mathlib/Data/List/ModifyLast.lean,Mathlib/Data/List/TFAE.lean,Mathlib/Data/Nat/Init.lean,Mathlib/Data/Num/Basic.lean,Mathlib/Data/Option/Defs.lean,Mathlib/Data/Option/NAry.lean,Mathlib/Data/Ordering/Basic.lean,Mathlib/Data/Prod/PProd.lean,Mathlib/Data/Rat/Init.lean,Mathlib/Data/Tree/Basic.lean,Mathlib/Data/Vector3.lean,Mathlib/Init.lean,Mathlib/Lean/Elab/Term.lean,Mathlib/Logic/ExistsUnique.lean,Mathlib/Logic/Function/Coequalizer.lean,Mathlib/Logic/Function/CompTypeclasses.lean,Mathlib/Logic/Function/Defs.lean,Mathlib/Logic/Function/ULift.lean,Mathlib/Logic/Nonempty.lean,Mathlib/Logic/Nontrivial/Defs.lean,Mathlib/Order/Bounds/Defs.lean,Mathlib/Order/Defs/LinearOrder.lean,Mathlib/Order/Defs/PartialOrder.lean,Mathlib/Order/Notation.lean,Mathlib/Tactic/Basic.lean,Mathlib/Tactic/CategoryTheory/CategoryStar.lean,Mathlib/Tactic/FunProp/Mor.lean,Mathlib/Tactic/GCongr/Core.lean,Mathlib/Tactic/Inhabit.lean,Mathlib/Tactic/Linter/DirectoryDependency.lean,Mathlib/Tactic/MkIffOfInductiveProp.lean,Mathlib/Tactic/TypeStar.lean,MathlibTest/BasicFiles/Init.lean,MathlibTest/BasicFiles/TacticBasic.lean,MathlibTest/ImplicitUniverses.lean	44	4	['SnirBroshi', 'github-actions', 'j-loreaux']	j-loreaux assignee:j-loreaux	2-12647 2 days ago	7-21604 7 days ago	7-24625 7 days
35867	edegeltje author:edegeltje	feat(CategoryTheory/Topos): Define subobject classifier for sheaf of types	This PR defines `Sheaf.classifier J : Classifier (Sheaf J (Type (max u v))`, which is the last ingredient missing to sheaf categories being elementary topoi. adapted from: https://github.com/edegeltje/CwFTT/blob/591d4505390172ae70e1bc97544d293a35cc0b3f/CwFTT/Classifier/Sheaf.lean --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-category-theory maintainer-merge	309/37	Mathlib.lean,Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean,Mathlib/CategoryTheory/Limits/Types/Products.lean,Mathlib/CategoryTheory/Sites/Closed.lean,Mathlib/CategoryTheory/Sites/Sheaf.lean,Mathlib/CategoryTheory/Topos/Sheaf.lean	6	68	['chrisflav', 'dagurtomas', 'edegeltje', 'github-actions', 'joelriou', 'mathlib-merge-conflicts', 'mathlib-splicebot', 'robin-carlier']	chrisflav assignee:chrisflav	1-81546 1 day ago	2-8394 2 days ago	12-21963 12 days
36470	joelriou author:joelriou	feat(CategoryTheory/Monoidal): the left adjoint of a lax monoidal functor is oplax monoidal	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-category-theory maintainer-merge	79/0	Mathlib/CategoryTheory/Monoidal/Functor.lean	1	4	['dagurtomas', 'github-actions']	nobody	1-38942 1 day ago	1-39008 1 day ago	3-29636 3 days
33935	mckoen author:mckoen	feat(CategoryTheory/Monoidal/Arrow): define monoidal structure on arrow category	defines a monoidal category structure on the arrow category of a cartesian closed category. --- - [x] depends on: #33974 - [x] depends on: #34887 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-category-theory maintainer-merge awaiting-author	511/0	Mathlib.lean,Mathlib/CategoryTheory/Monoidal/Arrow.lean,Mathlib/CategoryTheory/Monoidal/Limits/Shapes/Pullback.lean	3	23	['dagurtomas', 'github-actions', 'joelriou', 'mathlib-dependent-issues', 'mckoen']	joelriou assignee:joelriou	1-33383 1 day ago	2-2161 2 days ago	11-73773 11 days
35643	chrisflav author:chrisflav	chore(Algebra): make `TensorProduct.equivOfCompatibleSMul` more linear	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra maintainer-merge label:t-algebra$	64/47	Mathlib/LinearAlgebra/TensorProduct/Associator.lean,Mathlib/LinearAlgebra/TensorProduct/Basic.lean,Mathlib/RingTheory/Coalgebra/TensorProduct.lean,Mathlib/RingTheory/LinearDisjoint.lean,Mathlib/RingTheory/Localization/BaseChange.lean,Mathlib/RingTheory/Smooth/Fiber.lean,Mathlib/RingTheory/TensorProduct/Maps.lean,Mathlib/RingTheory/TensorProduct/Nontrivial.lean	8	17	['chrisflav', 'github-actions', 'kckennylau', 'robin-carlier']	kim-em assignee:kim-em	1-22856 1 day ago	1-27890 1 day ago	19-3423 19 days
34922	vasnesterov author:vasnesterov	feat(Tactic/ComputeAsymptotics/Multiseries): Multiseries definition and structural lemmas	Define `Multiseries` and `MultiseriesExpansion` and restate some `Seq` API for `Multiseries`. --- This is a part of the `compute_asymptotics` tactic (#28291). [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-data t-meta maintainer-merge	411/0	Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/ComputeAsymptotics/Multiseries/Defs.lean	3	17	['Vierkantor', 'github-actions', 'joneugster', 'mathlib-merge-conflicts', 'vasnesterov']	Vierkantor and joneugster assignee:Vierkantor assignee:joneugster	1-22278 1 day ago	5-25895 5 days ago	26-36011 26 days
35680	joelriou author:joelriou	feat(CategoryTheory/Sites): alternative constructor for points	By definition, given a point of a site `(C, J)`, the fiber of a presheaf `P` is defined as a filtered colimit indexed by the opposite category of the category of elements of the functor from `C` to types that is part of the definition of the point. In this PR, we introduce a constructor for points which allows to provide a functor `p : N ⥤ C` from a cofiltered and initially small instead. This construction is applied to the construction of the image of a point by a cocontinuous functor. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-category-theory maintainer-merge	337/0	Mathlib.lean,Mathlib/CategoryTheory/Sites/Point/Basic.lean,Mathlib/CategoryTheory/Sites/Point/Map.lean,Mathlib/CategoryTheory/Sites/Point/OfIsCofiltered.lean	4	16	['bryangingechen', 'github-actions', 'mathlib-merge-conflicts', 'robin-carlier']	adamtopaz assignee:adamtopaz	1-22113 1 day ago	1-22153 1 day ago	8-24185 8 days
36182	joelriou author:joelriou	feat(Algebra/Homology/SpectralObject): homology of the differentials	--- - [x] depends on: #35374 - [x] depends on: #35375 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra t-category-theory maintainer-merge label:t-algebra$	166/0	Mathlib.lean,Mathlib/Algebra/Homology/SpectralObject/Homology.lean	2	48	['faenuccio', 'github-actions', 'joelriou', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'robin-carlier', 'smorel394']	faenuccio assignee:faenuccio	1-16345 1 day ago	1-16445 1 day ago	1-84114 1 day
36197	RemyDegenne author:RemyDegenne	feat: integrability of a convex function of R.N. derivatives	For `f` a convex continuous real function, if `f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η))` is `(ν ⊗ₘ η)`-integrable, then `f (μ.rnDeriv ν)` is `ν`-integrable. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-measure-probability large-import maintainer-merge	146/2	Mathlib/Analysis/Convex/Approximation.lean,Mathlib/MeasureTheory/Measure/Decomposition/IntegralRNDeriv.lean,Mathlib/MeasureTheory/Measure/Decomposition/RadonNikodym.lean	3	12	['EtienneC30', 'RemyDegenne', 'github-actions']	EtienneC30 assignee:EtienneC30	1-15960 1 day ago	1-40327 1 day ago	6-49143 6 days
33780	ooovi author:ooovi	feat(Geometry/Convex/Cone): lineality space of pointed cones	Define the lineality space `PointedCone.lineal` as the submodule `C ⊓ -C`. Prove that it is the largest submodule of the cone, which is sometimes used as an alternative definition. Co-authored-by: Martin Winter --- dependency of #33664 - [x] depends on #33761 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-convex-geometry maintainer-merge	36/1	Mathlib/Geometry/Convex/Cone/Pointed.lean	1	23	['YaelDillies', 'artie2000', 'eric-wieser', 'github-actions', 'martinwintermath', 'mathlib4-merge-conflict-bot', 'ooovi', 'vihdzp']	nobody	1-3717 1 day ago	1-4399 1 day ago	28-2767 28 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/)	t-algebra maintainer-merge awaiting-author 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 and dagurtomas assignee:Vierkantor assignee:dagurtomas	37-12668 1 month ago	37-12672 37 days ago	15-81158 15 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/)	t-analysis maintainer-merge awaiting-author	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	31-34496 1 month ago	31-34496 31 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 FLT maintainer-merge	25/0	Mathlib/Topology/Algebra/Ring/Basic.lean	1	10	['bwangpj', 'dagurtomas', 'eric-wieser', 'github-actions', 'riccardobrasca']	dagurtomas assignee:dagurtomas	23-47362 23 days ago	52-42261 52 days ago	52-49181 52 days
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	large-import maintainer-merge awaiting-author	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	10-26588 10 days ago	10-51604 10 days ago	22-29706 22 days
35760	astrainfinita author:astrainfinita	chore: deprecate `ConditionallyCompleteLinearOrderedField`	Use the new mixin typeclass instead. Also, move the API for conditionally complete linear ordered fields into the `ConditionallyCompleteLinearOrderedField` namespace, and make instances scoped to this namespace. We should usually use `ℝ` instead. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra t-order maintainer-merge label:t-algebra$	124/52	Mathlib.lean,Mathlib/Algebra/Order/CompleteField.lean,Mathlib/Algebra/Order/Ring/StandardPart.lean,Mathlib/Data/Real/CompleteField.lean,Mathlib/Data/Real/Hom.lean	5	6	['Vierkantor', 'astrainfinita', 'github-actions', 'leanprover-radar']	Vierkantor assignee:Vierkantor	7-43870 7 days ago	9-23591 9 days ago	17-16360 17 days
36024	euprunin author:euprunin	chore: golf proofs	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): * `Fin.coe_sub_one`: unchanged 🎉 * `LieAlgebra.engel_isBot_of_isMin.lieCharpoly_coeff_natDegree`: 66 ms before, 35 ms after 🎉 * `WithTop.mul_lt_mul`: unchanged 🎉 * `CFC.spectrum_nonempty`: unchanged 🎉 * `ODE.hasDerivWithinAt_picard_Icc`: unchanged 🎉 * `Matrix.vecMul_injective_iff_isUnit`: 240 ms before, 68 ms after 🎉 * `MeasureTheory.SimpleFunc.measure_preimage_lt_top_of_memLp`: unchanged 🎉 * `Polynomial.content_eq_gcd_range_of_lt`: unchanged 🎉 * `RingHom.finiteType_isStableUnderBaseChange`: 163 ms before, 49 ms after 🎉 * `RingHom.Flat.holdsForLocalizationAway`: 91 ms before, <30 ms after 🎉 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/)	maintainer-merge	20/46	Mathlib/Algebra/Group/Fin/Basic.lean,Mathlib/Algebra/Lie/CartanExists.lean,Mathlib/Algebra/Order/Ring/WithTop.lean,Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean,Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean,Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean,Mathlib/Analysis/ODE/PicardLindelof.lean,Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean,Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean,Mathlib/RingTheory/Polynomial/Content.lean,Mathlib/RingTheory/RingHom/FiniteType.lean,Mathlib/RingTheory/RingHom/Flat.lean	12	14	['euprunin', 'github-actions', 'mathlib-merge-conflicts', 'tb65536', 'vihdzp']	tb65536 assignee:tb65536	5-37407 5 days ago	6-602 6 days ago	9-76682 9 days
36244	kim-em author:kim-em	chore(ci): add continue-on-error to non-critical workflow steps	This PR adds `continue-on-error: true` to non-critical workflow steps that interact with Zulip or perform cosmetic actions (emoji reactions, PR comments, label additions). These should never cause CI failures. Affected workflows: - `zulip_emoji_ci_status.yaml` — emoji update step - `zulip_emoji_closed_pr.yaml` — emoji update step - `zulip_emoji_labelling.yaml` — emoji update step (already had it) - `zulip_emoji_merge_delegate.yaml` — emoji update step (already had it) - `maintainer_bors.yml` / `maintainer_bors_wf_run.yml` — Zulip emoji reaction step - `maintainer_merge.yml` / `maintainer_merge_wf_run.yml` — Zulip message, PR comment, and label steps 🤖 Prepared with Claude Code	CI maintainer-merge merge-conflict	12/0	.github/workflows/maintainer_bors.yml,.github/workflows/maintainer_bors_wf_run.yml,.github/workflows/maintainer_merge.yml,.github/workflows/maintainer_merge_wf_run.yml,.github/workflows/zulip_emoji_ci_status.yaml,.github/workflows/zulip_emoji_closed_pr.yaml,.github/workflows/zulip_emoji_labelling.yaml,.github/workflows/zulip_emoji_merge_delegate.yaml	8	10	['bryangingechen', 'github-actions', 'grunweg', 'joneugster', 'kim-em']	nobody	4-67092 4 days ago	4-68614 4 days ago	3-76773 3 days
30112	gaetanserre author:gaetanserre	feat(Probability.Kernel): add representation of kernel as a map of a uniform measure	Add results about isolation of kernels randomness. In particular, it shows that one can write a Markov kernel as the map by a deterministic of a uniform measure on `[0, 1]`. It corresponds to Lemma 4.22 in "[Foundations of Modern Probability](https://link.springer.com/book/10.1007/978-3-030-61871-1)" by Olav Kallenberg, 2021. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-measure-probability maintainer-merge	129/0	Mathlib.lean,Mathlib/Probability/Kernel/Representation.lean	2	51	['DavidLedvinka', 'EtienneC30', 'RemyDegenne', 'gaetanserre', 'github-actions', 'mathlib4-merge-conflict-bot']	nobody	2-83969 2 days ago	3-811 3 days ago	92-14783 92 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-set-theory t-order maintainer-merge	222/241	Mathlib/CategoryTheory/Presentable/IsCardinalFiltered.lean,Mathlib/Order/Cofinal.lean,Mathlib/SetTheory/Cardinal/Cofinality.lean	3	16	['SnirBroshi', 'YaelDillies', 'b-mehta', 'github-actions', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'vihdzp']	b-mehta assignee:b-mehta	2-71556 2 days ago	15-51376 15 days ago	18-54055 18 days
36457	joelriou author:joelriou	feat(Algebra/Category/ModuleCat/Presheaf): the pushforward by a functor is monoidal	If `F : C ⥤ D` is a functor and `R : Dᵒᵖ ⥤ CommRingCat` is a presheaf of commutative rings, then the pushforward functor from the category of presheaves of modules on `R` to the category of presheaves of modules on `F.op ⋙ R` is monoidal. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-category-theory t-algebra maintainer-merge label:t-algebra$	50/0	Mathlib.lean,Mathlib/Algebra/Category/ModuleCat/Presheaf/Pushforward.lean,Mathlib/Algebra/Category/ModuleCat/Presheaf/PushforwardZeroMonoidal.lean	3	5	['chrisflav', 'github-actions', 'joelriou']	nobody	2-44593 2 days ago	2-46431 2 days ago	3-44448 3 days
36166	wwylele author:wwylele	feat(Data/Nat): formula for cardinal of finsuppAntidiag on Nat	Co-authored-by: Bingyu Xia --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge	82/0	Mathlib.lean,Mathlib/Algebra/Order/Antidiag/FinsuppEquiv.lean	2	16	['BryceT233', 'copilot-pull-request-reviewer', 'github-actions', 'tb65536', 'wwylele']	tb65536 assignee:tb65536	2-33937 2 days ago	2-79053 2 days ago	8-55349 8 days
35400	vlad902 author:vlad902	feat(SimpleGraph): `IsEdgeReachable` lemmas	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics maintainer-merge	19/0	Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean	1	10	['SnirBroshi', 'YaelDillies', 'github-actions', 'vlad902']	YaelDillies assignee:YaelDillies	2-26919 2 days ago	26-31039 26 days ago	26-30692 26 days
26770	Jun2M author:Jun2M	feat(Combinatorics/Graph): subgraph relations on `Graph`	This PR creates a new file `Combinatorics/Graph/Subgraph.lean`. In it, the PR introduces a partial order on graphs by subgraph relation, defines relations `IsInducedSubgraph`, `IsSpanningSubgraph` and `IsClosedSubgraph`. Co-authored-by: Peter Nelson --- - [x] depends on: #34783 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics maintainer-merge	362/0	Mathlib.lean,Mathlib/Combinatorics/Graph/Subgraph.lean	2	81	['Jun2M', 'YaelDillies', 'github-actions', 'lauramonk', 'mathlib-dependent-issues', 'mathlib4-merge-conflict-bot']	YaelDillies assignee:YaelDillies	2-14206 2 days ago	8-13416 8 days ago	166-61118 166 days
36316	JovanGerb author:JovanGerb	chore: import `Type*` in `Mathlib.Init`	The implementation of `Type*` is very short, so I've put its minimal dependencies in the same file, `Mathlib.Tactic.TypeStar`, and imported this in `Mathlib.Init`. This allows us to get rid of many explicit imports of this file, and lets it be available everywhere in mathlib. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	large-import maintainer-merge	58/87	Mathlib/Algebra/Notation.lean,Mathlib/Algebra/Notation/Defs.lean,Mathlib/Algebra/Notation/Lemmas.lean,Mathlib/Control/Functor.lean,Mathlib/Data/Bool/AllAny.lean,Mathlib/Data/Bracket.lean,Mathlib/Data/Int/Cast/Pi.lean,Mathlib/Data/Int/Init.lean,Mathlib/Data/List/Lookmap.lean,Mathlib/Data/List/ModifyLast.lean,Mathlib/Data/List/TFAE.lean,Mathlib/Data/Nat/Init.lean,Mathlib/Data/Num/Basic.lean,Mathlib/Data/Option/Defs.lean,Mathlib/Data/Option/NAry.lean,Mathlib/Data/Ordering/Basic.lean,Mathlib/Data/Prod/PProd.lean,Mathlib/Data/Rat/Init.lean,Mathlib/Data/Tree/Basic.lean,Mathlib/Data/Vector3.lean,Mathlib/Init.lean,Mathlib/Lean/Elab/Term.lean,Mathlib/Logic/ExistsUnique.lean,Mathlib/Logic/Function/Coequalizer.lean,Mathlib/Logic/Function/CompTypeclasses.lean,Mathlib/Logic/Function/Defs.lean,Mathlib/Logic/Function/ULift.lean,Mathlib/Logic/Nonempty.lean,Mathlib/Logic/Nontrivial/Defs.lean,Mathlib/Order/Bounds/Defs.lean,Mathlib/Order/Defs/LinearOrder.lean,Mathlib/Order/Defs/PartialOrder.lean,Mathlib/Order/Notation.lean,Mathlib/Tactic/Basic.lean,Mathlib/Tactic/CategoryTheory/CategoryStar.lean,Mathlib/Tactic/FunProp/Mor.lean,Mathlib/Tactic/GCongr/Core.lean,Mathlib/Tactic/Inhabit.lean,Mathlib/Tactic/Linter/DirectoryDependency.lean,Mathlib/Tactic/MkIffOfInductiveProp.lean,Mathlib/Tactic/TypeStar.lean,MathlibTest/BasicFiles/Init.lean,MathlibTest/BasicFiles/TacticBasic.lean,MathlibTest/ImplicitUniverses.lean	44	4	['SnirBroshi', 'github-actions', 'j-loreaux']	j-loreaux assignee:j-loreaux	2-12647 2 days ago	7-21604 7 days ago	7-24625 7 days
35867	edegeltje author:edegeltje	feat(CategoryTheory/Topos): Define subobject classifier for sheaf of types	This PR defines `Sheaf.classifier J : Classifier (Sheaf J (Type (max u v))`, which is the last ingredient missing to sheaf categories being elementary topoi. adapted from: https://github.com/edegeltje/CwFTT/blob/591d4505390172ae70e1bc97544d293a35cc0b3f/CwFTT/Classifier/Sheaf.lean --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-category-theory maintainer-merge	309/37	Mathlib.lean,Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean,Mathlib/CategoryTheory/Limits/Types/Products.lean,Mathlib/CategoryTheory/Sites/Closed.lean,Mathlib/CategoryTheory/Sites/Sheaf.lean,Mathlib/CategoryTheory/Topos/Sheaf.lean	6	68	['chrisflav', 'dagurtomas', 'edegeltje', 'github-actions', 'joelriou', 'mathlib-merge-conflicts', 'mathlib-splicebot', 'robin-carlier']	chrisflav assignee:chrisflav	1-81546 1 day ago	2-8394 2 days ago	12-21963 12 days
36470	joelriou author:joelriou	feat(CategoryTheory/Monoidal): the left adjoint of a lax monoidal functor is oplax monoidal	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-category-theory maintainer-merge	79/0	Mathlib/CategoryTheory/Monoidal/Functor.lean	1	4	['dagurtomas', 'github-actions']	nobody	1-38942 1 day ago	1-39008 1 day ago	3-29636 3 days
33935	mckoen author:mckoen	feat(CategoryTheory/Monoidal/Arrow): define monoidal structure on arrow category	defines a monoidal category structure on the arrow category of a cartesian closed category. --- - [x] depends on: #33974 - [x] depends on: #34887 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-category-theory maintainer-merge awaiting-author	511/0	Mathlib.lean,Mathlib/CategoryTheory/Monoidal/Arrow.lean,Mathlib/CategoryTheory/Monoidal/Limits/Shapes/Pullback.lean	3	23	['dagurtomas', 'github-actions', 'joelriou', 'mathlib-dependent-issues', 'mckoen']	joelriou assignee:joelriou	1-33383 1 day ago	2-2161 2 days ago	11-73773 11 days
35643	chrisflav author:chrisflav	chore(Algebra): make `TensorProduct.equivOfCompatibleSMul` more linear	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra maintainer-merge label:t-algebra$	64/47	Mathlib/LinearAlgebra/TensorProduct/Associator.lean,Mathlib/LinearAlgebra/TensorProduct/Basic.lean,Mathlib/RingTheory/Coalgebra/TensorProduct.lean,Mathlib/RingTheory/LinearDisjoint.lean,Mathlib/RingTheory/Localization/BaseChange.lean,Mathlib/RingTheory/Smooth/Fiber.lean,Mathlib/RingTheory/TensorProduct/Maps.lean,Mathlib/RingTheory/TensorProduct/Nontrivial.lean	8	17	['chrisflav', 'github-actions', 'kckennylau', 'robin-carlier']	kim-em assignee:kim-em	1-22856 1 day ago	1-27890 1 day ago	19-3423 19 days
34922	vasnesterov author:vasnesterov	feat(Tactic/ComputeAsymptotics/Multiseries): Multiseries definition and structural lemmas	Define `Multiseries` and `MultiseriesExpansion` and restate some `Seq` API for `Multiseries`. --- This is a part of the `compute_asymptotics` tactic (#28291). [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-data t-meta maintainer-merge	411/0	Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/ComputeAsymptotics/Multiseries/Defs.lean	3	17	['Vierkantor', 'github-actions', 'joneugster', 'mathlib-merge-conflicts', 'vasnesterov']	Vierkantor and joneugster assignee:Vierkantor assignee:joneugster	1-22278 1 day ago	5-25895 5 days ago	26-36011 26 days
35680	joelriou author:joelriou	feat(CategoryTheory/Sites): alternative constructor for points	By definition, given a point of a site `(C, J)`, the fiber of a presheaf `P` is defined as a filtered colimit indexed by the opposite category of the category of elements of the functor from `C` to types that is part of the definition of the point. In this PR, we introduce a constructor for points which allows to provide a functor `p : N ⥤ C` from a cofiltered and initially small instead. This construction is applied to the construction of the image of a point by a cocontinuous functor. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-category-theory maintainer-merge	337/0	Mathlib.lean,Mathlib/CategoryTheory/Sites/Point/Basic.lean,Mathlib/CategoryTheory/Sites/Point/Map.lean,Mathlib/CategoryTheory/Sites/Point/OfIsCofiltered.lean	4	16	['bryangingechen', 'github-actions', 'mathlib-merge-conflicts', 'robin-carlier']	adamtopaz assignee:adamtopaz	1-22113 1 day ago	1-22153 1 day ago	8-24185 8 days
36182	joelriou author:joelriou	feat(Algebra/Homology/SpectralObject): homology of the differentials	--- - [x] depends on: #35374 - [x] depends on: #35375 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra t-category-theory maintainer-merge label:t-algebra$	166/0	Mathlib.lean,Mathlib/Algebra/Homology/SpectralObject/Homology.lean	2	48	['faenuccio', 'github-actions', 'joelriou', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'robin-carlier', 'smorel394']	faenuccio assignee:faenuccio	1-16345 1 day ago	1-16445 1 day ago	1-84114 1 day
36197	RemyDegenne author:RemyDegenne	feat: integrability of a convex function of R.N. derivatives	For `f` a convex continuous real function, if `f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η))` is `(ν ⊗ₘ η)`-integrable, then `f (μ.rnDeriv ν)` is `ν`-integrable. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-measure-probability large-import maintainer-merge	146/2	Mathlib/Analysis/Convex/Approximation.lean,Mathlib/MeasureTheory/Measure/Decomposition/IntegralRNDeriv.lean,Mathlib/MeasureTheory/Measure/Decomposition/RadonNikodym.lean	3	12	['EtienneC30', 'RemyDegenne', 'github-actions']	EtienneC30 assignee:EtienneC30	1-15960 1 day ago	1-40327 1 day ago	6-49143 6 days
33780	ooovi author:ooovi	feat(Geometry/Convex/Cone): lineality space of pointed cones	Define the lineality space `PointedCone.lineal` as the submodule `C ⊓ -C`. Prove that it is the largest submodule of the cone, which is sometimes used as an alternative definition. Co-authored-by: Martin Winter --- dependency of #33664 - [x] depends on #33761 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-convex-geometry maintainer-merge	36/1	Mathlib/Geometry/Convex/Cone/Pointed.lean	1	23	['YaelDillies', 'artie2000', 'eric-wieser', 'github-actions', 'martinwintermath', 'mathlib4-merge-conflict-bot', 'ooovi', 'vihdzp']	nobody	1-3717 1 day ago	1-4399 1 day ago	28-2767 28 days
35616	SnirBroshi author:SnirBroshi	feat(Combinatorics/SimpleGraph/Copy): `IsContained` and `IsIndContained` are preorders	This makes `calc` work and provides `Std.Refl` and `IsTrans` instances. `grw` still doesn't work and mixing the two predicates in `calc` (to prove `IsContained`) also doesn't work. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics maintainer-merge	20/0	Mathlib/Combinatorics/SimpleGraph/Copy.lean	1	2	['YaelDillies', 'github-actions']	YaelDillies assignee:YaelDillies	0-47712 13 hours ago	20-75634 20 days ago	20-75287 20 days
36097	matthewjasper author:matthewjasper	chore: make pseudoparents of algebraic substructures reducible	Make functions that take an algebraic substructure and return a sibling class reducible, this matches actual parents and resolves some usage of `set_option backward.isDefEq.respectTransparency false`. For example it ensures that the field instance on `IntermediateField` has a compatible `Semiring` instance to the one from it extending a `Subalgebra`. Also remove @[simp] from `adjoin_toSubsemiring`, since it prevents other simp lemmas on `adjoin` from applying. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra maintainer-merge label:t-algebra$	23/16	Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean,Mathlib/Algebra/Algebra/Subalgebra/Basic.lean,Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean,Mathlib/Algebra/Field/Subfield/Defs.lean,Mathlib/Algebra/Ring/Subring/Defs.lean,Mathlib/Algebra/Ring/Subsemiring/Defs.lean,Mathlib/Algebra/Star/NonUnitalSubalgebra.lean,Mathlib/Algebra/Star/Subalgebra.lean,Mathlib/FieldTheory/IntermediateField/Basic.lean,Mathlib/RingTheory/NonUnitalSubring/Defs.lean,Mathlib/RingTheory/TensorProduct/Basic.lean	11	3	['dagurtomas', 'github-actions']	dagurtomas assignee:dagurtomas	0-40413 11 hours ago	9-79243 9 days ago	9-82245 9 days
36471	eric-wieser author:eric-wieser	feat: more API for Function.IsPartialInv	This also renames some lemmas to enable dot notation. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-logic maintainer-merge	33/22	Mathlib/Data/Set/Finite/Basic.lean,Mathlib/Logic/Encodable/Basic.lean,Mathlib/Logic/Function/Basic.lean	3	13	['Komyyy', 'eric-wieser', 'github-actions']	nobody	0-40269 11 hours ago	1-71869 1 day ago	2-75892 2 days
35360	vlad902 author:vlad902	chore: rename `cycleGraph_EulerianCircuit` to `cycleGraph.cycle`	Per [this](https://github.com/leanprover-community/mathlib4/pull/34797#discussion_r2807963752) review feedback, this definition is inappropriately named with an underscore and should be renamed. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics maintainer-merge	21/17	Mathlib/Combinatorics/SimpleGraph/Circulant.lean,Mathlib/Combinatorics/SimpleGraph/ConcreteColorings.lean	2	6	['YaelDillies', 'github-actions', 'vlad902']	YaelDillies assignee:YaelDillies	0-28032 7 hours ago	0-47674 13 hours ago	26-60102 26 days
36391	xroblot author:xroblot	feat(FieldTheory/Galois/IsGaloisGroup): Galois groups for quotients by normal subgroups	Assume `G `is a finite Galois group for `L/K`, `N ⊴ G` is normal, and `F = Fix(N)`. This PR proves: - `G ⧸ N` acts on `F` via `(g.N) • x := g • x` as a `MulSemiringAction`. Under `SMulCommClass G K L`, it is also `SMulCommClass (G ⧸ N) K F` - instance `quotient` : `IsGaloisGroup (G ⧸ N) K F` — the quotient group is a Galois group for the intermediate extension `F/K`. - theorem `quotientMap` under the hypothesis ` E ≤ F`: `IsGaloisGroup (H.map (QuotientGroup.mk' N)) E F` — if `H` is the Galois group for `L/E`, the image of `H` under the quotient map is a Galois group for `F/E`. Also add the tag `@[implicit_reducible]` to `IntermediateField.toSubfield` and remove `set_option backward.isDefEq.respectTransparency` from the file `HilbertTheory.lean`. --- - [x] depends on: #36365 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra maintainer-merge awaiting-author label:t-algebra$	82/0	Mathlib/FieldTheory/Galois/IsGaloisGroup.lean	1	19	['github-actions', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'robin-carlier', 'xroblot']	nobody	0-18907 5 hours ago	1-17860 1 day ago	0-12650 3 hours

PRs blocked on a zulip discussion

Number	Author	Title	Description	Labels	+/-	Modified files (first 100)	📝	💬	All users who commented or reviewed	Assignee(s)	Updated	Last status change	total time in review
17623	astrainfinita author:astrainfinita	feat(Algebra/Order/GroupWithZero/Unbundled): add some lemmas	Some lemmas in `Algebra.Order.GroupWithZero.Unbundled` have incorrect or unsatisfactory names, or assumptions that can be omitted using `ZeroLEOneClass`. The lemmas added in this PR are versions of existing lemmas that use the correct or better name or `ZeroLEOneClass` to omit an assumption. The original lemmas will be deprecated in #17593. \| New name \| Old name \| \|-------------------------\|-------------------------\| \| `mul_le_one_left₀` \| `Left.mul_le_one_of_le_of_le` \| \| `mul_lt_one_of_le_of_lt_left₀` (`0 ≤ ·` version) / `mul_lt_one_of_le_of_lt_of_pos_left` \| `Left.mul_lt_of_le_of_lt_one_of_pos` \| \| `mul_lt_one_of_lt_of_le_left₀` \| `Left.mul_lt_of_lt_of_le_one_of_nonneg` \| \| `mul_le_one_right₀` \| `Right.mul_le_one_of_le_of_le` \| \| `mul_lt_one_of_lt_of_le_right₀` (`0 ≤ ·` version) / `mul_lt_one_of_lt_of_le_of_pos_right` \| `Right.mul_lt_one_of_lt_of_le_of_pos` \| \| `mul_lt_one_of_le_of_lt_right₀` \| `Right.mul_lt_one_of_le_of_lt_of_nonneg` \| The following lemmas use `ZeroLEOneClass`. \| New name \| Old name \| \|-------------------------\|-------------------------\| \| `(Left.)one_le_mul₀` \| `Left.one_le_mul_of_le_of_le` \| \| `Left.one_lt_mul_of_le_of_lt₀` \| `Left.one_lt_mul_of_le_of_lt_of_pos` \| \| `Left.one_lt_mul_of_lt_of_le₀` \| `Left.lt_mul_of_lt_of_one_le_of_nonneg` / `one_lt_mul_of_lt_of_le` (still there) \| \| `(Left.)one_lt_mul₀` \| \| \| `Right.one_le_mul₀` \| `Right.one_le_mul_of_le_of_le` \| \| `Right.one_lt_mul_of_lt_of_le₀` \| `Right.one_lt_mul_of_lt_of_le_of_pos` \| \| `Right.one_lt_mul_of_le_of_lt₀` \| `Right.one_lt_mul_of_le_of_lt_of_nonneg` / `one_lt_mul_of_le_of_lt` (still there) / `one_lt_mul` (still there) \| \| `Right.one_lt_mul₀` \| `Right.one_lt_mul_of_lt_of_lt` \| --- Split from #17593. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	merge-conflict t-algebra awaiting-zulip t-order label:t-algebra$	146/44	Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean	2	11	['YaelDillies', 'astrainfinita', 'github-actions', 'j-loreaux']	nobody	479-31318 1 year ago	486-23877 486 days ago	33-53295 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	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	323-73095 10 months ago	344-85737 344 days ago	24-46029 24 days
15654	TpmKranz author:TpmKranz	feat(Computability): language-preserving maps between NFA and RE	Map REs to NFAs via Thompson's construction and NFAs to REs using GNFAs Last chunk of #12648 --- - [ ] depends on: #15651 - [ ] depends on: #15649 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	blocked-by-other-PR new-contributor t-computability merge-conflict awaiting-zulip	985/2	Mathlib.lean,Mathlib/Computability/GNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean,Mathlib/Computability/RegularExpressions.lean,Mathlib/Data/FinEnum/Option.lean,docs/references.bib	7	3	['github-actions', 'leanprover-community-mathlib4-bot', 'meithecatte']	nobody	312-80995 10 months ago	582-17780 582 days ago	0-179 2 minutes
17458	urkud author:urkud	refactor(Algebra/Group): make `IsUnit` a typeclass	Also change some lemmas to assume `[IsUnit _]` instead of `[Invertible _]`. Motivated by potential non-defeq diamonds in #14986, see also [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Invertible.20and.20data) I no longer plan to merge this PR, but I'm going to cherry-pick some changes to a new PR before closing this one. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	merge-conflict t-algebra awaiting-zulip label:t-algebra$	82/72	Mathlib/Algebra/CharP/Invertible.lean,Mathlib/Algebra/Group/Invertible/Basic.lean,Mathlib/Algebra/Group/Units/Defs.lean,Mathlib/Algebra/GroupWithZero/Invertible.lean,Mathlib/Algebra/GroupWithZero/Units/Basic.lean,Mathlib/Algebra/Polynomial/Degree/Units.lean,Mathlib/Algebra/Polynomial/Splits.lean,Mathlib/Analysis/Convex/Segment.lean,Mathlib/Analysis/Normed/Affine/Isometry.lean,Mathlib/Analysis/Normed/Ring/Units.lean,Mathlib/CategoryTheory/Linear/Basic.lean,Mathlib/FieldTheory/Finite/Basic.lean,Mathlib/FieldTheory/Separable.lean,Mathlib/FieldTheory/SeparableDegree.lean,Mathlib/GroupTheory/Submonoid/Inverses.lean,Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean,Mathlib/LinearAlgebra/AffineSpace/Combination.lean,Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean,Mathlib/LinearAlgebra/CliffordAlgebra/Inversion.lean,Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean,Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean,Mathlib/NumberTheory/MulChar/Basic.lean,Mathlib/RingTheory/Localization/NumDen.lean,Mathlib/RingTheory/Polynomial/Content.lean,Mathlib/RingTheory/Polynomial/GaussLemma.lean,Mathlib/RingTheory/Valuation/Basic.lean	26	12	['MichaelStollBayreuth', 'acmepjz', 'eric-wieser', 'github-actions', 'leanprover-bot', 'leanprover-community-bot-assistant', 'urkud']	nobody	252-61344 8 months ago	524-8987 524 days ago	0-66650 18 hours
25218	kckennylau author:kckennylau	feat(AlgebraicGeometry): Tate normal form of elliptic curves	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	merge-conflict t-algebraic-geometry awaiting-zulip new-contributor	291/26	Mathlib.lean,Mathlib/AlgebraicGeometry/EllipticCurve/IsomOfJ.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Modular/TateNormalForm.lean,Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean,Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean	5	31	['MichaelStollBayreuth', 'Multramate', 'acmepjz', 'github-actions', 'grunweg', 'kckennylau', 'leanprover-community-bot-assistant']	nobody	252-60182 8 months ago	285-35299 285 days ago	6-44784 6 days
28803	astrainfinita author:astrainfinita	refactor: unbundle algebra from `ENormed*`	Further speed up the search in the algebraic typeclass hierarchy by avoiding searching for `TopologicalSpace`. This PR continues the work from #23961. - Change `ESeminormed(Add)Monoid` and `ENormed(Add)Monoid` so they no longer carry algebraic data. - Deprecate `ESeminormed(Add)CommMonoid` and `ENormed(Add)CommMonoid` in favor of `ESeminormed(Add)Monoid` and `ENormed(Add)Monoid` with a commutative algebraic typeclass. \|Old\|New\| \|---\|---\| \| `[ESeminormed(Add)(Comm)Monoid E]` \| `[(Add)(Comm)Monoid E] [ESeminormed(Add)Monoid E]` \| \| `[ENormed(Add)(Comm)Monoid]` \| `[(Add)(Comm)Monoid E] [ENormed(Add)Monoid]` \| See [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2328803.20refactor.3A.20unbundle.20algebra.20from.20.60ENormed*.60/with/536024350) ------------ - [x] depends on: #28813	t-algebra merge-conflict slow-typeclass-synthesis awaiting-zulip t-analysis label:t-algebra$	80/63	Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/Analysis/Normed/Group/Continuity.lean,Mathlib/Analysis/Normed/Group/InfiniteSum.lean,Mathlib/Analysis/NormedSpace/IndicatorFunction.lean,Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean,Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean,Mathlib/MeasureTheory/Function/L1Space/Integrable.lean,Mathlib/MeasureTheory/Function/LocallyIntegrable.lean,Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean,Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean,Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean,Mathlib/MeasureTheory/Integral/IntegrableOn.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean	14	28	['astrainfinita', 'bryangingechen', 'github-actions', 'grunweg', 'kbuzzard', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib-bors', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'sgouezel']	grunweg assignee:grunweg	192-75827 6 months ago	201-26981 201 days ago	0-19882 5 hours
28925	grunweg author:grunweg	chore: remove `linear_combination'` tactic	When `linear_combination` was refactored in #15899, the old code was kept as the `linear_combination'` tactic, for easier migration. The consensus of the zulip discussion ([#mathlib4 > Narrowing the scope of `linear_combination` @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Narrowing.20the.20scope.20of.20.60linear_combination.60/near/470237816)) was to wait, and "revisit this once people have experienced the various tactics in practice". One year later, the old tactic has almost no uses: it is unused in mathlib; [searching on github](https://github.com/search?q=linear_combination%27%20path%3A*.lean&type=code) yields 37 hits --- all of which are in various forks of mathlib. Thus, removing this tactic seems appropriate. --- Do not merge before the zulip discussion has concluded! [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	merge-conflict file-removed awaiting-zulip	0/564	Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/LinearCombination'.lean,Mathlib/Tactic/Linter/UnusedTactic.lean,MathlibTest/linear_combination'.lean	5	4	['euprunin', 'github-actions', 'grunweg', 'mathlib4-merge-conflict-bot']	nobody	149-53037 4 months ago	200-84834 200 days ago	0-1 1 second
30150	imbrem author:imbrem	feat(CategoryTheory/Monoidal): to_additive for MonoidalCategory	Add `AddMonoidalCategory`, the additive version of `MonoidalCategory`. To get this to work, I needed to _remove_ the `to_additive` attributes in `Discrete.lean`, since existing code relies on the `AddMonoid M → MonoidalCategory M` instance. For now, we simply implement the additive variants by hand instead. --- As discussed in #28718; I added an `AddMonoidalCategory` struct and tagged `MonoidalCategory` with `to_additive`, along with the lemmas in `Category.lean`. I think this is the right approach, since under this framework the "correct" additive version of `Discrete.lean` would be mapping an `AddMonoid` to an `AddMonoidalCategory`. Next steps would be to: - Make `monoidal_coherence` and `coherence` support `AddMonoidalCategory` - Add `CocartesianMonoidalCategory` extending `AddMonoidalCategory` [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-category-theory large-import new-contributor merge-conflict awaiting-zulip t-meta	444/125	Mathlib/CategoryTheory/Monoidal/Category.lean,Mathlib/CategoryTheory/Monoidal/Discrete.lean,Mathlib/Tactic/ToAdditive/GuessName.lean	3	22	['JovanGerb', 'YaelDillies', 'github-actions', 'imbrem', 'mathlib4-merge-conflict-bot']	nobody	121-63911 4 months ago	161-42577 161 days ago	1-160 1 day
15651	TpmKranz author:TpmKranz	feat(Computability/NFA): operations for Thompson's construction	Lays the groundwork for a proof of equivalence of RE and NFA, w.r.t. described language. Actual connection to REs comes later, after the groundwork for the opposite direction has been laid. Third chunk of #12648 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-computability merge-conflict awaiting-author awaiting-zulip	307/5	Mathlib/Computability/NFA.lean	1	27	['TpmKranz', 'YaelDillies', 'dupuisf', 'github-actions', 'leanprover-community-bot-assistant', 'meithecatte', 'rudynicolop']	nobody	116-81043 3 months ago	536-22031 536 days ago	45-84611 45 days
15649	TpmKranz author:TpmKranz	feat(Computability): introduce Generalised NFA as bridge to Regular Expression	Lays the groundwork for a proof of equivalence of NFA and RE, w.r.t. described language. Actual connection to NFA comes later, after the groundwork for the opposite direction has been laid. Second chunk of #12648 --- - [x] depends on: #15647 [Data.FinEnum.Option unchanged since then] [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-computability merge-conflict awaiting-author awaiting-zulip	298/0	Mathlib.lean,Mathlib/Computability/GNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/RegularExpressions.lean,docs/references.bib	5	7	['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'meithecatte', 'trivial1711']	nobody	116-10884 3 months ago	461-60814 461 days ago	23-54870 23 days
20648	anthonyde author:anthonyde	feat: formalize regular expression -> εNFA	The file `Computability/RegularExpressionsToEpsilonNFA.lean` contains a formal definition of Thompson's method for constructing an `εNFA` from a `RegularExpression` and a proof of its correctness. --- - [x] depends on: #20644 - [x] depends on: #20645 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	merge-conflict t-computability awaiting-zulip new-contributor	490/0	Mathlib.lean,Mathlib/Computability/RegularExpressionsToEpsilonNFA.lean,docs/references.bib	3	7	['anthonyde', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'meithecatte', 'qawbecrdtey']	nobody	115-48052 3 months ago	312-80981 312 days ago	75-77754 75 days
11800	JADekker author:JADekker	feat: KappaLindelöf spaces	Define KappaLindelöf spaces by following the first one-third of the API for Lindelöf spaces. The remainder will be added in a future PR. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	please-adopt merge-conflict t-topology awaiting-zulip	301/2	Mathlib.lean,Mathlib/Topology/Compactness/KappaLindelof.lean,Mathlib/Topology/Compactness/Lindelof.lean	3	38	['ADedecker', 'JADekker', 'PatrickMassot', 'StevenClontz', 'adomani', 'github-actions', 'grunweg', 'kim-em', 'urkud']	nobody	115-19918 3 months ago	590-40200 590 days ago	123-25636 123 days
30668	astrainfinita author:astrainfinita	feat: `QuotType`	This typeclass is primarily for use by type synonyms of `Quot` and `Quotient`. Using `QuotType` API for type synonyms of `Quot` and `Quotient` will avoid defeq abuse caused by directly using `Quot` and `Quotient` APIs. This PR also adds some typeclasses to support different ways to find the quotient map that should be used. See the documentation comments of these typeclasses for examples of usage. --- It's not a typical design to use these auxiliary typeclasses and term elaborators, but I haven't found a better way to support these notations. Some of the naming may need to be discussed. For example: - `⟦·⟧` is currently called `mkQ` in names. This distinguishes it from other `.mk`s and makes it possible to write the quotient map as `mkQ` `mkQ'` ~~`mkQ_ h`~~. But this will also require changing the old lemma names. - It would be helpful if the names of new type classes explained their functionality better. [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/migrate.20to.20.60QuotLike.60.20API) This PR continues the work from #16421. Original PR: https://github.com/leanprover-community/mathlib4/pull/16421	RFC t-data awaiting-zulip	629/0	Mathlib.lean,Mathlib/Data/QuotType.lean,MathlibTest/QuotType.lean	3	20	['YaelDillies', 'astrainfinita', 'github-actions', 'mathlib4-merge-conflict-bot', 'plp127', 'vihdzp']	nobody	94-1764 3 months ago	146-57017 146 days ago	0-81 1 minute
33368	urkud author:urkud	feat: define `Complex.UnitDisc.shift`	Also review the existing API UPD: I'm going to define a `PSL(2, Real)` action instead. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-analysis awaiting-zulip merge-conflict	273/39	Mathlib.lean,Mathlib/Analysis/Complex/UnitDisc/Basic.lean,Mathlib/Analysis/Complex/UnitDisc/Shift.lean	3	7	['github-actions', 'j-loreaux', 'mathlib4-merge-conflict-bot', 'sgouezel', 'urkud']	j-loreaux assignee:j-loreaux	66-56477 2 months ago	67-16810 67 days ago	7-33574 7 days
32828	Hagb author:Hagb	feat(Algebra/Order/Group/Defs): add `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid'`	It is similar to `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid`, while with different hypotheses. The conclusion `IsOrderedCancelMonoid α` on `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` still holds when the hypothesis `CommGroup α` is weakened to `CancelCommMonoid α` while `PartialOrder α` is strengthened to `LinearOrder α`. --- [`IsOrderedAddMonoid.toIsOrderedCancelAddMonoid`](https://leanprover-community.github.io/mathlib4_docs/find/?pattern=IsOrderedAddMonoid.toIsOrderedCancelAddMonoid#doc) and `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid'`: https://github.com/leanprover-community/mathlib4/blob/97f78b1a4311fed1844b94f1c069219a48a098e1/Mathlib/Algebra/Order/Group/Defs.lean#L52-L62 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	awaiting-zulip t-algebra label:t-algebra$	4/0	Mathlib/Algebra/Order/Group/Defs.lean	1	8	['Garmelon', 'Vierkantor', 'artie2000', 'github-actions', 'leanprover-radar']	eric-wieser assignee:eric-wieser	51-18912 1 month ago	51-18912 51 days ago	40-42357 40 days
33031	chiyunhsu author:chiyunhsu	feat(Combinatorics/Enumerative/Partition): add combinatorial proof of Euler's partition theorem	The new file EulerComb.lean contains the combinatorial proof of Euler's partition theorem. The analytic proof of the theorem and its generalization of Glaisher's Theorem has already been formalized in [Glaisher.lean](https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Combinatorics/Enumerative/Partition/Glaisher.lean). The generalization of the combinatorial proof from this file to Glaisher's Theorem is within reach. --- Zulip discussion: [#mathlib4 > Glaisher’s Bijection on integer partitions](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Glaisher.E2.80.99s.20Bijection.20on.20integer.20partitions/with/570808111) [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics new-contributor awaiting-zulip	531/0	Mathlib.lean,Mathlib/Combinatorics/Enumerative/Partition/EulerComb.lean	2	5	['chiyunhsu', 'github-actions', 'tb65536', 'vihdzp']	b-mehta assignee:b-mehta	44-23730 1 month ago	44-23730 44 days ago	42-22427 42 days
32608	PrParadoxy author:PrParadoxy	feat(LinearAlgebra/PiTensorProduct): API for PiTensorProducts indexed by sets	This PR addresses a TODO item in LinearAlgebra/PiTensorProduct.lean: * API for the various ways ι can be split into subsets; connect this with the binary tensor product -- specifically by describing tensors of type ⨂ (i : S), M i, for S : Set ι. Our primary motivation is to formalise the notion of "restricted tensor products". This will be the content of a follow-up PR. Beyond that, the Set API is natural in contexts where the index type has an independent interpretation. An example is quantum physics, where ι ranges over distinguishable degrees of freedom, and where its is common practice to annotate objects by the set of indices they are defined on. --- Stub file with preliminary definition of the restricted tensor product as a direct limit of tensors indexed by finite subsets of an index type: https://github.com/PrParadoxy/mathlib4/blob/restricted-stub/Mathlib/LinearAlgebra/PiTensorProduct/Restricted.lean --- - [x] depends on: #32598 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor awaiting-zulip t-algebra label:t-algebra$	300/2	Mathlib.lean,Mathlib/LinearAlgebra/PiTensorProduct.lean,Mathlib/LinearAlgebra/PiTensorProduct/Set.lean	3	28	['PrParadoxy', 'dagurtomas', 'eric-wieser', 'github-actions', 'goliath-klein', 'leanprover-radar', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot']	dagurtomas assignee:dagurtomas	41-36335 1 month ago	82-13237 82 days 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/)	new-contributor awaiting-zulip t-measure-probability	4/0	Mathlib/MeasureTheory/Constructions/Polish/Basic.lean	1	9	['ADedecker', 'LTolDe', 'dupuisf', 'github-actions', 'jcommelin']	PatrickMassot assignee:PatrickMassot	41-36140 1 month ago	67-20272 67 days ago	11-7507 11 days
34720	Paul-Lez author:Paul-Lez	feat(RingTheory/PowerSeries/Composition): define composition of power series	This PR defines the composition of two power series, and adds various pieces of API lemmas (this is mostly fixing up and upstreaming code from [this repo](https://github.com/rmhi/formal_deriv)). This is the first of a series of PRs upstreaming work that was done at the CFT workshop in Oxford last summer, working towards proving some results about the `exp` and `log` power series (and their composition!), and constructing the isomorphism $(\mathfrak{m}_K ^ n, +) \cong (1 + \mathfrak{m}_K ^ n, \times)$ for sufficiently large $n$, where $K$ is a characteristic zero local field. Co-authored-by: Richard Hill Co-authored-by: Calle Sönne --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-ring-theory awaiting-zulip	844/0	Mathlib.lean,Mathlib/RingTheory/PowerSeries/Composition.lean	2	3	['Paul-Lez', 'github-actions', 'vihdzp']	nobody	32-82149 1 month ago	40-34069 40 days ago	0-10 10 seconds
33441	dupuisf author:dupuisf	feat: add `LawfulInv` class for types with an inverse that behaves like `Ring.inverse`	This PR introduces a new typeclass `LawfulInv` for types which have an `Inv` instance that is equal to zero on non-invertible elements. This is meant to replace `Ring.inverse`. The current plan is to do this refactor in several steps: 1. This PR, which only introduces the class and adds instances for matrices and continuous linear maps. 2. Add instances for all C*-algebras, and make `CStarAlgebra` extend this. 3. Deprecate `Ring.inverse`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	awaiting-zulip t-algebra merge-conflict label:t-algebra$	185/27	Mathlib/Algebra/GroupWithZero/Defs.lean,Mathlib/Algebra/GroupWithZero/Invertible.lean,Mathlib/Algebra/GroupWithZero/Units/Basic.lean,Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean,Mathlib/LinearAlgebra/Matrix/PosDef.lean,Mathlib/RingTheory/DividedPowers/Padic.lean,Mathlib/Topology/Algebra/Module/Equiv.lean	7	35	['dupuisf', 'eric-wieser', 'github-actions', 'j-loreaux', 'mathlib-merge-conflicts', 'mathlib4-merge-conflict-bot', 'plp127']	nobody	24-54488 24 days ago	53-1223 53 days ago	7-54141 7 days
26299	adomani author:adomani	perf: the `whitespace` linter only acts on modified files	Introduces an `IO.Ref` to allow the `commandStart` linter to only run on files that git considers modified with respect to `master`. The linter is also active on files that have had some error, as these are likely being modified! The PR should also mitigate the speed-up that the linter introduced: [#mathlib4 > A whitespace linter @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/A.20whitespace.20linter/near/525091877) Assuming that this goes well, a similar mechanism could be applied to several linters that do not need to run on all code, just on the modified code. Implementation detail: the linter is currently either on or off in "whole" files. It may be also a future development to make this more granular and only run the linter on "modifed commands in modified files", but this is not currently the plan for this modification! --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-linter awaiting-zulip awaiting-author	55/7	Mathlib/Tactic/Linter/Whitespace.lean	1	19	['adomani', 'eric-wieser', 'github-actions', 'grunweg', 'joneugster', 'kim-em', 'leanprover-bot', 'leanprover-radar', 'mathlib-bors', 'mathlib4-merge-conflict-bot']	grunweg assignee:grunweg	24-46914 24 days ago	197-43232 197 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	22-17533 22 days ago	23-40213 23 days ago	0-187 3 minutes
35578	Shreyas4991 author:Shreyas4991	fix: writer monad should use an additive logging type	The Writer monad's w type is supposed to be additive, not multiplicative. This is how it is conceptually used in Haskell (as a logging type). Haskell uses `Monoid` because it doesn't make a distinction between `AddMonoid` and `Monoid`. [#mathlib4 > Writer should use an additive monoid @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Writer.20should.20use.20an.20additive.20monoid/near/574990415) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-data awaiting-zulip	10/10	Mathlib/Control/Monad/Cont.lean,Mathlib/Control/Monad/Writer.lean	2	4	['Shreyas4991', 'eric-wieser', 'github-actions']	nobody	21-82447 21 days ago	21-82448 21 days ago	0-18707 5 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/)	new-contributor t-computability merge-conflict awaiting-author awaiting-zulip	159/0	Mathlib/Computability/DFA.lean,Mathlib/Computability/Language.lean	2	60	['EtienneC30', 'YaelDillies', 'github-actions', 'maemre', 'mathlib4-merge-conflict-bot', 'meithecatte', 'urkud']	nobody	16-41286 16 days ago	362-19225 362 days ago	48-67492 48 days
22361	rudynicolop author:rudynicolop	feat(Computability/NFA): nfa closure properties	Add the closure properties union, intersection and reversal for NFA. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-computability merge-conflict awaiting-author awaiting-zulip	218/2	Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean	2	91	['EtienneC30', 'b-mehta', 'ctchou', 'github-actions', 'leanprover-community-bot-assistant', 'meithecatte', 'rudynicolop']	nobody	16-41270 16 days ago	313-23164 313 days ago	39-61332 39 days
23929	meithecatte author:meithecatte	feat(Computability/NFA): improve bound on pumping lemma	--- - [x] depends on: #25321 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-computability awaiting-zulip new-contributor awaiting-author	101/10	Mathlib/Computability/EpsilonNFA.lean,Mathlib/Computability/NFA.lean	2	42	['YaelDillies', 'dagurtomas', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'meithecatte']	nobody	15-61299 15 days ago	280-4198 280 days ago	34-10092 34 days
34649	peabrainiac author:peabrainiac	feat(Analysis/Calculus/ContDiff): add notation `ℕ∞ω` for `WithTop ℕ∞`	Add a `ContDiff`-scoped notation `ℕ∞ω` for `WithTop ℕ∞`, accompanying the existing notations `∞` and `ω` for `(⊤ : ℕ∞) : ℕ∞ω` and `⊤ : ℕ∞ω`. --- [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/RFC.3A.20notation.20for.20.60WithTop.20.E2.84.95.E2.88.9E.60/near/573917824) I've also replaced `WithTop ℕ∞` with this new notation already in the files that mention it the most, but not in all files yet; many mention `WithTop ℕ∞` just a couple of times but don't open the `ContDiff` namespace. I'm not sure whether that should be taken as a sign to not make the notation scoped, or whether the solution is just to `open scoped ContDiff` in these files or not use the notation there. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-differential-geometry t-analysis awaiting-author awaiting-zulip merge-conflict	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	13-6838 13 days ago	31-81479 31 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/)	t-data awaiting-author awaiting-zulip	162/0	Mathlib/Data/Quot.lean,Mathlib/Data/Set/Image.lean,Mathlib/Data/SetLike/Basic.lean,Mathlib/Data/Setoid/Basic.lean	4	5	['SnirBroshi', 'TwoFX', 'eric-wieser', 'github-actions', 'mathlib-merge-conflicts']	TwoFX assignee:TwoFX	11-43500 11 days ago	107-46840 107 days ago	35-84279 35 days
34245	staroperator author:staroperator	feat(Data/Set): add `Set.Uncountable`	There are `Set` specialized shortcuts `Set.Finite`, `Set.Infinite` and `Set.Countable`, but lacking `Set.Uncountable`. I find this useful in #34246. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-data awaiting-zulip	82/4	Mathlib/Analysis/Real/Cardinality.lean,Mathlib/Data/Set/Countable.lean,Mathlib/SetTheory/Cardinal/Basic.lean	3	17	['github-actions', 'joneugster', 'staroperator', 'vihdzp']	joneugster assignee:joneugster	8-39513 8 days ago	39-12760 39 days ago	12-21154 12 days
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	14	['YuvalFilmus', 'artie2000', 'github-actions', 'mathlib-merge-conflicts', 'urkud', 'vihdzp']	ADedecker and urkud assignee:urkud assignee:ADedecker	8-12572 8 days ago	19-16679 19 days ago	39-23486 39 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 merge-conflict label:t-algebra$	3/9	Mathlib/Algebra/Group/Action/Defs.lean,Mathlib/Algebra/Group/Action/Units.lean	2	26	['alreadydone', 'github-actions', 'kbuzzard', 'leanprover-radar', 'mathlib-merge-conflicts']	jcommelin assignee:jcommelin	4-45392 4 days ago	24-48239 24 days ago	0-56658 15 hours
36522	nielsvoss author:nielsvoss	chore(Topology): rename lim -> Filter.lim and limUnder -> Filter.limUnder, and make a lemma protected	Add the namespace `Filter` to `lim` and `limUnder`, since the docstring for `lim` suggests that they were never intended to be placed in the namespace. Also make `MeasureTheory.StronglyMeasurable.limUnder` protected, to allow its proof to refer to `Filter.limUnder` as `limUnder`. See discussion here: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Rename.20lim.20to.20Filter.2Elim.3F/with/578862980 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-topology awaiting-zulip	12/8	Mathlib/MeasureTheory/Constructions/Polish/StronglyMeasurable.lean,Mathlib/MeasureTheory/Function/FactorsThrough.lean,Mathlib/Topology/Defs/Filter.lean	3	7	['github-actions', 'grunweg', 'nielsvoss']	nobody	2-8609 2 days ago	2-41090 2 days ago	0-1564 26 minutes
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$	64/24	Mathlib/Algebra/GroupWithZero/Commute.lean,Mathlib/Algebra/GroupWithZero/Invertible.lean,Mathlib/Algebra/GroupWithZero/Units/Basic.lean	3	1	['github-actions']	nobody	0-1550 25 minutes ago	48-58418 48 days ago	0-1 1 second

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
36510	Parcly-Taxel author:Parcly-Taxel	chore: delete >6 month old deprecated modules	* Every `deprecated_module` up to and including `2025-09-12`. * `Mathlib.Deprecated.Estimator` and `Mathlib.Deprecated.MLList.BestFirst` from #29549. * `Mathlib.Data.Nat.PartENat` from #29231. * `Mathlib.Deprecated.RingHom` from #33429 – at the time it was removed (see https://github.com/leanprover-community/mathlib4/blob/561ba4ae9408025b2d4c9403116b575b7d2a0205/Mathlib/Deprecated/RingHom.lean) there were only two declarations inside and they both had `@[deprecated (since := "2025-06-09")]`, so there was effectively a `deprecated_module (since := "2025-06-09")` on top.	file-removed tech debt	0/1606	Mathlib.lean,Mathlib/Analysis/NormedSpace/BallAction.lean,Mathlib/Analysis/NormedSpace/DualNumber.lean,Mathlib/Analysis/NormedSpace/FunctionSeries.lean,Mathlib/Analysis/NormedSpace/HomeomorphBall.lean,Mathlib/Analysis/NormedSpace/IndicatorFunction.lean,Mathlib/Analysis/NormedSpace/Int.lean,Mathlib/Analysis/NormedSpace/OperatorNorm/Asymptotics.lean,Mathlib/Analysis/NormedSpace/OperatorNorm/Basic.lean,Mathlib/Analysis/NormedSpace/OperatorNorm/Bilinear.lean,Mathlib/Analysis/NormedSpace/OperatorNorm/Completeness.lean,Mathlib/Analysis/NormedSpace/OperatorNorm/Mul.lean,Mathlib/Analysis/NormedSpace/OperatorNorm/NNNorm.lean,Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean,Mathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean,Mathlib/Analysis/NormedSpace/Pointwise.lean,Mathlib/Analysis/NormedSpace/RCLike.lean,Mathlib/Analysis/NormedSpace/Real.lean,Mathlib/Analysis/NormedSpace/SphereNormEquiv.lean,Mathlib/Data/Nat/PartENat.lean,Mathlib/Deprecated/Estimator.lean,Mathlib/Deprecated/MLList/BestFirst.lean,Mathlib/Deprecated/Order.lean,Mathlib/Deprecated/RingHom.lean,Mathlib/RingTheory/Valuation/IntegrallyClosed.lean,Mathlib/Topology/Algebra/Module/StrongDual.lean,MathlibTest/search/BestFirst.lean	27	1	['github-actions']	nobody	2-68610 2 days ago	2-69213 2 days ago	2-68866 2 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	92/101	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/TuringMachine/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	2	['github-actions', 'mathlib-merge-conflicts']	joneugster assignee:joneugster	2-62291 2 days ago	2-63019 2 days ago	12-76708 12 days