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 16, 2026 at 18:32 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	3-85775 3 days ago	4-48046 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-17772 1 day ago	1-34248 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-3907 1 month ago	39-3911 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-25735 1 month ago	33-25735 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-38601 25 days ago	54-33500 54 days ago	54-40680 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-35109 9 days ago	11-14830 11 days ago	19-7859 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-25176 4 days ago	4-70292 4 days ago	10-46848 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-5445 4 days ago	10-4655 10 days ago	168-52617 168 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	3-72785 3 days ago	3-86033 3 days ago	14-13462 14 days
36470	joelriou author:joelriou	feat(CategoryTheory/Monoidal): the left adjoint of a lax monoidal functor is oplax monoidal	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-category-theory maintainer-merge	79/0	Mathlib/CategoryTheory/Monoidal/Functor.lean	1	4	['dagurtomas', 'github-actions']	nobody	3-30181 3 days ago	3-30247 3 days ago	5-21135 5 days
33935	mckoen author:mckoen	feat(CategoryTheory/Monoidal/Arrow): define monoidal structure on arrow category	defines a monoidal category structure on the arrow category of a cartesian closed category. --- - [x] depends on: #33974 - [x] depends on: #34887 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-category-theory maintainer-merge awaiting-author	511/0	Mathlib.lean,Mathlib/CategoryTheory/Monoidal/Arrow.lean,Mathlib/CategoryTheory/Monoidal/Limits/Shapes/Pullback.lean	3	23	['dagurtomas', 'github-actions', 'joelriou', 'mathlib-dependent-issues', 'mckoen']	joelriou assignee:joelriou	3-24622 3 days ago	3-79800 3 days ago	11-73773 11 days
35643	chrisflav author:chrisflav	chore(Algebra): make `TensorProduct.equivOfCompatibleSMul` more linear	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra maintainer-merge label:t-algebra$	64/47	Mathlib/LinearAlgebra/TensorProduct/Associator.lean,Mathlib/LinearAlgebra/TensorProduct/Basic.lean,Mathlib/RingTheory/Coalgebra/TensorProduct.lean,Mathlib/RingTheory/LinearDisjoint.lean,Mathlib/RingTheory/Localization/BaseChange.lean,Mathlib/RingTheory/Smooth/Fiber.lean,Mathlib/RingTheory/TensorProduct/Maps.lean,Mathlib/RingTheory/TensorProduct/Nontrivial.lean	8	17	['chrisflav', 'github-actions', 'kckennylau', 'robin-carlier']	kim-em assignee:kim-em	3-14095 3 days ago	3-19129 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-13352 3 days ago	3-13392 3 days ago	10-15684 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-7584 3 days ago	3-7684 3 days ago	3-75613 3 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-7199 3 days ago	3-31566 3 days ago	8-40642 8 days
33780	ooovi author:ooovi	feat(Geometry/Convex/Cone): lineality space of pointed cones	Define the lineality space `PointedCone.lineal` as the submodule `C ⊓ -C`. Prove that it is the largest submodule of the cone, which is sometimes used as an alternative definition. Co-authored-by: Martin Winter --- dependency of #33664 - [x] depends on #33761 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-convex-geometry maintainer-merge	36/1	Mathlib/Geometry/Convex/Cone/Pointed.lean	1	23	['YaelDillies', 'artie2000', 'eric-wieser', 'github-actions', 'martinwintermath', 'mathlib4-merge-conflict-bot', 'ooovi', 'vihdzp']	nobody	2-81356 2 days ago	2-82038 2 days ago	29-80666 29 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-38951 2 days ago	22-66873 22 days ago	22-66786 22 days
36097	matthewjasper author:matthewjasper	chore: make pseudoparents of algebraic substructures reducible	Make functions that take an algebraic substructure and return a sibling class reducible, this matches actual parents and resolves some usage of `set_option backward.isDefEq.respectTransparency false`. For example it ensures that the field instance on `IntermediateField` has a compatible `Semiring` instance to the one from it extending a `Subalgebra`. Also remove @[simp] from `adjoin_toSubsemiring`, since it prevents other simp lemmas on `adjoin` from applying. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra maintainer-merge label:t-algebra$	23/16	Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean,Mathlib/Algebra/Algebra/Subalgebra/Basic.lean,Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean,Mathlib/Algebra/Field/Subfield/Defs.lean,Mathlib/Algebra/Ring/Subring/Defs.lean,Mathlib/Algebra/Ring/Subsemiring/Defs.lean,Mathlib/Algebra/Star/NonUnitalSubalgebra.lean,Mathlib/Algebra/Star/Subalgebra.lean,Mathlib/FieldTheory/IntermediateField/Basic.lean,Mathlib/RingTheory/NonUnitalSubring/Defs.lean,Mathlib/RingTheory/TensorProduct/Basic.lean	11	3	['dagurtomas', 'github-actions']	dagurtomas assignee:dagurtomas	2-31652 2 days ago	11-70482 11 days ago	11-73744 11 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-31508 2 days ago	3-63108 3 days ago	4-67391 4 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-19271 2 days ago	2-38913 2 days ago	28-51601 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	1-76707 1 day ago	13-30644 13 days ago	44-52895 44 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-31878 1 day ago	1-35172 1 day ago	4-55257 4 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-18684 1 day ago	12-16909 12 days ago	12-16822 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-18101 1 day ago	7-78241 7 days ago	11-68181 11 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-11771 1 day ago	2-20923 2 days ago	2-20836 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-5257 1 day ago	11-38791 11 days ago	17-60628 17 days

