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 17, 2026 at 04:03 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	4-33596 4 days ago	4-82267 4 days ago	2-15970 2 days
36290	euprunin author:euprunin	chore(AlgebraicGeometry): unsqueeze terminal `simp`:s (`simp only […]` to `simp`)	The goal of this PR is to decrease the number of times lemmas are called explicitly. 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): * `AlgebraicGeometry.IsClosedImmersion.Spec_iff`: 141 ms before, 108 ms after 🎉 * `AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.denom_notMem`: unchanged 🎉 Profiled using `set_option trace.profiler true in`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebraic-geometry ready-to-merge	2/2	Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean,Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean	2	4	['github-actions', 'joelriou', 'mathlib-bors']	alexjbest assignee:alexjbest	1-51993 1 day ago	1-68469 1 day ago	8-50409 8 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	39-38128 1 month ago	39-38132 39 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	33-59956 1 month ago	33-59956 33 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	25-72822 25 days ago	54-67721 54 days ago	54-74879 54 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	9-69330 9 days ago	11-49051 11 days ago	19-42058 19 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	4-59397 4 days ago	5-18113 5 days ago	10-81047 10 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	4-39666 4 days ago	10-38876 10 days ago	169-416 169 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	4-20606 4 days ago	4-33854 4 days ago	14-47661 14 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	3-48316 3 days ago	3-53350 3 days ago	19-3423 19 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	3-47573 3 days ago	3-47613 3 days ago	10-49883 10 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	3-41805 3 days ago	3-41905 3 days ago	4-23412 4 days
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	3-41420 3 days ago	3-65787 3 days ago	8-74841 8 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	2-73172 2 days ago	23-14694 23 days ago	23-14585 23 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	2-65729 2 days ago	4-10929 4 days ago	5-15190 5 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	2-53492 2 days ago	2-73134 2 days ago	28-85800 28 days
34622	vihdzp author:vihdzp	feat: Nat/Int casts on char two rings	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra maintainer-merge label:t-algebra$	50/8	Mathlib/Algebra/CharP/Two.lean,Mathlib/Data/Set/Insert.lean	2	11	['erdOne', 'eric-wieser', 'github-actions', 'vihdzp']	erdOne assignee:erdOne	2-24528 2 days ago	13-64865 13 days ago	45-694 45 days
36473	AlexeyMilovanov author:AlexeyMilovanov	feat(Computability.Primrec.List): add primrec proofs for drop, takeWhile, and dropWhile	This PR adds missing proofs that several standard `List` operations are primitive recursive (Primrec), as well as a basic property of `tail` and `drop`. Specifically, it introduces: * `List.tail_iterate`: Applying `tail` to a list `n` times is equivalent to dropping `n` elements. * `Primrec.list_drop`: `List.drop` is primitive recursive. * `Primrec.list_take`: `List.take` is primitive recursive. * `Primrec.list_takeWhile`: `List.takeWhile` is primitive recursive. * `Primrec.list_dropWhile`: `List.dropWhile` is primitive recursive. These are basic computability properties for lists that were currently missing from `Mathlib.Computability.Primrec.List`. All proofs use standard combinators and `of_eq`.	t-computability new-contributor maintainer-merge	27/0	Mathlib/Computability/Primrec/List.lean,Mathlib/Data/List/TakeDrop.lean	2	23	['AlexeyMilovanov', 'Komyyy', 'github-actions']	nobody	1-66099 1 day ago	1-69393 1 day ago	5-3056 5 days
36137	smmercuri author:smmercuri	feat: define pullbacks of `HeightOneSpectrum`	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-ring-theory maintainer-merge	8/0	Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean	1	3	['erdOne', 'github-actions']	erdOne assignee:erdOne	1-52905 1 day ago	12-51130 12 days ago	12-51021 12 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`. --- [![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	1-52322 1 day ago	8-26062 8 days ago	12-15980 12 days
36640	euprunin author:euprunin	chore: replace long terminal `rw […]`:s (≥5 lemmas) with bare `simp`:s	The goal of this PR is to decrease the number of times lemmas are called explicitly. 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): * `CategoryTheory.Functor.reflectsMonomorphisms.of_iso`: unchanged 🎉 * `CategoryTheory.Functor.reflectsEpimorphisms.of_iso`: unchanged 🎉 * `Orientation.oangle_add_right_smul_rotation_pi_div_two`: unchanged 🎉 * `Equiv.Perm.IsCycle.sign`: unchanged 🎉 * `sdiff_sdiff_right`: unchanged 🎉 * `dvd_coeff_zero_of_aeval_eq_prime_smul_of_minpoly_isEisensteinAt`: unchanged 🎉 Profiled using `set_option trace.profiler true in`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge	6/7	Mathlib/CategoryTheory/Functor/EpiMono.lean,Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean,Mathlib/GroupTheory/Perm/Cycle/Basic.lean,Mathlib/Order/BooleanAlgebra/Basic.lean,Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean	5	4	['erdOne', 'euprunin', 'github-actions']	nobody	1-45992 1 day ago	2-55144 2 days ago	2-55035 2 days
35323	martinwintermath author:martinwintermath	feat(Geometry/Convex/Cone): Add lemmas for PointedCone.dual	Add several useful lemmas for `PointedCone.dual` in preparation for duality theory for FG cones. Some other changes are: * renamed `dual_le_dual` to `dual_anti` and added partner lemma `dual_antitone` * removed TODO comment since the stated lemma is not sufficient to prove the claim, an also this has now been proven and will become a PR in the near future. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-convex-geometry maintainer-merge	37/6	Mathlib/Geometry/Convex/Cone/Dual.lean	1	23	['YaelDillies', 'github-actions', 'martinwintermath']	YaelDillies assignee:YaelDillies	1-39478 1 day ago	11-73012 11 days ago	17-60628 17 days
34554	SnirBroshi author:SnirBroshi	feat(Data/Nat/Factorization/Divisors): calculate divisors using prime factorization	--- There are over 200 files that import both `divisors` and `factorization`, but none of them seemed to fit, so I created a new file for this. (`Data.Nat.Factorization.PrimePow` and `NumberTheory.ArithmeticFunction.Misc` are the best I found) [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-data maintainer-merge	91/0	Mathlib.lean,Mathlib/Data/Nat/Factorization/Divisors.lean	2	24	['SnirBroshi', 'YaelDillies', 'b-mehta', 'eric-wieser', 'github-actions', 'jcommelin', 'joneugster', 'mathlib-bors', 'plp127']	joneugster assignee:joneugster	1-19917 1 day ago	19-67560 19 days ago	20-28562 20 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']	dagurtomas assignee:dagurtomas	1-10817 1 day ago	4-71891 4 days ago	5-70146 5 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	39-38128 1 month ago	39-38132 39 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	33-59956 1 month ago	33-59956 33 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	25-72822 25 days ago	54-67721 54 days ago	54-74879 54 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	9-69330 9 days ago	11-49051 11 days ago	19-42058 19 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	4-59397 4 days ago	5-18113 5 days ago	10-81047 10 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	4-39666 4 days ago	10-38876 10 days ago	169-416 169 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	4-20606 4 days ago	4-33854 4 days ago	14-47661 14 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	3-48316 3 days ago	3-53350 3 days ago	19-3423 19 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	3-47573 3 days ago	3-47613 3 days ago	10-49883 10 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	3-41805 3 days ago	3-41905 3 days ago	4-23412 4 days
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	3-41420 3 days ago	3-65787 3 days ago	8-74841 8 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	2-73172 2 days ago	23-14694 23 days ago	23-14585 23 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	2-65729 2 days ago	4-10929 4 days ago	5-15190 5 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	2-53492 2 days ago	2-73134 2 days ago	28-85800 28 days
34622	vihdzp author:vihdzp	feat: Nat/Int casts on char two rings	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra maintainer-merge label:t-algebra$	50/8	Mathlib/Algebra/CharP/Two.lean,Mathlib/Data/Set/Insert.lean	2	11	['erdOne', 'eric-wieser', 'github-actions', 'vihdzp']	erdOne assignee:erdOne	2-24528 2 days ago	13-64865 13 days ago	45-694 45 days
36473	AlexeyMilovanov author:AlexeyMilovanov	feat(Computability.Primrec.List): add primrec proofs for drop, takeWhile, and dropWhile	This PR adds missing proofs that several standard `List` operations are primitive recursive (Primrec), as well as a basic property of `tail` and `drop`. Specifically, it introduces: * `List.tail_iterate`: Applying `tail` to a list `n` times is equivalent to dropping `n` elements. * `Primrec.list_drop`: `List.drop` is primitive recursive. * `Primrec.list_take`: `List.take` is primitive recursive. * `Primrec.list_takeWhile`: `List.takeWhile` is primitive recursive. * `Primrec.list_dropWhile`: `List.dropWhile` is primitive recursive. These are basic computability properties for lists that were currently missing from `Mathlib.Computability.Primrec.List`. All proofs use standard combinators and `of_eq`.	t-computability new-contributor maintainer-merge	27/0	Mathlib/Computability/Primrec/List.lean,Mathlib/Data/List/TakeDrop.lean	2	23	['AlexeyMilovanov', 'Komyyy', 'github-actions']	nobody	1-66099 1 day ago	1-69393 1 day ago	5-3056 5 days
36137	smmercuri author:smmercuri	feat: define pullbacks of `HeightOneSpectrum`	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-ring-theory maintainer-merge	8/0	Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean	1	3	['erdOne', 'github-actions']	erdOne assignee:erdOne	1-52905 1 day ago	12-51130 12 days ago	12-51021 12 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`. --- [![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	1-52322 1 day ago	8-26062 8 days ago	12-15980 12 days
36640	euprunin author:euprunin	chore: replace long terminal `rw […]`:s (≥5 lemmas) with bare `simp`:s	The goal of this PR is to decrease the number of times lemmas are called explicitly. 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): * `CategoryTheory.Functor.reflectsMonomorphisms.of_iso`: unchanged 🎉 * `CategoryTheory.Functor.reflectsEpimorphisms.of_iso`: unchanged 🎉 * `Orientation.oangle_add_right_smul_rotation_pi_div_two`: unchanged 🎉 * `Equiv.Perm.IsCycle.sign`: unchanged 🎉 * `sdiff_sdiff_right`: unchanged 🎉 * `dvd_coeff_zero_of_aeval_eq_prime_smul_of_minpoly_isEisensteinAt`: unchanged 🎉 Profiled using `set_option trace.profiler true in`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge	6/7	Mathlib/CategoryTheory/Functor/EpiMono.lean,Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean,Mathlib/GroupTheory/Perm/Cycle/Basic.lean,Mathlib/Order/BooleanAlgebra/Basic.lean,Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean	5	4	['erdOne', 'euprunin', 'github-actions']	nobody	1-45992 1 day ago	2-55144 2 days ago	2-55035 2 days
35323	martinwintermath author:martinwintermath	feat(Geometry/Convex/Cone): Add lemmas for PointedCone.dual	Add several useful lemmas for `PointedCone.dual` in preparation for duality theory for FG cones. Some other changes are: * renamed `dual_le_dual` to `dual_anti` and added partner lemma `dual_antitone` * removed TODO comment since the stated lemma is not sufficient to prove the claim, an also this has now been proven and will become a PR in the near future. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-convex-geometry maintainer-merge	37/6	Mathlib/Geometry/Convex/Cone/Dual.lean	1	23	['YaelDillies', 'github-actions', 'martinwintermath']	YaelDillies assignee:YaelDillies	1-39478 1 day ago	11-73012 11 days ago	17-60628 17 days
34554	SnirBroshi author:SnirBroshi	feat(Data/Nat/Factorization/Divisors): calculate divisors using prime factorization	--- There are over 200 files that import both `divisors` and `factorization`, but none of them seemed to fit, so I created a new file for this. (`Data.Nat.Factorization.PrimePow` and `NumberTheory.ArithmeticFunction.Misc` are the best I found) [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-data maintainer-merge	91/0	Mathlib.lean,Mathlib/Data/Nat/Factorization/Divisors.lean	2	24	['SnirBroshi', 'YaelDillies', 'b-mehta', 'eric-wieser', 'github-actions', 'jcommelin', 'joneugster', 'mathlib-bors', 'plp127']	joneugster assignee:joneugster	1-19917 1 day ago	19-67560 19 days ago	20-28562 20 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']	dagurtomas assignee:dagurtomas	1-10817 1 day ago	4-71891 4 days ago	5-70146 5 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 merge-conflict	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	5	['SnirBroshi', 'github-actions', 'j-loreaux', 'mathlib-merge-conflicts']	j-loreaux assignee:j-loreaux	0-69958 19 hours ago	9-47064 9 days ago	9-50323 9 days
36353	smmercuri author:smmercuri	feat(NumberField/InfinitePlace/Ramification): add cardinality results for (un)ramified places over	The number of unramified/ramified places over a fixed infinite place `v` is equal/twice the number of unmixed/mixed complex embeddings over `v.embedding` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-number-theory maintainer-merge	137/34	Mathlib/Data/Set/Card.lean,Mathlib/Logic/Basic.lean,Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean,Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean	4	14	['MichaelStollBayreuth', 'github-actions', 'smmercuri', 'tb65536']	MichaelStollBayreuth assignee:MichaelStollBayreuth	0-68550 19 hours ago	1-53966 1 day ago	6-64953 6 days
36720	YanYablonovskiy author:YanYablonovskiy	feat(Order): `OrderType.lift` and more order type API	Adding the universe lifting operation to `OrderType` , addresses a 'TODO' . --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-order new-contributor maintainer-merge	36/2	Mathlib/Order/Types/Defs.lean	1	17	['YaelDillies', 'YanYablonovskiy', 'github-actions']	nobody	0-61166 16 hours ago	0-61230 16 hours ago	0-62295 17 hours
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`. --- - [x] depends on: #36365 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra maintainer-merge label:t-algebra$	83/1	Mathlib/FieldTheory/Galois/IsGaloisGroup.lean	1	19	['github-actions', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'robin-carlier', 'xroblot']	nobody	0-50434 14 hours ago	1-64616 1 day ago	1-77157 1 day
35233	kim-em author:kim-em	chore: lake shake --add-public --keep-implied --keep-prefix --fix	This PR runs `lake shake --add-public --keep-implied --keep-prefix --fix` again after https://github.com/leanprover-community/mathlib4/pull/34511, picking up the remaining 28 files that now have suggestions. 🤖 Prepared with Claude Code	large-import maintainer-merge awaiting-author LLM-generated	13/12	Mathlib/Algebra/Category/ModuleCat/Sheaf/Quasicoherent.lean,Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean,Mathlib/Data/Nat/Init.lean,Mathlib/LinearAlgebra/Matrix/Kronecker.lean,Mathlib/LinearAlgebra/TensorProduct/Basic.lean,Mathlib/LinearAlgebra/TensorProduct/Defs.lean,Mathlib/LinearAlgebra/TensorProduct/Map.lean,Mathlib/Logic/Basic.lean,Mathlib/Logic/Relation.lean,Mathlib/RingTheory/MatrixAlgebra.lean,Mathlib/Tactic/Hint.lean,Mathlib/Tactic/Linter/FindDeprecations.lean,Mathlib/Tactic/Nontriviality/Core.lean,Mathlib/Tactic/NormNum/Result.lean,Mathlib/Tactic/Order/CollectFacts.lean,Mathlib/Tactic/Tauto.lean	16	16	['TwoFX', 'Vierkantor', 'adomani', 'bryangingechen', 'github-actions', 'joneugster', 'kim-em', 'mathlib-merge-conflicts', 'mathlib-splicebot']	nobody	0-46305 12 hours ago	12-77064 12 days ago	24-55404 24 days
36317	tb65536 author:tb65536	feat(NumberTheory/NumberField/Discriminant/Basic): define the root discriminant	This PR adds the definition of the root discriminant of a number field. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-number-theory t-algebra maintainer-merge label:t-algebra$	14/0	Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean	1	4	['github-actions', 'mariainesdff', 'mathlib-merge-conflicts']	mariainesdff assignee:mariainesdff	0-45208 12 hours ago	3-67361 3 days ago	9-47742 9 days
36101	wwylele author:wwylele	feat(RingTheory): lemmas about power of maximal ideal	This adds `IsMaximal.mul_mem_pow` that generalizes `Ideal.IsPrime.mul_mem_pow ` from (IsPrime + IsDedekindDomain) to IsMaximal (Except for the trivial bot case, which is why the prime version is kept) Also added a related `Quotient.isUnit_mk_pow_iff_notMem` for determining units in a quotient by power Disclosure of AI usage: this was produced when I chat with LLM for certain exercise problems, and I identified these small lemmas that can be implemented. Also asked LLM for some hints for idea. Code entirely written by me --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-ring-theory maintainer-merge	52/6	Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean,Mathlib/RingTheory/Ideal/Operations.lean,Mathlib/RingTheory/Ideal/Quotient/Nilpotent.lean	3	9	['chrisflav', 'copilot-pull-request-reviewer', 'github-actions', 'wwylele']	chrisflav assignee:chrisflav	0-33381 9 hours ago	2-26098 2 days ago	12-69185 12 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$	21/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-23845 6 hours ago	0-21770 6 hours ago	0-5503 1 hour
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	522/0	Mathlib.lean,Mathlib/CategoryTheory/Monoidal/Arrow.lean,Mathlib/CategoryTheory/Monoidal/Limits/Shapes/Pullback.lean	3	24	['dagurtomas', 'github-actions', 'joelriou', 'mathlib-dependent-issues', 'mckoen']	joelriou assignee:joelriou	0-18570 5 hours ago	3-59001 3 days ago	12-38890 12 days
35756	mariainesdff author:mariainesdff	feat(Data/Nat/Choose/Multinomial): add lemmas	Co-authored-by: @AntoineChambert-Loir. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics t-data maintainer-merge	25/0	Mathlib/Data/Nat/Choose/Multinomial.lean	1	5	['github-actions', 'joneugster']	joneugster assignee:joneugster	0-15784 4 hours ago	0-45712 12 hours ago	18-61782 18 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 maintainer-merge	100/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	11	['github-actions', 'joneugster', 'mathlib-merge-conflicts']	joneugster assignee:joneugster	0-15650 4 hours ago	1-4928 1 day ago	14-56994 14 days
36466	wwylele author:wwylele	feat(Geometry/Euclidean): misc lemma about μHE	Some building blocks for #34826 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-euclidean-geometry t-measure-probability maintainer-merge	61/0	Mathlib/Geometry/Euclidean/Volume/Measure.lean	1	4	['copilot-pull-request-reviewer', 'github-actions', 'jsm28']	jsm28 assignee:jsm28	0-14719 4 hours ago	6-2601 6 days ago	6-2492 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	24	['YaelDillies', 'artie2000', 'eric-wieser', 'github-actions', 'martinwintermath', 'mathlib4-merge-conflict-bot', 'ooovi', 'vihdzp']	YaelDillies assignee:YaelDillies	0-10962 3 hours ago	3-29859 3 days ago	30-28465 30 days
36064	marcelolynch author:marcelolynch	ci: Push to the cache using OIDC and federated credentials	This migration replaces static SAS-based cache upload auth with GitHub OIDC + Entra app registrations in Azure. Concretely, each workflow run gets a GitHub-issued OIDC token, and Azure AD (Entra) exchanges that token for a short-lived access token for Storage. We do this through app registrations configured with federated credentials, so no client secret or SAS needs to be stored for normal operation. A key design point is identity separation. We use two different app registrations (two app IDs): one for `master` workflows and one for non-master workflows. That lets us enforce different trust and permission boundaries in Azure RBAC, instead of giving one shared credential broad write access to every workflow type. Note that this separation is not implemented by this change: for now, both identities are still contributing to the same cache. On the cache client side (Cache/Requests.lean / Cache/Main.lean), auth selection is robust to empty bearer values, and there is migration-safe fallback behavior: if bearer upload fails with auth errors and SAS is available, it retries with SAS. The workflow also supports fallback to MATHLIB_CACHE_SAS when minting fails. Benefits: - OIDC/federated credentials remove dependency on a static shared upload secret. - Tokens are minted just-in-time and short-lived. - We can enforce least privilege cleanly by using separate app identities for different workflow classes. - Blast radius is reduced: master and non-master workflows can have different RBAC scopes. - We keep operational safety during migration by retaining controlled SAS fallback, but SAS is no longer the primary auth path.	CI maintainer-merge	124/34	.github/workflows/bors.yml,.github/workflows/build.yml,.github/workflows/build_fork.yml,.github/workflows/build_template.yml,.github/workflows/ci_dev.yml,Cache/Main.lean,Cache/README.md,Cache/Requests.lean	8	9	['bryangingechen', 'github-actions', 'joneugster', 'marcelolynch', 'mathlib-merge-conflicts']	jcommelin assignee:jcommelin	0-10950 3 hours ago	7-22856 7 days ago	8-60546 8 days
36429	yuma-mizuno author:yuma-mizuno	feat(CategoryTheory/Bicategory): functor bicategories for lax functors	This code is largely adapted from the existing implementation of the functor bicategory of oplax functors. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-category-theory maintainer-merge	614/25	Mathlib.lean,Mathlib/CategoryTheory/Bicategory/FunctorBicategory/Lax.lean,Mathlib/CategoryTheory/Bicategory/FunctorBicategory/Oplax.lean,Mathlib/CategoryTheory/Bicategory/Modification/Lax.lean,Mathlib/CategoryTheory/Bicategory/Modification/Oplax.lean,Mathlib/CategoryTheory/Bicategory/Modification/Pseudo.lean,Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Lax.lean,Mathlib/CategoryTheory/Bicategory/NaturalTransformation/Oplax.lean	8	20	['github-actions', 'robin-carlier', 'yuma-mizuno']	adamtopaz assignee:adamtopaz	0-10943 3 hours ago	1-69151 1 day ago	4-51841 4 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']	robin-carlier assignee:robin-carlier	0-10942 3 hours ago	3-64468 3 days ago	5-55334 5 days

PRs blocked on a zulip discussion

Number	Author	Title	Description	Labels	+/-	Modified files (first 100)	📝	💬	All users who commented or reviewed	Assignee(s)	Updated	Last status change	total time in review
17623	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	481-56778 1 year ago	488-49337 488 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	326-12155 10 months ago	347-24797 347 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	315-20055 10 months ago	584-43240 584 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	255-404 8 months ago	526-34447 526 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	254-85642 8 months ago	287-60759 287 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	195-14887 6 months ago	203-52441 203 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	151-78497 5 months ago	203-23894 203 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	124-2971 4 months ago	163-68037 163 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	119-20103 3 months ago	538-47491 538 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	118-36344 3 months ago	463-86274 463 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	117-73512 3 months ago	315-20041 315 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	117-45378 3 months ago	592-65660 592 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	96-27224 3 months ago	148-82477 148 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	68-81937 2 months ago	69-42270 69 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	53-44372 1 month ago	53-44372 53 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	46-49190 1 month ago	46-49190 46 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	43-61795 1 month ago	84-38697 84 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	43-61600 1 month ago	69-45732 69 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	35-21209 1 month ago	42-59529 42 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	26-79948 26 days ago	55-26683 55 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	26-72374 26 days ago	199-68692 199 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	24-42993 24 days ago	25-65673 25 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	24-21507 24 days ago	24-21508 24 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	18-66746 18 days ago	364-44685 364 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	18-66730 18 days ago	315-48624 315 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	18-359 18 days ago	282-29658 282 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	15-32298 15 days ago	34-20539 34 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	13-68960 13 days ago	109-72300 109 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	10-64973 10 days ago	41-38220 41 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	10-38032 10 days ago	21-42139 21 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	6-70852 6 days ago	26-73699 26 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	4-34069 4 days ago	4-66550 4 days ago	0-1564 26 minutes

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
36663	plp127 author:plp127	fix(Computability/Halting): remove `set_option linter.flexible false`	Also unsqueeze some terminal `simp`s. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	tech debt t-computability	12/17	Mathlib/Computability/Halting.lean	1	1	['github-actions']	nobody	2-1334 2 days ago	2-1412 2 days ago	2-1303 2 days
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	1-79762 1 day ago	5-8273 5 days ago	5-8164 5 days
36195	Vierkantor author:Vierkantor	chore(*): add backticks around identifiers in docstrings	This PR fixes docstrings that refer to identifiers (like add_comm) with underscores or non-balanced [square brackets], by putting `backticks` around those identifiers (or $\LaTeX$ dollar signs, as appropriate). These were spotted by a WIP linter, and are intended to ease the transition to Verso docstrings (where these issues will become errors). Another PR will fix references to identifiers that have been renamed (those that had underscores in Lean 3). --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	documentation tech debt	159/132	Mathlib/Algebra/Group/NatPowAssoc.lean,Mathlib/Algebra/Lie/UniversalEnveloping.lean,Mathlib/Algebra/MvPolynomial/Degrees.lean,Mathlib/Algebra/Polynomial/RuleOfSigns.lean,Mathlib/AlgebraicGeometry/Geometrically/Integral.lean,Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean,Mathlib/Analysis/CStarAlgebra/Spectrum.lean,Mathlib/Analysis/Fourier/AddCircle.lean,Mathlib/Analysis/Real/Cardinality.lean,Mathlib/Analysis/Real/OfDigits.lean,Mathlib/Analysis/SpecialFunctions/Arcosh.lean,Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/RootsExtrema.lean,Mathlib/CategoryTheory/EqToHom.lean,Mathlib/CategoryTheory/Functor/Flat.lean,Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean,Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean,Mathlib/Computability/TuringMachine/ToPartrec.lean,Mathlib/Data/Int/Cast/Field.lean,Mathlib/Data/List/Defs.lean,Mathlib/Data/List/Rotate.lean,Mathlib/Data/PNat/Xgcd.lean,Mathlib/Data/ZMod/Factorial.lean,Mathlib/FieldTheory/Minpoly/Field.lean,Mathlib/GroupTheory/Schreier.lean,Mathlib/InformationTheory/KullbackLeibler/KLFun.lean,Mathlib/LinearAlgebra/Alternating/Uncurry/Fin.lean,Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean,Mathlib/LinearAlgebra/Dual/Basis.lean,Mathlib/LinearAlgebra/ExteriorPower/Basis.lean,Mathlib/LinearAlgebra/LinearDisjoint.lean,Mathlib/MeasureTheory/Group/Measure.lean,Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/Periodic.lean,Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean,Mathlib/MeasureTheory/Measure/Restrict.lean,Mathlib/MeasureTheory/VectorMeasure/Decomposition/Hahn.lean,Mathlib/ModelTheory/Basic.lean,Mathlib/NumberTheory/LucasPrimality.lean,Mathlib/NumberTheory/Modular.lean,Mathlib/NumberTheory/Padics/Hensel.lean,Mathlib/NumberTheory/Padics/PadicVal/Basic.lean,Mathlib/Order/LiminfLimsup.lean,Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Independence.lean,Mathlib/Probability/Independence/Basic.lean,Mathlib/Probability/Independence/Conditional.lean,Mathlib/Probability/Independence/Kernel/Indep.lean,Mathlib/Probability/Martingale/Upcrossing.lean,Mathlib/RingTheory/DedekindDomain/Factorization.lean,Mathlib/RingTheory/DividedPowers/Padic.lean,Mathlib/RingTheory/Ideal/Maps.lean,Mathlib/RingTheory/IntegralDomain.lean,Mathlib/RingTheory/LinearDisjoint.lean,Mathlib/RingTheory/Localization/AtPrime/Basic.lean,Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean,Mathlib/RingTheory/Regular/RegularSequence.lean,Mathlib/Tactic/Algebraize.lean,Mathlib/Tactic/ArithMult.lean,Mathlib/Tactic/ArithMult/Init.lean,Mathlib/Tactic/FieldSimp/Attr.lean,Mathlib/Tactic/FieldSimp/Lemmas.lean,Mathlib/Tactic/FunProp/Types.lean,Mathlib/Tactic/LinearCombination'.lean,Mathlib/Tactic/LinearCombination.lean,Mathlib/Tactic/LinearCombination/Lemmas.lean,Mathlib/Tactic/Linter/TextBased.lean,Mathlib/Tactic/NormNum/Basic.lean,Mathlib/Tactic/NormNum/Inv.lean,Mathlib/Tactic/SetLike.lean,Mathlib/Tactic/SplitIfs.lean,Mathlib/Tactic/SwapVar.lean,Mathlib/Tactic/Translate/Core.lean,Mathlib/Tactic/Widget/SelectPanelUtils.lean,Mathlib/Topology/Order/LowerUpperTopology.lean,Mathlib/Topology/Order/UpperLowerSetTopology.lean,Mathlib/Util/AtomM.lean	76	14	['Vierkantor', 'github-actions', 'grunweg', 'mathlib-merge-conflicts']	nobody	0-47595 13 hours ago	0-47628 13 hours ago	4-10667 4 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 maintainer-merge	100/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	11	['github-actions', 'joneugster', 'mathlib-merge-conflicts']	joneugster assignee:joneugster	0-15650 4 hours ago	1-4928 1 day ago	14-56994 14 days
36751	vlad902 author:vlad902	chore(Data): remove some `set_option linter.flexible false`	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	tech debt t-data	28/56	Mathlib/Data/EReal/Operations.lean,Mathlib/Data/Nat/Digits/Defs.lean,Mathlib/Data/Nat/Digits/Lemmas.lean,Mathlib/Data/Num/Lemmas.lean,Mathlib/Data/Rat/Cast/CharZero.lean,Mathlib/Data/Set/Prod.lean,Mathlib/Data/WSeq/Basic.lean	7	3	['github-actions', 'grunweg', 'plp127']	nobody	0-15147 4 hours ago	0-20200 5 hours ago	0-20926 5 hours