All maintainer merge'd PRs

Number	Author	Title	Description	Labels	+/-	Modified files (first 100)	📝	💬	All users who commented or reviewed	Assignee(s)	Updated	Last status change	total time in review
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-3907 1 month ago	39-3911 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-25735 1 month ago	33-25735 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-38601 25 days ago	54-33500 54 days ago	54-40680 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-35109 9 days ago	11-14830 11 days ago	19-7859 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-25176 4 days ago	4-70292 4 days ago	10-46848 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-5445 4 days ago	10-4655 10 days ago	168-52617 168 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	3-72785 3 days ago	3-86033 3 days ago	14-13462 14 days
36470	joelriou author:joelriou	feat(CategoryTheory/Monoidal): the left adjoint of a lax monoidal functor is oplax monoidal	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-category-theory maintainer-merge	79/0	Mathlib/CategoryTheory/Monoidal/Functor.lean	1	4	['dagurtomas', 'github-actions']	nobody	3-30181 3 days ago	3-30247 3 days ago	5-21135 5 days
33935	mckoen author:mckoen	feat(CategoryTheory/Monoidal/Arrow): define monoidal structure on arrow category	defines a monoidal category structure on the arrow category of a cartesian closed category. --- - [x] depends on: #33974 - [x] depends on: #34887 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-category-theory maintainer-merge awaiting-author	511/0	Mathlib.lean,Mathlib/CategoryTheory/Monoidal/Arrow.lean,Mathlib/CategoryTheory/Monoidal/Limits/Shapes/Pullback.lean	3	23	['dagurtomas', 'github-actions', 'joelriou', 'mathlib-dependent-issues', 'mckoen']	joelriou assignee:joelriou	3-24622 3 days ago	3-79800 3 days ago	11-73773 11 days
35643	chrisflav author:chrisflav	chore(Algebra): make `TensorProduct.equivOfCompatibleSMul` more linear	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra maintainer-merge label:t-algebra$	64/47	Mathlib/LinearAlgebra/TensorProduct/Associator.lean,Mathlib/LinearAlgebra/TensorProduct/Basic.lean,Mathlib/RingTheory/Coalgebra/TensorProduct.lean,Mathlib/RingTheory/LinearDisjoint.lean,Mathlib/RingTheory/Localization/BaseChange.lean,Mathlib/RingTheory/Smooth/Fiber.lean,Mathlib/RingTheory/TensorProduct/Maps.lean,Mathlib/RingTheory/TensorProduct/Nontrivial.lean	8	17	['chrisflav', 'github-actions', 'kckennylau', 'robin-carlier']	kim-em assignee:kim-em	3-14095 3 days ago	3-19129 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-13352 3 days ago	3-13392 3 days ago	10-15684 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-7584 3 days ago	3-7684 3 days ago	3-75613 3 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-7199 3 days ago	3-31566 3 days ago	8-40642 8 days
33780	ooovi author:ooovi	feat(Geometry/Convex/Cone): lineality space of pointed cones	Define the lineality space `PointedCone.lineal` as the submodule `C ⊓ -C`. Prove that it is the largest submodule of the cone, which is sometimes used as an alternative definition. Co-authored-by: Martin Winter --- dependency of #33664 - [x] depends on #33761 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-convex-geometry maintainer-merge	36/1	Mathlib/Geometry/Convex/Cone/Pointed.lean	1	23	['YaelDillies', 'artie2000', 'eric-wieser', 'github-actions', 'martinwintermath', 'mathlib4-merge-conflict-bot', 'ooovi', 'vihdzp']	nobody	2-81356 2 days ago	2-82038 2 days ago	29-80666 29 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-38951 2 days ago	22-66873 22 days ago	22-66786 22 days
36097	matthewjasper author:matthewjasper	chore: make pseudoparents of algebraic substructures reducible	Make functions that take an algebraic substructure and return a sibling class reducible, this matches actual parents and resolves some usage of `set_option backward.isDefEq.respectTransparency false`. For example it ensures that the field instance on `IntermediateField` has a compatible `Semiring` instance to the one from it extending a `Subalgebra`. Also remove @[simp] from `adjoin_toSubsemiring`, since it prevents other simp lemmas on `adjoin` from applying. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra maintainer-merge label:t-algebra$	23/16	Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean,Mathlib/Algebra/Algebra/Subalgebra/Basic.lean,Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean,Mathlib/Algebra/Field/Subfield/Defs.lean,Mathlib/Algebra/Ring/Subring/Defs.lean,Mathlib/Algebra/Ring/Subsemiring/Defs.lean,Mathlib/Algebra/Star/NonUnitalSubalgebra.lean,Mathlib/Algebra/Star/Subalgebra.lean,Mathlib/FieldTheory/IntermediateField/Basic.lean,Mathlib/RingTheory/NonUnitalSubring/Defs.lean,Mathlib/RingTheory/TensorProduct/Basic.lean	11	3	['dagurtomas', 'github-actions']	dagurtomas assignee:dagurtomas	2-31652 2 days ago	11-70482 11 days ago	11-73744 11 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-31508 2 days ago	3-63108 3 days ago	4-67391 4 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-19271 2 days ago	2-38913 2 days ago	28-51601 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	1-76707 1 day ago	13-30644 13 days ago	44-52895 44 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-31878 1 day ago	1-35172 1 day ago	4-55257 4 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-18684 1 day ago	12-16909 12 days ago	12-16822 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-18101 1 day ago	7-78241 7 days ago	11-68181 11 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-11771 1 day ago	2-20923 2 days ago	2-20836 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-5257 1 day ago	11-38791 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	0-72096 20 hours ago	19-33339 19 days ago	19-80763 19 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	0-62996 17 hours ago	4-37670 4 days ago	5-35947 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-35737 9 hours ago	9-12843 9 days ago	9-16124 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-34329 9 hours ago	1-19745 1 day ago	6-30754 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-26945 7 hours ago	0-27009 7 hours ago	0-28096 7 hours
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']	nobody	0-23446 6 hours ago	1-34930 1 day ago	4-51841 4 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']	nobody	0-17179 4 hours ago	6-75035 6 days ago	8-26347 8 days
36391	xroblot author:xroblot	feat(FieldTheory/Galois/IsGaloisGroup): Galois groups for quotients by normal subgroups	Assume `G `is a finite Galois group for `L/K`, `N ⊴ G` is normal, and `F = Fix(N)`. This PR proves: - `G ⧸ N` acts on `F` via `(g.N) • x := g • x` as a `MulSemiringAction`. Under `SMulCommClass G K L`, it is also `SMulCommClass (G ⧸ N) K F` - instance `quotient` : `IsGaloisGroup (G ⧸ N) K F` — the quotient group is a Galois group for the intermediate extension `F/K`. - theorem `quotientMap` under the hypothesis ` E ≤ F`: `IsGaloisGroup (H.map (QuotientGroup.mk' N)) E F` — if `H` is the Galois group for `L/E`, the image of `H` under the quotient map is a Galois group for `F/E`. --- - [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-16213 4 hours ago	1-30395 1 day ago	1-42958 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-12084 3 hours ago	12-42843 12 days ago	24-21205 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-10987 3 hours ago	3-33140 3 days ago	9-13543 9 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-22557 1 year ago	488-15116 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	325-64334 10 months ago	346-76976 346 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	314-72234 10 months ago	584-9019 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	254-52583 8 months ago	526-226 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-51421 8 months ago	287-26538 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	194-67066 6 months ago	203-18220 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-44276 5 months ago	202-76073 202 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	123-55150 4 months ago	163-33816 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	118-72282 3 months ago	538-13270 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-2123 3 months ago	463-52053 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-39291 3 months ago	314-72220 314 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-11157 3 months ago	592-31439 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	95-79403 3 months ago	148-48256 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-47716 2 months ago	69-8049 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-10151 1 month ago	53-10151 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-14969 1 month ago	46-14969 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-27574 1 month ago	84-4476 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-27379 1 month ago	69-11511 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	34-73388 1 month ago	42-25308 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-45727 26 days ago	54-78862 54 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-38153 26 days ago	199-34471 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-8772 24 days ago	25-31452 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	23-73686 23 days ago	23-73687 23 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-32525 18 days ago	364-10464 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-32509 18 days ago	315-14403 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	17-52538 17 days ago	281-81837 281 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	14-84477 14 days ago	33-72718 33 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-34739 13 days ago	109-38079 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-30752 10 days ago	41-3999 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-3811 10 days ago	21-7918 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-36631 6 days ago	26-39478 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	3-86248 3 days ago	4-32329 4 days ago	0-1564 26 minutes
36698	ghseeli author:ghseeli	feat(Combinatorics/Enumerative): Latin squares	This PR defines Latin rectangles and Latin squares and proves an extension theorem using Hall's Marriage Theorem. ## Main results - `group_to_cayley_table`: every finite group `G` yields a `LatinSquare G G`. - `latin_rectangle_extends_one_row`: a (non-square) `LatinRectangle` extends to a `LatinRectangle` with one more row. This is an application of Hall's Marriage Theorem, `hallMatchingsOn.nonempty`. - `latin_rectangle_extends_to_latin_square`: a `LatinRectangle` extends to a `LatinSquare`. This is included in a new file `Combinatorics/Enumerative/LatinSquare.lean`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor WIP awaiting-zulip t-combinatorics	934/0	Mathlib.lean,Mathlib/Combinatorics/Enumerative/LatinSquare.lean	2	3	['ghseeli', 'github-actions']	nobody	0-55413 15 hours ago	0-72386 20 hours ago	0-170 2 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
36662	plp127 author:plp127	fix(Data/EReal): remove `set_option linter.flexible false`	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-data tech debt	1/5	Mathlib/Data/EReal/Operations.lean	1	1	['github-actions']	nobody	1-53700 1 day ago	1-54980 1 day ago	1-54893 1 day
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	1-53513 1 day ago	1-53591 1 day ago	1-53504 1 day
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-45541 1 day ago	4-60452 4 days ago	4-60365 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	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	10	['github-actions', 'joneugster', 'mathlib-merge-conflicts']	joneugster assignee:joneugster	0-57001 15 hours ago	0-57107 15 hours ago	14-22795 14 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-13374 3 hours ago	0-13407 3 hours ago	3-62868 3 days
36635	Vierkantor author:Vierkantor	chore(*): turn comments before declarations into docstrings	This PR goes through the whole of Mathlib and replaces `/- comments -/` with `/-- docstrings -/` or `/-! module docs -/` whenever they appear before a declaration. A lot of these appear to be simple typos, where a docstring was actually intended. Where a comment was originally intended, I would argue it is still a good idea include the comments in the generated documentation, or at least it does not hurt anyone. These instances were found by a linter, in an upcoming PR. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	tech debt	253/260	Mathlib/Algebra/Algebra/Subalgebra/Basic.lean,Mathlib/Algebra/Category/ModuleCat/Abelian.lean,Mathlib/Algebra/Category/ModuleCat/Semi.lean,Mathlib/Algebra/DirectSum/Internal.lean,Mathlib/Algebra/Group/Defs.lean,Mathlib/Algebra/Group/Subgroup/MulOppositeLemmas.lean,Mathlib/Algebra/Group/Submonoid/Basic.lean,Mathlib/Algebra/Group/Submonoid/Membership.lean,Mathlib/Algebra/Group/Subsemigroup/Basic.lean,Mathlib/Algebra/GroupWithZero/Range.lean,Mathlib/Algebra/Order/Group/Unbundled/Basic.lean,Mathlib/Algebra/Order/GroupWithZero/Unbundled/Defs.lean,Mathlib/Algebra/Order/Monoid/Unbundled/Defs.lean,Mathlib/Algebra/Order/Ring/Star.lean,Mathlib/Algebra/Order/Sub/Defs.lean,Mathlib/Algebra/Polynomial/CoeffList.lean,Mathlib/Algebra/Ring/Ext.lean,Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean,Mathlib/Algebra/Star/SelfAdjoint.lean,Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean,Mathlib/AlgebraicGeometry/Morphisms/WeaklyEtale.lean,Mathlib/Analysis/Analytic/Constructions.lean,Mathlib/Analysis/CStarAlgebra/Module/Constructions.lean,Mathlib/Analysis/CStarAlgebra/Module/Synonym.lean,Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean,Mathlib/Analysis/Complex/UpperHalfPlane/MoebiusAction.lean,Mathlib/Analysis/Convex/Function.lean,Mathlib/Analysis/Distribution/SchwartzSpace/Fourier.lean,Mathlib/Analysis/Distribution/TemperedDistribution.lean,Mathlib/Analysis/Fourier/Convolution.lean,Mathlib/Analysis/InnerProductSpace/Adjoint.lean,Mathlib/Analysis/InnerProductSpace/Orthogonal.lean,Mathlib/Analysis/InnerProductSpace/TensorProduct.lean,Mathlib/Analysis/LConvolution.lean,Mathlib/Analysis/LocallyConvex/WeakDual.lean,Mathlib/Analysis/Meromorphic/Basic.lean,Mathlib/Analysis/Normed/Algebra/GelfandMazur.lean,Mathlib/Analysis/Normed/Algebra/Unitization.lean,Mathlib/Analysis/Normed/Module/FiniteDimension.lean,Mathlib/Analysis/Normed/Module/MStructure.lean,Mathlib/Analysis/Normed/Operator/Banach.lean,Mathlib/Analysis/Normed/Operator/ContinuousAlgEquiv.lean,Mathlib/Analysis/RCLike/Basic.lean,Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean,Mathlib/CategoryTheory/Action/Concrete.lean,Mathlib/CategoryTheory/Equivalence.lean,Mathlib/CategoryTheory/FintypeCat.lean,Mathlib/CategoryTheory/Iso.lean,Mathlib/CategoryTheory/Limits/Cones.lean,Mathlib/CategoryTheory/Limits/FintypeCat.lean,Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean,Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean,Mathlib/CategoryTheory/Monoidal/Closed/Ideal.lean,Mathlib/CategoryTheory/Products/Basic.lean,Mathlib/Combinatorics/Hindman.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean,Mathlib/Combinatorics/SimpleGraph/Hall.lean,Mathlib/Data/Complex/Basic.lean,Mathlib/Data/ENNReal/Holder.lean,Mathlib/Data/Finset/Sym.lean,Mathlib/Data/Fintype/Sets.lean,Mathlib/Data/Nat/Multiplicity.lean,Mathlib/Data/Set/Pointwise/Support.lean,Mathlib/Data/Set/Semiring.lean,Mathlib/Data/Sign/Defs.lean,Mathlib/FieldTheory/RatFunc/AsPolynomial.lean,Mathlib/Geometry/Euclidean/Volume/Measure.lean,Mathlib/GroupTheory/Coset/Defs.lean,Mathlib/GroupTheory/FreeGroup/IsFreeGroup.lean,Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean,Mathlib/GroupTheory/GroupAction/SubMulAction.lean,Mathlib/GroupTheory/OrderOfElement.lean,Mathlib/GroupTheory/OreLocalization/Basic.lean,Mathlib/GroupTheory/QuotientGroup/Defs.lean,Mathlib/GroupTheory/SpecificGroups/Alternating/MaximalSubgroups.lean,Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean,Mathlib/LinearAlgebra/Complex/Module.lean,Mathlib/LinearAlgebra/DFinsupp.lean,Mathlib/LinearAlgebra/Isomorphisms.lean,Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean,Mathlib/LinearAlgebra/PiTensorProduct.lean,Mathlib/Logic/Basic.lean,Mathlib/Logic/UnivLE.lean,Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean,Mathlib/MeasureTheory/Function/ConditionalLExpectation.lean,Mathlib/MeasureTheory/Function/JacobianOneDim.lean,Mathlib/MeasureTheory/Function/UniformIntegrable.lean,Mathlib/MeasureTheory/Group/Measure.lean,Mathlib/MeasureTheory/Integral/Lebesgue/Add.lean,Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean,Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean,Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean,Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean,Mathlib/ModelTheory/Algebra/Field/CharP.lean,Mathlib/NumberTheory/Chebyshev.lean,Mathlib/NumberTheory/NumberField/Cyclotomic/Basic.lean,Mathlib/Order/BooleanAlgebra/Basic.lean,Mathlib/Order/BourbakiWitt.lean,Mathlib/Order/CompleteLattice/Basic.lean	139	1	['github-actions']	nobody	0-13151 3 hours ago	0-13176 3 hours ago	0-13132 3 hours
36725	vlad902 author:vlad902	chore(Algebra): remove some `set_option linter.flexible false`	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra tech debt label:t-algebra$	4/13	Mathlib/Algebra/Group/Submonoid/Basic.lean,Mathlib/Algebra/LinearRecurrence.lean,Mathlib/Algebra/Module/ZLattice/Summable.lean,Mathlib/Algebra/Ring/Subring/Basic.lean	4	3	['github-actions', 'grunweg', 'vlad902']	nobody	0-8366 2 hours ago	0-8433 2 hours ago	0-20364 5 hours
36738	vlad902 author:vlad902	chore(*): remove some `set_option linter.flexible false`	These `set_option`s are derived from the fact that prior to #29027, linarith and nlinarith were not properly marked as flexible. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	tech debt	0/9	Mathlib/Analysis/Calculus/LHopital.lean,Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean,Mathlib/Combinatorics/Additive/SmallTripling.lean	4	1	['github-actions']	nobody	0-2681 44 minutes ago	0-8249 2 hours ago	0-8162 2 hours
36741	vlad902 author:vlad902	chore(*): golf and 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	6/24	Mathlib/Combinatorics/Additive/Corner/Roth.lean,Mathlib/GroupTheory/FreeGroup/Basic.lean,Mathlib/GroupTheory/HNNExtension.lean,Mathlib/NumberTheory/PellMatiyasevic.lean,Mathlib/Topology/Piecewise.lean	5	1	['github-actions']	nobody	0-2078 34 minutes ago	0-2147 34 minutes ago	0-2060 34 minutes
36742	vlad902 author:vlad902	chore(*): 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	12/25	Mathlib/AlgebraicGeometry/Cover/Directed.lean,Mathlib/Logic/Equiv/List.lean,Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean,Mathlib/RingTheory/Valuation/ValuativeRel/Basic.lean,Mathlib/SetTheory/Ordinal/Notation.lean,Mathlib/Tactic/NormNum/Irrational.lean	6	1	['github-actions']	nobody	0-1977 32 minutes ago	0-2071 33 minutes ago	0-1984 33 minutes