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: April 22, 2026 at 18:35 UTC

Stale ready-to-merge'd PRs

There are currently no stale PRs labelled auto-merge-after-CI or ready-to-merge. Congratulations!

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
36216	michaellee94 author:michaellee94	feat(CategoryTheory): characterize pullback squares via the `Over` category	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-category-theory new-contributor maintainer-merge awaiting-author	47/0	Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean	1	18	['dagurtomas', 'github-actions', 'joelriou', 'michaellee94']	robin-carlier assignee:robin-carlier	26-77992 26 days ago	26-77992 26 days ago	2-43344 2 days
37057	erdOne author:erdOne	feat(AlgebraicTopology): `SimplexCategory.toTop_map_δ_apply`	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebraic-topology maintainer-merge awaiting-author merge-conflict	48/2	Mathlib/AlgebraicTopology/CechNerve.lean,Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean,Mathlib/AlgebraicTopology/SimplexCategory/Defs.lean,Mathlib/AlgebraicTopology/TopologicalSimplex.lean,Mathlib/Data/Fin/SuccPred.lean	5	17	['Raph-DG', 'dagurtomas', 'erdOne', 'github-actions', 'joelriou', 'mathlib-merge-conflicts', 'riccardobrasca']	robin-carlier assignee:robin-carlier	14-44795 14 days ago	16-6035 16 days ago	4-43742 4 days
37603	Parcly-Taxel author:Parcly-Taxel	refactor: review of `SetSemiring`	* Rename `Set.up` and `SetSemiring.down` to `SetSemiring.ofSet` and `SetSemiring.toSet` respectively. Unprotect both and make them equivalences, following `FreeMonoid`. * Derive `CompleteAtomicBooleanAlgebra` for `SetSemiring` immediately. * Add `imageHom_id` and `imageHom_comp`. The three existing lemmas about `imageHom` are coalesced into `imageHom_apply`. Ultimately inspired by https://github.com/leanprover-community/mathlib4/pull/36934#issuecomment-4183475568.	maintainer-merge	120/165	Mathlib/Algebra/Algebra/Operations.lean,Mathlib/Data/Set/Semiring.lean	2	41	['Parcly-Taxel', 'YaelDillies', 'eric-wieser', 'github-actions', 'mathlib-merge-conflicts', 'sgouezel']	nobody	14-14782 14 days ago	14-9990 14 days ago	15-14186 15 days
33443	sahanwijetunga author:sahanwijetunga	feat: Define Isometries of Bilinear Spaces	--- We define Isometries of Bilinear Spaces, closely following the implementation of isometries of quadratic spaces. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra new-contributor maintainer-merge label:t-algebra$	278/0	Mathlib.lean,Mathlib/LinearAlgebra/BilinearForm/Isometry.lean,Mathlib/LinearAlgebra/BilinearForm/IsometryEquiv.lean	3	25	['github-actions', 'robin-carlier', 'sahanwijetunga']	mattrobball assignee:mattrobball	12-39029 12 days ago	12-39188 12 days ago	60-60774 60 days
37846	grunweg author:grunweg	fix(positivity): still prove non-negativity in the `Nat.cast` extension if positivity fails	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-meta maintainer-merge	11/2	Mathlib/Tactic/Positivity/Basic.lean,MathlibTest/positivity.lean	2	4	['dwrensha', 'github-actions']	dwrensha assignee:dwrensha	11-61076 11 days ago	12-22585 12 days ago	12-22118 12 days
37592	erdOne author:erdOne	feat: set up API for `ConvexSpace`	We introduce `sConvexCombo` and the indexed version `iConvexCombo` as the main API for `ConvexSpace` and prove lemmas around the new definitions. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra large-import maintainer-merge awaiting-author label:t-algebra$	452/133	Mathlib/Analysis/Convex/MetricSpace.lean,Mathlib/LinearAlgebra/ConvexSpace.lean,Mathlib/LinearAlgebra/ConvexSpace/AffineSpace.lean	3	37	['YaelDillies', 'erdOne', 'faenuccio', 'github-actions']	faenuccio assignee:faenuccio	10-12720 10 days ago	15-40347 15 days ago	3-61210 3 days
30077	agjftucker author:agjftucker	feat(Analysis/Calculus/ImplicitFunction): define implicitFunctionOfBivariate	Introduce a further specialization of the implicit function theorem; one which applies to a curried bivariate function. --- - [x] depends on: #26985 This is in large part a response to sgouezel's review comment on #16743 > The real question is whether it's best to formulate the result for curried or uncurried function. My bet is that curried would be better since most functions on products in fact come in curried form, but since you've already written fully the uncurried version (and a todo saying that it would be good having the curried version as well), let's keep it like that for now. #26985 reviewed by j-loreaux and later on by winstonyin. #16743 and #26300 reviewed by sgouezel. [Zulip chat](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Inverse.20function.20theorem.20and.20ContinuousLinearEquiv/with/567586606) with Yury Kudryashov. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-analysis maintainer-merge	187/0	Mathlib.lean,Mathlib/Analysis/Calculus/FDeriv/Partial.lean,Mathlib/Analysis/Calculus/ImplicitFunction/Bivariate.lean,Mathlib/Analysis/Calculus/ImplicitFunction/ProdDomain.lean	4	14	['agjftucker', 'github-actions', 'j-loreaux', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'mathlib4-merge-conflict-bot']	j-loreaux assignee:j-loreaux	9-15019 9 days ago	9-13728 9 days ago	60-68422 60 days
37053	artie2000 author:artie2000	refactor(Analysis/Convex/Cone): use `PointedCone` in Riesz extension theorem	Change the statement of the Riesz extension theorem to take a `PointedCone` rather than a `ConvexCone`. This PR is part of a series replacing `ConvexCone` with `PointedCone`. https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Replacing.20.60ConvexCone.60.20with.20.60PointedCone.60/near/581184307 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-convex-geometry maintainer-merge	15/12	Mathlib/Analysis/Convex/Cone/Extension.lean,Mathlib/Geometry/Convex/Cone/Pointed.lean	2	8	['YaelDillies', 'artie2000', 'github-actions', 'mathlib-merge-conflicts', 'ocfnash']	nobody	8-18337 8 days ago	8-17369 8 days ago	27-52687 27 days
36308	SnirBroshi author:SnirBroshi	feat(Combinatorics/SimpleGraph/Subgraph): a couple of `subgraphOfAdj` lemmas	Also golf a lemma (it's one line longer but it looks simpler to me). --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics maintainer-merge	14/5	Mathlib/Combinatorics/SimpleGraph/Subgraph.lean	1	4	['SnirBroshi', 'YaelDillies', 'github-actions']	b-mehta assignee:b-mehta	7-62884 7 days ago	46-41825 46 days ago	46-41358 46 days
37400	SnirBroshi author:SnirBroshi	feat(Combinatorics/SimpleGraph/Acyclic): endpoints of a path have at most one neighbor in the path	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics maintainer-merge	15/0	Mathlib/Combinatorics/SimpleGraph/Acyclic.lean	1	5	['Rida-Hamadani', 'Ruben-VandeVelde', 'SnirBroshi', 'github-actions']	nobody	6-57605 6 days ago	20-17652 20 days ago	22-55285 22 days
37420	artie2000 author:artie2000	refactor: change definitions to avoid `ConvexCone`	Change the definitions of `PointedCone.positive` and `PointedCone.closure` to avoid mentioning `ConvexCone`. This PR is part of a series deprecating `ConvexCone`: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Replacing.20.60ConvexCone.60.20with.20.60PointedCone.60/with/582738985 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-convex-geometry maintainer-merge	10/4	Mathlib/Analysis/Convex/Cone/Closure.lean,Mathlib/Geometry/Convex/Cone/Pointed.lean	2	3	['YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'ooovi', 'vihdzp']	nobody	6-24389 6 days ago	6-23637 6 days ago	21-42789 21 days
37393	SnirBroshi author:SnirBroshi	refactor(Algebra/Order/Monoid/Unbundled/Defs): upgrade `*ReflectLE` from `abbrev`s to `class`es	... to mitigate performance regression caused by #36629. Currently the 4 classes `{Mul/Add}{Left/Right}ReflectLE` are an `abbrev` for `ContravariantClass` so when TC-search tries to synthesize them it ends up looking through all the `ContravariantClass` instances and not just the relevant ones. --- [Zulip](https://leanprover.zulipchat.com/#narrow/channel/116290-rss/topic/Significant.20commits.20to.20mathlib4/near/582661644) [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra maintainer-merge label:t-algebra$	76/69	Mathlib/Algebra/Order/Group/Multiset.lean,Mathlib/Algebra/Order/GroupWithZero/Unbundled/Defs.lean,Mathlib/Algebra/Order/Monoid/Defs.lean,Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean,Mathlib/Algebra/Order/Monoid/Unbundled/Defs.lean,Mathlib/Algebra/Order/Monoid/Unbundled/OrderDual.lean,Mathlib/Algebra/Order/Positive/Ring.lean,Mathlib/Data/DFinsupp/Order.lean,Mathlib/Data/Finsupp/Order.lean,Mathlib/SetTheory/Ordinal/Arithmetic.lean	10	14	['JovanGerb', 'SnirBroshi', 'github-actions', 'leanprover-radar', 'vihdzp']	kim-em assignee:kim-em	5-83732 5 days ago	6-2718 6 days ago	22-26112 22 days
37864	JovanGerb author:JovanGerb	chore: reorder arguments of `AddMonoidHom.map_zsmul`	This PR modifies `AddMonoidHom.map_nsmul`, `AddMonoidHom.map_zsmul` and `AddMonoidHom.map_zsmul'` so that their order of arguments is as expected. This is then consistent with `map_nsmul`/`map_zsmul`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra maintainer-merge label:t-algebra$	21/22	Mathlib/Algebra/Category/Grp/ZModuleEquivalence.lean,Mathlib/Algebra/Group/Hom/Defs.lean,Mathlib/Algebra/GroupWithZero/Action/Defs.lean,Mathlib/Algebra/Module/CharacterModule.lean,Mathlib/Algebra/Module/Equiv/Basic.lean,Mathlib/Analysis/Complex/Circle.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean,Mathlib/CategoryTheory/Linear/Basic.lean,Mathlib/CategoryTheory/Linear/LinearFunctor.lean	9	8	['JovanGerb', 'github-actions', 'mathlib-merge-conflicts', 'themathqueen']	nobody	5-27722 5 days ago	5-30346 5 days ago	10-33669 10 days
37588	Vierkantor author:Vierkantor	feat(Linter/DocString): ignore Verso linter errors about links and LaTeX	I went through [the weekly linting log](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Weekly.20linting.20log/near/582485221) and found most of the warnings come from three sources. All of these are sensical syntax in our current Markdown dialect, and should be fixed automatically by a script, instead of manually. I expect after these changes we'll be down to hundreds of linter errors rather than two thousand. * References [between square brackets] without a following link URL. Verso has different implementations for references depending on what kind they are, and since there are a thousand references we should be using a script to fix these. * Autolinks: bare URLs or URLs between . Autolinks are intentionally not supported by Verso but replacing every `https://...` with `[https://...](https://...)` would be too noisy. * LaTeX blocks: Verso does have TeX blocks but with an incompatible syntax. Better to fix it with a script. I ended up using preprocessing in addition to postprocessing to filter out errors: using the error message we can determine whether it is a reference, but for errors caused by autolinks and LaTeX blocks I couldn't figure out how to do so easily: the information about the parse error does report a string position but this is always the last character of the docstring. So instead we modify the docstring before it is passed into Verso to get rid of the offending syntax. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-linter large-import maintainer-merge	113/5	Mathlib/Tactic/Linter/DocString.lean,MathlibTest/DocString.lean	2	18	['Vierkantor', 'github-actions', 'thorimur']	thorimur assignee:thorimur	5-20615 5 days ago	5-17005 5 days ago	8-1503 8 days
37808	JovanGerb author:JovanGerb	feat(Translate): locally modify name guessing dictionaries	This PR adds the feature to `to_dual` and `to_additive` that you can now locally modify the name translation dictionary. With this change, we run the risk of having the automated translations being harder to predict. For this reason, the changes to the dictionary do not persisted through imports. Instead, the change lasts until the end of the file (though it ignores sections). See https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Order.20dual.20tactic/near/580834166 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-meta maintainer-merge	111/39	Mathlib/Order/GaloisConnection/Basic.lean,Mathlib/Order/GaloisConnection/Defs.lean,Mathlib/Order/Interval/Set/Basic.lean,Mathlib/Order/Interval/Set/Disjoint.lean,Mathlib/Tactic/Translate/Core.lean,Mathlib/Tactic/Translate/GuessName.lean,Mathlib/Tactic/Translate/ToAdditive.lean,Mathlib/Tactic/Translate/ToDual.lean,MathlibTest/ToDual.lean	9	4	['JovanGerb', 'bryangingechen', 'github-actions', 'joneugster']	joneugster assignee:joneugster	5-20482 5 days ago	10-13121 10 days ago	10-12654 10 days
37411	vasnesterov author:vasnesterov	feat(Tactic/ComputeAsymptotics/Multiseries): introduce `Monomial`	* Introduce `Monomial` and `UnitMonomial` * Define `Monomial.toFun` and algebraic operations on monomials: negation, inversion, multiplication. --- - [x] depends on: #37414 This is a part of the `compute_asymptotics` tactic (#28291). [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-meta maintainer-merge	232/0	Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/ComputeAsymptotics/Multiseries/Monomial/Basic.lean	3	9	['github-actions', 'joneugster', 'mathlib-dependent-issues']	joneugster assignee:joneugster	5-6649 5 days ago	5-5887 5 days ago	5-11122 5 days
37418	vasnesterov author:vasnesterov	feat(Tactic/ComputeAsymptotics/Multiseries): introduce `Multiseries.Sorted`	* Introduce `Multiseries.leadingExp` - the leading exponent of a multiseries, along with a few structural lemmas. * Introduce `Multiseries.Sorted` predicate stating that exponents in a multiseries as a list are strictly decreasing. * Provide constructors (`nil`, `cons`), a coinductive principle, and basic constructions for `Sorted`. --- This is a part of the `compute_asymptotics` tactic (#28291). [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-meta maintainer-merge	201/0	Mathlib/Tactic/ComputeAsymptotics/Multiseries/Defs.lean	1	32	['github-actions', 'joneugster', 'mathlib-merge-conflicts', 'vasnesterov']	joneugster assignee:joneugster	5-6526 5 days ago	5-7255 5 days ago	21-41738 21 days
38179	wwylele author:wwylele	feat(Combinatorics): Pentagonal numbers	Introduces definition of pentagonal number https://en.wikipedia.org/wiki/Pentagonal_number in preparation for pentagonal number theorem. --- This is extracted from #33143 as suggested. I only put a few elementary properties here to limit the code change size. The future file structure will be - Combinatorics/Enumerative/Pentagonal.lean (this PR) - Topology/Algebra/InfiniteSum/Pentagonal.lean + RingTheory/PowerSeries/Pentagonal.lean (#33143, depends on previous one) pentagonal theorem in generic form and for power series - Combinatorics/Enumerative/Partition/Pentagonal.lean (future PR, depends on the previous one): connection between partition and pentagonal numbers This originally comes from my own repo https://github.com/wwylele/PentagonalNumberTheorem. In the past, there were also PR #31156 and #31362 independently worked by @BeibeiX0 on the same topic, and I tried avoiding stepping on each other's toes when making #33143. Then #31156 and #31362 were closed for unclear reason. As I mostly rewrote the code based on my own repo, I only put my name here, but given that I unavoidably took inspiration from other PRs, if @BeibeiX0 would like his name to be added to co-author and copyright notice, I am happy to do so. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics maintainer-merge	75/0	Mathlib.lean,Mathlib/Combinatorics/Enumerative/Pentagonal.lean	2	27	['copilot-pull-request-reviewer', 'github-actions', 'tb65536', 'wwylele']	nobody	4-70524 4 days ago	4-71096 4 days ago	4-76787 4 days
37931	Vierkantor author:Vierkantor	chore(Tactic): make the (deprecated) `replace` syntax a `@[tactic_alt]`	This PR replaces the tactic docstring for Mathlib's version of `replace` with a `@[tactic_alt]` attribute + `tactic_extension`. Also update the module docs which did not get updated when `replace` got upstreamed to core Lean. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	documentation t-meta maintainer-merge	7/31	Mathlib/Tactic/Replace.lean	1	2	['github-actions', 'joneugster']	dwrensha assignee:dwrensha	3-62781 3 days ago	9-11070 9 days ago	9-10603 9 days
35906	scp020 author:scp020	feat(Combinatorics/SimpleGraph/Walk): chords of walks	Define `Walk.IsChord` and `Walk.IsChordless` predicates in a new file `SimpleGraph/Walk/Chord.lean`. See "chord" in https://en.wikipedia.org/wiki/Glossary_of_graph_theory --- [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Walk.2EIsChordless.20live.20in.20mathlib.3F/with/575277309) [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics new-contributor maintainer-merge	59/0	Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Walk/Chord.lean	2	68	['SnirBroshi', 'YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'scp020']	YaelDillies assignee:YaelDillies	3-5394 3 days ago	3-4760 3 days ago	42-35916 42 days
37868	Jun2M author:Jun2M	feat(Combinatorics/Graph): map on `Graph`	This PR introduces vertex map on graphs, `map`. This creates a new file `Maps` which will be home to `map` and morphisms between `Graph`s. Co-authored-by: Peter Nelson [apn.uni@gmail.com](mailto:apn.uni@gmail.com) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics maintainer-merge	108/0	Mathlib.lean,Mathlib/Combinatorics/Graph/Maps.lean	2	8	['Jun2M', 'YaelDillies', 'b-mehta', 'github-actions', 'mathlib-merge-conflicts']	nobody	2-3332 2 days ago	2-3332 2 days ago	12-13565 12 days
37171	SnirBroshi author:SnirBroshi	chore(Data/Int/Init): generalize `le_induction` from `Prop` to `Sort*` + def lemmas	--- [Zulip 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Add.20note.20to.20help.20search.20similar.20thms/near/535331432) [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-data large-import maintainer-merge	56/48	Mathlib/Data/Int/Basic.lean,Mathlib/Data/Int/Init.lean,Mathlib/GroupTheory/CoprodI.lean	3	8	['SnirBroshi', 'github-actions', 'joneugster', 'mathlib-merge-conflicts', 'plp127']	joneugster assignee:joneugster	2-2080 2 days ago	21-48946 21 days ago	22-44713 22 days
38301	SnirBroshi author:SnirBroshi	feat(Algebra/Group/Commutator): tag `addCommutatorElement` as a scoped instance	#34784 additivized commutators and made the multiplicative commutator instance available under `open scoped commutatorElement`. This makes the additive instance available under `open scoped addCommutatorElement`. --- ~~Should we instead make it scoped under the `addCommutatorElement` namespace? The existing usages of additive commutators come from decls marked with `open scoped commutatorElement in @[to_additive]`, and `to_additive` seemingly doesn't mind that the additivized version is not an instance. So I think they don't have to live in the same namespace.~~ [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra maintainer-merge label:t-algebra$	6/0	Mathlib/Algebra/Group/Commutator.lean	1	6	['SnirBroshi', 'github-actions', 'tb65536']	nobody	2-1673 2 days ago	2-1816 2 days ago	2-1349 2 days
37941	NoahW314 author:NoahW314	feat(RingTheory/MvPolynomial/Homogeneous): add `homogeneousComponent` lemma	Add a lemma about the `support` of the `(weighted)HomogeneousComponent` of a `MvPolynomial`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-ring-theory maintainer-merge	10/0	Mathlib/RingTheory/MvPolynomial/Homogeneous.lean,Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean	2	3	['github-actions', 'mathlib-merge-conflicts', 'robin-carlier']	robin-carlier assignee:robin-carlier	1-36759 1 day ago	4-63284 4 days ago	10-48601 10 days
38172	joelriou author:joelriou	feat(AlgebraicTopology/SimplicialSet): Mulstruct.mulOne and oneMul	We introduce definitions `SSet.PtSimplex.MulStruct.oneMul/mulOne` which shall later be interpreted as an explanation for the relations satisfied by the neutral element for the multiplication on homotopy groups of Kan complexes. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebraic-topology maintainer-merge	53/0	Mathlib/AlgebraicTopology/SimplicialSet/KanComplex/MulStruct.lean	1	6	['github-actions', 'joelriou', 'robin-carlier']	robin-carlier assignee:robin-carlier	1-22284 1 day ago	1-22459 1 day ago	5-4086 5 days
34854	GrigorenkoPV author:GrigorenkoPV	chore(Combinatorics/Enumerative/Catalan): split into `Basic` & `Tree`	--- Split off from #34853 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-combinatorics maintainer-merge awaiting-author	225/194	Mathlib.lean,Mathlib/Combinatorics/Enumerative/Catalan.lean,Mathlib/Combinatorics/Enumerative/Catalan/Basic.lean,Mathlib/Combinatorics/Enumerative/Catalan/Tree.lean,Mathlib/Combinatorics/Enumerative/DyckWord.lean,Mathlib/RingTheory/PowerSeries/Catalan.lean	6	7	['SnirBroshi', 'Vierkantor', 'YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'vihdzp']	nobody	1-19558 1 day ago	10-27179 10 days ago	45-55669 45 days
36401	JovanGerb author:JovanGerb	feat(positivity): positivity extension for `a - b`	This PR adds support in `positivity` for proving things about subtraction. For example, if the goal is `0 < a - b`, and there is a local hypothesis of type `b < a`, then we close the goal. The motivation is that we want `positivity` to be a flexible tactic. So, when trying to prove `0 < a - b` using a local hypothesis, we should look for the simp normal form of this, which is `b < a`. --- [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Can.20I.20make.20positivity.20work.20for.20this.3F/near/578277240) [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-meta maintainer-merge	63/26	Mathlib/Analysis/Calculus/Taylor.lean,Mathlib/Analysis/Complex/AbelLimit.lean,Mathlib/Analysis/Complex/BorelCaratheodory.lean,Mathlib/Analysis/Complex/Hadamard.lean,Mathlib/Analysis/Convex/BetweenList.lean,Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean,Mathlib/Analysis/SpecificLimits/FloorPow.lean,Mathlib/Geometry/Manifold/Riemannian/PathELength.lean,Mathlib/Tactic/Positivity/Basic.lean,MathlibTest/positivity.lean	10	12	['JovanGerb', 'Vierkantor', 'github-actions', 'hrmacbeth', 'j-loreaux', 'joneugster', 'leanprover-radar']	joneugster assignee:joneugster	1-16823 1 day ago	1-16823 1 day ago	29-80546 29 days
38257	joelriou author:joelriou	feat(CategoryTheory): MorphismProperty.single	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-category-theory maintainer-merge	63/1	Mathlib/CategoryTheory/MorphismProperty/Basic.lean,Mathlib/CategoryTheory/MorphismProperty/IsSmall.lean,Mathlib/CategoryTheory/ObjectProperty/Local.lean	3	6	['github-actions', 'joelriou', 'robin-carlier']	nobody	1-16009 1 day ago	1-16233 1 day ago	2-84231 2 days
38083	tb65536 author:tb65536	feat(RingTheory/DiscreteValuationRing/Basic): compute the length of the quotient of a DVR	This PR computes the length of the quotient of a DVR by constructing an order isomorphism between the ideals and the order dual of `ENat`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-ring-theory t-algebra large-import maintainer-merge label:t-algebra$	55/0	Mathlib/RingTheory/DiscreteValuationRing/Basic.lean,Mathlib/RingTheory/PrincipalIdealDomain.lean	2	9	['github-actions', 'robin-carlier', 'tb65536']	robin-carlier assignee:robin-carlier	1-14947 1 day ago	1-14126 1 day ago	6-80918 6 days
38161	ADedecker author:ADedecker	fix: wrong set-builder syntax in the definition of `CompactConvergenceCLM`	See https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Simp.20failure.20due.20to.20set.20builder.20notation/near/586133497 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-topology easy maintainer-merge	1/1	Mathlib/Topology/Algebra/Module/Spaces/CompactConvergenceCLM.lean	1	3	['github-actions', 'themathqueen']	j-loreaux assignee:j-loreaux	1-9884 1 day ago	5-16996 5 days ago	5-16529 5 days
37347	JovanGerb author:JovanGerb	feat: implementation of `@[use_set_notation_for_order]`	This PR allows the use of `⊆` notation while the underlying constant is `≤`. Similarly for `⊂`/`<`, `⊇`/`≥` and `⊃`/`>`. - The idea is to later extend this feature to other set notation constants, such as union/intersection. - There are some types for which we cannot use `LE.le` as the underlying constant, such as `List` and `Multiset`. So, the elaborator for the `⊆` notation needs to make a decision which underlying constant to elaborate to, depending on the type. Sometimes the type is not known yet, which makes things awkward. Most of these cases are solved by delaying the elaboration until later when the type is known. - However, in some cases this doesn't work either, such as `simp_rw [and_comm (_ ⊆ _)]`, where it is impossible to tell the type when elaborating the term. So, some such cases need to be fixed by making it `simp_rw [and_comm (_ ≤ _)]`. This is because `simp_rw`, unlike `rw`, fully elaborates the rewrite rules before using them. So, when we get the new rewrite tactic, this problem will mostly go away. See also https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Any.20infimum.20based.20version.20of.20.60OmegaCompletePartialOrder.60.3F/near/579333629 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-meta maintainer-merge	345/0	Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/SetNotationForOrder.lean,MathlibTest/SetNotationForOrder.lean	4	48	['JovanGerb', 'Vierkantor', 'github-actions', 'thorimur']	alexjbest and thorimur assignee:alexjbest assignee:thorimur	1-1043 1 day ago	1-16676 1 day ago	23-1393 23 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
36216	michaellee94 author:michaellee94	feat(CategoryTheory): characterize pullback squares via the `Over` category	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-category-theory new-contributor maintainer-merge awaiting-author	47/0	Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean	1	18	['dagurtomas', 'github-actions', 'joelriou', 'michaellee94']	robin-carlier assignee:robin-carlier	26-77992 26 days ago	26-77992 26 days ago	2-43344 2 days
37057	erdOne author:erdOne	feat(AlgebraicTopology): `SimplexCategory.toTop_map_δ_apply`	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebraic-topology maintainer-merge awaiting-author merge-conflict	48/2	Mathlib/AlgebraicTopology/CechNerve.lean,Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean,Mathlib/AlgebraicTopology/SimplexCategory/Defs.lean,Mathlib/AlgebraicTopology/TopologicalSimplex.lean,Mathlib/Data/Fin/SuccPred.lean	5	17	['Raph-DG', 'dagurtomas', 'erdOne', 'github-actions', 'joelriou', 'mathlib-merge-conflicts', 'riccardobrasca']	robin-carlier assignee:robin-carlier	14-44795 14 days ago	16-6035 16 days ago	4-43742 4 days
37603	Parcly-Taxel author:Parcly-Taxel	refactor: review of `SetSemiring`	* Rename `Set.up` and `SetSemiring.down` to `SetSemiring.ofSet` and `SetSemiring.toSet` respectively. Unprotect both and make them equivalences, following `FreeMonoid`. * Derive `CompleteAtomicBooleanAlgebra` for `SetSemiring` immediately. * Add `imageHom_id` and `imageHom_comp`. The three existing lemmas about `imageHom` are coalesced into `imageHom_apply`. Ultimately inspired by https://github.com/leanprover-community/mathlib4/pull/36934#issuecomment-4183475568.	maintainer-merge	120/165	Mathlib/Algebra/Algebra/Operations.lean,Mathlib/Data/Set/Semiring.lean	2	41	['Parcly-Taxel', 'YaelDillies', 'eric-wieser', 'github-actions', 'mathlib-merge-conflicts', 'sgouezel']	nobody	14-14782 14 days ago	14-9990 14 days ago	15-14186 15 days
33443	sahanwijetunga author:sahanwijetunga	feat: Define Isometries of Bilinear Spaces	--- We define Isometries of Bilinear Spaces, closely following the implementation of isometries of quadratic spaces. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra new-contributor maintainer-merge label:t-algebra$	278/0	Mathlib.lean,Mathlib/LinearAlgebra/BilinearForm/Isometry.lean,Mathlib/LinearAlgebra/BilinearForm/IsometryEquiv.lean	3	25	['github-actions', 'robin-carlier', 'sahanwijetunga']	mattrobball assignee:mattrobball	12-39029 12 days ago	12-39188 12 days ago	60-60774 60 days
37846	grunweg author:grunweg	fix(positivity): still prove non-negativity in the `Nat.cast` extension if positivity fails	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-meta maintainer-merge	11/2	Mathlib/Tactic/Positivity/Basic.lean,MathlibTest/positivity.lean	2	4	['dwrensha', 'github-actions']	dwrensha assignee:dwrensha	11-61076 11 days ago	12-22585 12 days ago	12-22118 12 days
37592	erdOne author:erdOne	feat: set up API for `ConvexSpace`	We introduce `sConvexCombo` and the indexed version `iConvexCombo` as the main API for `ConvexSpace` and prove lemmas around the new definitions. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra large-import maintainer-merge awaiting-author label:t-algebra$	452/133	Mathlib/Analysis/Convex/MetricSpace.lean,Mathlib/LinearAlgebra/ConvexSpace.lean,Mathlib/LinearAlgebra/ConvexSpace/AffineSpace.lean	3	37	['YaelDillies', 'erdOne', 'faenuccio', 'github-actions']	faenuccio assignee:faenuccio	10-12720 10 days ago	15-40347 15 days ago	3-61210 3 days
30077	agjftucker author:agjftucker	feat(Analysis/Calculus/ImplicitFunction): define implicitFunctionOfBivariate	Introduce a further specialization of the implicit function theorem; one which applies to a curried bivariate function. --- - [x] depends on: #26985 This is in large part a response to sgouezel's review comment on #16743 > The real question is whether it's best to formulate the result for curried or uncurried function. My bet is that curried would be better since most functions on products in fact come in curried form, but since you've already written fully the uncurried version (and a todo saying that it would be good having the curried version as well), let's keep it like that for now. #26985 reviewed by j-loreaux and later on by winstonyin. #16743 and #26300 reviewed by sgouezel. [Zulip chat](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Inverse.20function.20theorem.20and.20ContinuousLinearEquiv/with/567586606) with Yury Kudryashov. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-analysis maintainer-merge	187/0	Mathlib.lean,Mathlib/Analysis/Calculus/FDeriv/Partial.lean,Mathlib/Analysis/Calculus/ImplicitFunction/Bivariate.lean,Mathlib/Analysis/Calculus/ImplicitFunction/ProdDomain.lean	4	14	['agjftucker', 'github-actions', 'j-loreaux', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'mathlib4-merge-conflict-bot']	j-loreaux assignee:j-loreaux	9-15019 9 days ago	9-13728 9 days ago	60-68422 60 days
37053	artie2000 author:artie2000	refactor(Analysis/Convex/Cone): use `PointedCone` in Riesz extension theorem	Change the statement of the Riesz extension theorem to take a `PointedCone` rather than a `ConvexCone`. This PR is part of a series replacing `ConvexCone` with `PointedCone`. https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Replacing.20.60ConvexCone.60.20with.20.60PointedCone.60/near/581184307 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-convex-geometry maintainer-merge	15/12	Mathlib/Analysis/Convex/Cone/Extension.lean,Mathlib/Geometry/Convex/Cone/Pointed.lean	2	8	['YaelDillies', 'artie2000', 'github-actions', 'mathlib-merge-conflicts', 'ocfnash']	nobody	8-18337 8 days ago	8-17369 8 days ago	27-52687 27 days
36308	SnirBroshi author:SnirBroshi	feat(Combinatorics/SimpleGraph/Subgraph): a couple of `subgraphOfAdj` lemmas	Also golf a lemma (it's one line longer but it looks simpler to me). --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics maintainer-merge	14/5	Mathlib/Combinatorics/SimpleGraph/Subgraph.lean	1	4	['SnirBroshi', 'YaelDillies', 'github-actions']	b-mehta assignee:b-mehta	7-62884 7 days ago	46-41825 46 days ago	46-41358 46 days
37400	SnirBroshi author:SnirBroshi	feat(Combinatorics/SimpleGraph/Acyclic): endpoints of a path have at most one neighbor in the path	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics maintainer-merge	15/0	Mathlib/Combinatorics/SimpleGraph/Acyclic.lean	1	5	['Rida-Hamadani', 'Ruben-VandeVelde', 'SnirBroshi', 'github-actions']	nobody	6-57605 6 days ago	20-17652 20 days ago	22-55285 22 days
37420	artie2000 author:artie2000	refactor: change definitions to avoid `ConvexCone`	Change the definitions of `PointedCone.positive` and `PointedCone.closure` to avoid mentioning `ConvexCone`. This PR is part of a series deprecating `ConvexCone`: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Replacing.20.60ConvexCone.60.20with.20.60PointedCone.60/with/582738985 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-convex-geometry maintainer-merge	10/4	Mathlib/Analysis/Convex/Cone/Closure.lean,Mathlib/Geometry/Convex/Cone/Pointed.lean	2	3	['YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'ooovi', 'vihdzp']	nobody	6-24389 6 days ago	6-23637 6 days ago	21-42789 21 days
37393	SnirBroshi author:SnirBroshi	refactor(Algebra/Order/Monoid/Unbundled/Defs): upgrade `*ReflectLE` from `abbrev`s to `class`es	... to mitigate performance regression caused by #36629. Currently the 4 classes `{Mul/Add}{Left/Right}ReflectLE` are an `abbrev` for `ContravariantClass` so when TC-search tries to synthesize them it ends up looking through all the `ContravariantClass` instances and not just the relevant ones. --- [Zulip](https://leanprover.zulipchat.com/#narrow/channel/116290-rss/topic/Significant.20commits.20to.20mathlib4/near/582661644) [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra maintainer-merge label:t-algebra$	76/69	Mathlib/Algebra/Order/Group/Multiset.lean,Mathlib/Algebra/Order/GroupWithZero/Unbundled/Defs.lean,Mathlib/Algebra/Order/Monoid/Defs.lean,Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean,Mathlib/Algebra/Order/Monoid/Unbundled/Defs.lean,Mathlib/Algebra/Order/Monoid/Unbundled/OrderDual.lean,Mathlib/Algebra/Order/Positive/Ring.lean,Mathlib/Data/DFinsupp/Order.lean,Mathlib/Data/Finsupp/Order.lean,Mathlib/SetTheory/Ordinal/Arithmetic.lean	10	14	['JovanGerb', 'SnirBroshi', 'github-actions', 'leanprover-radar', 'vihdzp']	kim-em assignee:kim-em	5-83732 5 days ago	6-2718 6 days ago	22-26112 22 days
37864	JovanGerb author:JovanGerb	chore: reorder arguments of `AddMonoidHom.map_zsmul`	This PR modifies `AddMonoidHom.map_nsmul`, `AddMonoidHom.map_zsmul` and `AddMonoidHom.map_zsmul'` so that their order of arguments is as expected. This is then consistent with `map_nsmul`/`map_zsmul`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra maintainer-merge label:t-algebra$	21/22	Mathlib/Algebra/Category/Grp/ZModuleEquivalence.lean,Mathlib/Algebra/Group/Hom/Defs.lean,Mathlib/Algebra/GroupWithZero/Action/Defs.lean,Mathlib/Algebra/Module/CharacterModule.lean,Mathlib/Algebra/Module/Equiv/Basic.lean,Mathlib/Analysis/Complex/Circle.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean,Mathlib/CategoryTheory/Linear/Basic.lean,Mathlib/CategoryTheory/Linear/LinearFunctor.lean	9	8	['JovanGerb', 'github-actions', 'mathlib-merge-conflicts', 'themathqueen']	nobody	5-27722 5 days ago	5-30346 5 days ago	10-33669 10 days
37588	Vierkantor author:Vierkantor	feat(Linter/DocString): ignore Verso linter errors about links and LaTeX	I went through [the weekly linting log](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Weekly.20linting.20log/near/582485221) and found most of the warnings come from three sources. All of these are sensical syntax in our current Markdown dialect, and should be fixed automatically by a script, instead of manually. I expect after these changes we'll be down to hundreds of linter errors rather than two thousand. * References [between square brackets] without a following link URL. Verso has different implementations for references depending on what kind they are, and since there are a thousand references we should be using a script to fix these. * Autolinks: bare URLs or URLs between . Autolinks are intentionally not supported by Verso but replacing every `https://...` with `[https://...](https://...)` would be too noisy. * LaTeX blocks: Verso does have TeX blocks but with an incompatible syntax. Better to fix it with a script. I ended up using preprocessing in addition to postprocessing to filter out errors: using the error message we can determine whether it is a reference, but for errors caused by autolinks and LaTeX blocks I couldn't figure out how to do so easily: the information about the parse error does report a string position but this is always the last character of the docstring. So instead we modify the docstring before it is passed into Verso to get rid of the offending syntax. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-linter large-import maintainer-merge	113/5	Mathlib/Tactic/Linter/DocString.lean,MathlibTest/DocString.lean	2	18	['Vierkantor', 'github-actions', 'thorimur']	thorimur assignee:thorimur	5-20615 5 days ago	5-17005 5 days ago	8-1503 8 days
37808	JovanGerb author:JovanGerb	feat(Translate): locally modify name guessing dictionaries	This PR adds the feature to `to_dual` and `to_additive` that you can now locally modify the name translation dictionary. With this change, we run the risk of having the automated translations being harder to predict. For this reason, the changes to the dictionary do not persisted through imports. Instead, the change lasts until the end of the file (though it ignores sections). See https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Order.20dual.20tactic/near/580834166 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-meta maintainer-merge	111/39	Mathlib/Order/GaloisConnection/Basic.lean,Mathlib/Order/GaloisConnection/Defs.lean,Mathlib/Order/Interval/Set/Basic.lean,Mathlib/Order/Interval/Set/Disjoint.lean,Mathlib/Tactic/Translate/Core.lean,Mathlib/Tactic/Translate/GuessName.lean,Mathlib/Tactic/Translate/ToAdditive.lean,Mathlib/Tactic/Translate/ToDual.lean,MathlibTest/ToDual.lean	9	4	['JovanGerb', 'bryangingechen', 'github-actions', 'joneugster']	joneugster assignee:joneugster	5-20482 5 days ago	10-13121 10 days ago	10-12654 10 days
37411	vasnesterov author:vasnesterov	feat(Tactic/ComputeAsymptotics/Multiseries): introduce `Monomial`	* Introduce `Monomial` and `UnitMonomial` * Define `Monomial.toFun` and algebraic operations on monomials: negation, inversion, multiplication. --- - [x] depends on: #37414 This is a part of the `compute_asymptotics` tactic (#28291). [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-meta maintainer-merge	232/0	Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/ComputeAsymptotics/Multiseries/Monomial/Basic.lean	3	9	['github-actions', 'joneugster', 'mathlib-dependent-issues']	joneugster assignee:joneugster	5-6649 5 days ago	5-5887 5 days ago	5-11122 5 days
37418	vasnesterov author:vasnesterov	feat(Tactic/ComputeAsymptotics/Multiseries): introduce `Multiseries.Sorted`	* Introduce `Multiseries.leadingExp` - the leading exponent of a multiseries, along with a few structural lemmas. * Introduce `Multiseries.Sorted` predicate stating that exponents in a multiseries as a list are strictly decreasing. * Provide constructors (`nil`, `cons`), a coinductive principle, and basic constructions for `Sorted`. --- This is a part of the `compute_asymptotics` tactic (#28291). [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-meta maintainer-merge	201/0	Mathlib/Tactic/ComputeAsymptotics/Multiseries/Defs.lean	1	32	['github-actions', 'joneugster', 'mathlib-merge-conflicts', 'vasnesterov']	joneugster assignee:joneugster	5-6526 5 days ago	5-7255 5 days ago	21-41738 21 days
38179	wwylele author:wwylele	feat(Combinatorics): Pentagonal numbers	Introduces definition of pentagonal number https://en.wikipedia.org/wiki/Pentagonal_number in preparation for pentagonal number theorem. --- This is extracted from #33143 as suggested. I only put a few elementary properties here to limit the code change size. The future file structure will be - Combinatorics/Enumerative/Pentagonal.lean (this PR) - Topology/Algebra/InfiniteSum/Pentagonal.lean + RingTheory/PowerSeries/Pentagonal.lean (#33143, depends on previous one) pentagonal theorem in generic form and for power series - Combinatorics/Enumerative/Partition/Pentagonal.lean (future PR, depends on the previous one): connection between partition and pentagonal numbers This originally comes from my own repo https://github.com/wwylele/PentagonalNumberTheorem. In the past, there were also PR #31156 and #31362 independently worked by @BeibeiX0 on the same topic, and I tried avoiding stepping on each other's toes when making #33143. Then #31156 and #31362 were closed for unclear reason. As I mostly rewrote the code based on my own repo, I only put my name here, but given that I unavoidably took inspiration from other PRs, if @BeibeiX0 would like his name to be added to co-author and copyright notice, I am happy to do so. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics maintainer-merge	75/0	Mathlib.lean,Mathlib/Combinatorics/Enumerative/Pentagonal.lean	2	27	['copilot-pull-request-reviewer', 'github-actions', 'tb65536', 'wwylele']	nobody	4-70524 4 days ago	4-71096 4 days ago	4-76787 4 days
37931	Vierkantor author:Vierkantor	chore(Tactic): make the (deprecated) `replace` syntax a `@[tactic_alt]`	This PR replaces the tactic docstring for Mathlib's version of `replace` with a `@[tactic_alt]` attribute + `tactic_extension`. Also update the module docs which did not get updated when `replace` got upstreamed to core Lean. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	documentation t-meta maintainer-merge	7/31	Mathlib/Tactic/Replace.lean	1	2	['github-actions', 'joneugster']	dwrensha assignee:dwrensha	3-62781 3 days ago	9-11070 9 days ago	9-10603 9 days
35906	scp020 author:scp020	feat(Combinatorics/SimpleGraph/Walk): chords of walks	Define `Walk.IsChord` and `Walk.IsChordless` predicates in a new file `SimpleGraph/Walk/Chord.lean`. See "chord" in https://en.wikipedia.org/wiki/Glossary_of_graph_theory --- [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Walk.2EIsChordless.20live.20in.20mathlib.3F/with/575277309) [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics new-contributor maintainer-merge	59/0	Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Walk/Chord.lean	2	68	['SnirBroshi', 'YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'scp020']	YaelDillies assignee:YaelDillies	3-5394 3 days ago	3-4760 3 days ago	42-35916 42 days
37868	Jun2M author:Jun2M	feat(Combinatorics/Graph): map on `Graph`	This PR introduces vertex map on graphs, `map`. This creates a new file `Maps` which will be home to `map` and morphisms between `Graph`s. Co-authored-by: Peter Nelson [apn.uni@gmail.com](mailto:apn.uni@gmail.com) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics maintainer-merge	108/0	Mathlib.lean,Mathlib/Combinatorics/Graph/Maps.lean	2	8	['Jun2M', 'YaelDillies', 'b-mehta', 'github-actions', 'mathlib-merge-conflicts']	nobody	2-3332 2 days ago	2-3332 2 days ago	12-13565 12 days
37171	SnirBroshi author:SnirBroshi	chore(Data/Int/Init): generalize `le_induction` from `Prop` to `Sort*` + def lemmas	--- [Zulip 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Add.20note.20to.20help.20search.20similar.20thms/near/535331432) [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-data large-import maintainer-merge	56/48	Mathlib/Data/Int/Basic.lean,Mathlib/Data/Int/Init.lean,Mathlib/GroupTheory/CoprodI.lean	3	8	['SnirBroshi', 'github-actions', 'joneugster', 'mathlib-merge-conflicts', 'plp127']	joneugster assignee:joneugster	2-2080 2 days ago	21-48946 21 days ago	22-44713 22 days
38301	SnirBroshi author:SnirBroshi	feat(Algebra/Group/Commutator): tag `addCommutatorElement` as a scoped instance	#34784 additivized commutators and made the multiplicative commutator instance available under `open scoped commutatorElement`. This makes the additive instance available under `open scoped addCommutatorElement`. --- ~~Should we instead make it scoped under the `addCommutatorElement` namespace? The existing usages of additive commutators come from decls marked with `open scoped commutatorElement in @[to_additive]`, and `to_additive` seemingly doesn't mind that the additivized version is not an instance. So I think they don't have to live in the same namespace.~~ [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra maintainer-merge label:t-algebra$	6/0	Mathlib/Algebra/Group/Commutator.lean	1	6	['SnirBroshi', 'github-actions', 'tb65536']	nobody	2-1673 2 days ago	2-1816 2 days ago	2-1349 2 days
37941	NoahW314 author:NoahW314	feat(RingTheory/MvPolynomial/Homogeneous): add `homogeneousComponent` lemma	Add a lemma about the `support` of the `(weighted)HomogeneousComponent` of a `MvPolynomial`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-ring-theory maintainer-merge	10/0	Mathlib/RingTheory/MvPolynomial/Homogeneous.lean,Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean	2	3	['github-actions', 'mathlib-merge-conflicts', 'robin-carlier']	robin-carlier assignee:robin-carlier	1-36759 1 day ago	4-63284 4 days ago	10-48601 10 days
38172	joelriou author:joelriou	feat(AlgebraicTopology/SimplicialSet): Mulstruct.mulOne and oneMul	We introduce definitions `SSet.PtSimplex.MulStruct.oneMul/mulOne` which shall later be interpreted as an explanation for the relations satisfied by the neutral element for the multiplication on homotopy groups of Kan complexes. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebraic-topology maintainer-merge	53/0	Mathlib/AlgebraicTopology/SimplicialSet/KanComplex/MulStruct.lean	1	6	['github-actions', 'joelriou', 'robin-carlier']	robin-carlier assignee:robin-carlier	1-22284 1 day ago	1-22459 1 day ago	5-4086 5 days
34854	GrigorenkoPV author:GrigorenkoPV	chore(Combinatorics/Enumerative/Catalan): split into `Basic` & `Tree`	--- Split off from #34853 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-combinatorics maintainer-merge awaiting-author	225/194	Mathlib.lean,Mathlib/Combinatorics/Enumerative/Catalan.lean,Mathlib/Combinatorics/Enumerative/Catalan/Basic.lean,Mathlib/Combinatorics/Enumerative/Catalan/Tree.lean,Mathlib/Combinatorics/Enumerative/DyckWord.lean,Mathlib/RingTheory/PowerSeries/Catalan.lean	6	7	['SnirBroshi', 'Vierkantor', 'YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'vihdzp']	nobody	1-19558 1 day ago	10-27179 10 days ago	45-55669 45 days
36401	JovanGerb author:JovanGerb	feat(positivity): positivity extension for `a - b`	This PR adds support in `positivity` for proving things about subtraction. For example, if the goal is `0 < a - b`, and there is a local hypothesis of type `b < a`, then we close the goal. The motivation is that we want `positivity` to be a flexible tactic. So, when trying to prove `0 < a - b` using a local hypothesis, we should look for the simp normal form of this, which is `b < a`. --- [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Can.20I.20make.20positivity.20work.20for.20this.3F/near/578277240) [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-meta maintainer-merge	63/26	Mathlib/Analysis/Calculus/Taylor.lean,Mathlib/Analysis/Complex/AbelLimit.lean,Mathlib/Analysis/Complex/BorelCaratheodory.lean,Mathlib/Analysis/Complex/Hadamard.lean,Mathlib/Analysis/Convex/BetweenList.lean,Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean,Mathlib/Analysis/SpecificLimits/FloorPow.lean,Mathlib/Geometry/Manifold/Riemannian/PathELength.lean,Mathlib/Tactic/Positivity/Basic.lean,MathlibTest/positivity.lean	10	12	['JovanGerb', 'Vierkantor', 'github-actions', 'hrmacbeth', 'j-loreaux', 'joneugster', 'leanprover-radar']	joneugster assignee:joneugster	1-16823 1 day ago	1-16823 1 day ago	29-80546 29 days
38257	joelriou author:joelriou	feat(CategoryTheory): MorphismProperty.single	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-category-theory maintainer-merge	63/1	Mathlib/CategoryTheory/MorphismProperty/Basic.lean,Mathlib/CategoryTheory/MorphismProperty/IsSmall.lean,Mathlib/CategoryTheory/ObjectProperty/Local.lean	3	6	['github-actions', 'joelriou', 'robin-carlier']	nobody	1-16009 1 day ago	1-16233 1 day ago	2-84231 2 days
38083	tb65536 author:tb65536	feat(RingTheory/DiscreteValuationRing/Basic): compute the length of the quotient of a DVR	This PR computes the length of the quotient of a DVR by constructing an order isomorphism between the ideals and the order dual of `ENat`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-ring-theory t-algebra large-import maintainer-merge label:t-algebra$	55/0	Mathlib/RingTheory/DiscreteValuationRing/Basic.lean,Mathlib/RingTheory/PrincipalIdealDomain.lean	2	9	['github-actions', 'robin-carlier', 'tb65536']	robin-carlier assignee:robin-carlier	1-14947 1 day ago	1-14126 1 day ago	6-80918 6 days
38161	ADedecker author:ADedecker	fix: wrong set-builder syntax in the definition of `CompactConvergenceCLM`	See https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Simp.20failure.20due.20to.20set.20builder.20notation/near/586133497 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-topology easy maintainer-merge	1/1	Mathlib/Topology/Algebra/Module/Spaces/CompactConvergenceCLM.lean	1	3	['github-actions', 'themathqueen']	j-loreaux assignee:j-loreaux	1-9884 1 day ago	5-16996 5 days ago	5-16529 5 days
37347	JovanGerb author:JovanGerb	feat: implementation of `@[use_set_notation_for_order]`	This PR allows the use of `⊆` notation while the underlying constant is `≤`. Similarly for `⊂`/`<`, `⊇`/`≥` and `⊃`/`>`. - The idea is to later extend this feature to other set notation constants, such as union/intersection. - There are some types for which we cannot use `LE.le` as the underlying constant, such as `List` and `Multiset`. So, the elaborator for the `⊆` notation needs to make a decision which underlying constant to elaborate to, depending on the type. Sometimes the type is not known yet, which makes things awkward. Most of these cases are solved by delaying the elaboration until later when the type is known. - However, in some cases this doesn't work either, such as `simp_rw [and_comm (_ ⊆ _)]`, where it is impossible to tell the type when elaborating the term. So, some such cases need to be fixed by making it `simp_rw [and_comm (_ ≤ _)]`. This is because `simp_rw`, unlike `rw`, fully elaborates the rewrite rules before using them. So, when we get the new rewrite tactic, this problem will mostly go away. See also https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Any.20infimum.20based.20version.20of.20.60OmegaCompletePartialOrder.60.3F/near/579333629 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-meta maintainer-merge	345/0	Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/SetNotationForOrder.lean,MathlibTest/SetNotationForOrder.lean	4	48	['JovanGerb', 'Vierkantor', 'github-actions', 'thorimur']	alexjbest and thorimur assignee:alexjbest assignee:thorimur	1-1043 1 day ago	1-16676 1 day ago	23-1393 23 days
38085	dagurtomas author:dagurtomas	feat(CategoryTheory): define profunctors	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-category-theory maintainer-merge	152/0	Mathlib.lean,Mathlib/CategoryTheory/Profunctor/Basic.lean	2	15	['dagurtomas', 'github-actions', 'robin-carlier']	robin-carlier assignee:robin-carlier	0-82806 23 hours ago	0-82173 22 hours ago	6-59332 6 days
38184	tb65536 author:tb65536	chore(Algebra/Algebra/Tower): make `Algebra.algHom` an alias of `IsScalarTower.toAlgHom`	`Algebra.algHom` is a duplicate of `IsScalarTower.ofAlgHom` so I've made it an alias to make this clearer. Zulip thread: [#mathlib4 > duplication: Algebra.algHom = IsScalarTower.toAlgHom](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/duplication.3A.20Algebra.2EalgHom.20.3D.20IsScalarTower.2EtoAlgHom/with/569828872) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-ring-theory t-algebra maintainer-merge label:t-algebra$	27/26	Mathlib/Algebra/Algebra/Hom.lean,Mathlib/Algebra/Algebra/Tower.lean	2	14	['acmepjz', 'github-actions', 'tb65536', 'themathqueen']	nobody	0-75179 20 hours ago	0-74391 20 hours ago	4-67038 4 days
37291	IvanRenison author:IvanRenison	refactor(Combinatorics/SimpleGraph): move `chromaticNumber_le_two_iff_isBipartite` and `chromaticNumber_eq_two_iff` to `Bipartite` file	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics maintainer-merge	10/12	Mathlib/Combinatorics/SimpleGraph/Bipartite.lean,Mathlib/Combinatorics/SimpleGraph/Coloring/Constructions.lean	2	3	['Ruben-VandeVelde', 'github-actions', 'mathlib-merge-conflicts']	nobody	0-69412 19 hours ago	0-68750 18 hours ago	25-65538 25 days
37738	khwilson author:khwilson	feat(Topology/Order/Bornology): generalize `cobounded_eq`	`Real.cobounded_eq` and `Int.cobounded_eq` are used in several places throughout Mathlib. They are currently proved in terms of the Metric topology on `Int` and `Real`, but they're really properties of the order bornology on those objects. Generalize those constructions to `IsOrderBornology` for `LinearOrder`'s and add a few more constructions that are true in other circumstances, e.g., `cobounded NNReal = .atTop` follows from the fact that `NNReal` is both `NoMaxOrder` and `OrderBot`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge t-order	57/18	Mathlib/Analysis/Polynomial/Basic.lean,Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean,Mathlib/Topology/Instances/Int.lean,Mathlib/Topology/Instances/Real/Lemmas.lean,Mathlib/Topology/Order/Bornology.lean	5	14	['YaelDillies', 'github-actions', 'khwilson', 'vihdzp']	bryangingechen assignee:bryangingechen	0-63050 17 hours ago	14-67490 14 days ago	15-15978 15 days
38201	joelriou author:joelriou	feat(Topology): more API for ZerothHomotopy	This PR introduces a very basic API for `ZerothHomotopy`. As it was not very well typed, the generic constructor `⟦x⟧` for quotients is replaced by a specific constructor `ZerothHomotopy.mk`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-topology maintainer-merge	48/16	Mathlib/Topology/Connected/LocPathConnected.lean,Mathlib/Topology/Connected/PathConnected.lean	2	5	['SnirBroshi', 'github-actions', 'joelriou', 'robin-carlier']	nobody	0-41290 11 hours ago	0-41648 11 hours ago	3-64834 3 days
36416	j-loreaux author:j-loreaux	feat(Analysis/CStarAlgebra): norms of sums of orthogonal selfadjoint elements	--- - [ ] depends on: #36407 - [ ] depends on: #37569 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-analysis maintainer-merge awaiting-author	130/1	Mathlib/Algebra/Star/BigOperators.lean,Mathlib/Algebra/Star/SelfAdjoint.lean,Mathlib/Analysis/CStarAlgebra/Fuglede.lean,Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean	4	22	['github-actions', 'grunweg', 'j-loreaux', 'loefflerd', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'themathqueen']	loefflerd assignee:loefflerd	0-39105 10 hours ago	0-39105 10 hours ago	17-76622 17 days
37439	ADedecker author:ADedecker	feat: UniformConvergenceCLM version of ContinuousLinearEquiv.arrowCongr	The absence of `@[simp]` attribute comes from the fact that the generated lemmas would break the API boundary. I think the solution to all of this will eventually be to define generic type aliases `Topology.WithUniform` / `Topology.WithUniformOn` / `Topology.WithPointwise`... which will behave like [WithLp](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Normed/Lp/WithLp.html#WithLp) (thus disabling the very-abused defeqs around here). --- - [ ] depends on: #37614 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-topology maintainer-merge	182/3	Mathlib/Topology/Algebra/Module/Equiv.lean,Mathlib/Topology/Algebra/Module/Spaces/CompactConvergenceCLM.lean,Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean,Mathlib/Topology/Algebra/Module/Spaces/UniformConvergenceCLM.lean	4	9	['ADedecker', 'github-actions', 'loefflerd', 'mathlib-dependent-issues', 'mathlib-merge-conflicts']	loefflerd assignee:loefflerd	0-8598 2 hours ago	0-8598 2 hours ago	15-44249 15 days
38313	thorimur author:thorimur	feat: warn on deprecated declarations in `scripts/check-yaml`	This PR updates `scripts/check-yaml.lean` to warn on deprecated declarations. It also cleans up some code: `initSearchPath` does exactly what the removed code plus `CoreM.withImportModules` does (and as far as I can see we no longer need `CoreM`). Also modulizes and removes the dependence on Mathlib. --- - [x] depends on: #38312 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	CI maintainer-merge	32/26	scripts/check-yaml.lean	1	3	['github-actions', 'grunweg', 'mathlib-dependent-issues']	jcommelin assignee:jcommelin	0-7496 2 hours ago	1-74794 1 day ago	1-74758 1 day

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	518-22727 1 year ago	unknown	unknown
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	351-72404 11 months ago	unknown	unknown
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	291-52753 9 months ago	unknown	unknown
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	291-51591 9 months ago	unknown	unknown
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	231-67236 7 months ago	240-18390 240 days ago	0-16864 4 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	188-44446 6 months ago	unknown	unknown
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	160-55320 5 months ago	200-33986 200 days ago	0-29227 8 hours
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	155-72452 5 months ago	unknown	unknown
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	155-2293 5 months ago	unknown	unknown
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	154-39461 5 months ago	unknown	unknown
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	154-11327 5 months ago	unknown	unknown
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	132-79573 4 months ago	unknown	unknown
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	105-47886 3 months ago	106-8219 106 days ago	5-70690 5 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	90-10321 3 months ago	90-10321 90 days ago	40-36049 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	83-15139 2 months ago	83-15139 83 days ago	42-19879 42 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	80-27549 2 months ago	106-11681 106 days ago	0-246 4 minutes
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	71-73558 2 months ago	unknown	unknown
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	63-45897 2 months ago	91-79032 91 days ago	7-22559 7 days
20238	maemre author:maemre	feat(Computability/DFA): Closure of regular languages under some set operations	This shows that regular languages are closed under complement and intersection by constructing DFAs for them. --- Closure under all other operations will be proved when someone adds the proof for DFA<->regular expression equivalence, so they are not part of this PR. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	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	55-32695 1 month ago	unknown	unknown
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	55-32679 1 month ago	unknown	unknown
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	54-52708 1 month ago	318-82007 318 days ago	0-37135 10 hours
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 merge-conflict	23/2	Mathlib/Tactic/Linter/TextBased.lean	1	5	['github-actions', 'grunweg', 'joneugster', 'mathlib-merge-conflicts', 'vihdzp']	nobody	35-70460 1 month ago	unknown	unknown
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']	nobody	35-5455 1 month ago	121-4646 121 days ago	10-64694 10 days
36890	vihdzp author:vihdzp	chore(SetTheory): `le_mul_left` → `le_mul_of_pos_left`	The new theorem names/statements match [`Nat.le_mul_of_pos_left`](https://leanprover-community.github.io/mathlib4_docs/Init/Data/Nat/Lemmas.html#Nat.le_mul_of_pos_left). The cardinal one has also been moved to an earlier file. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-set-theory awaiting-zulip merge-conflict	28/23	Mathlib/SetTheory/Cardinal/Arithmetic.lean,Mathlib/SetTheory/Cardinal/Basic.lean,Mathlib/SetTheory/Cardinal/Free.lean,Mathlib/SetTheory/Ordinal/Arithmetic.lean,Mathlib/SetTheory/Ordinal/Exponential.lean,Mathlib/SetTheory/Ordinal/Notation.lean	6	2	['github-actions', 'mathlib-merge-conflicts']	nobody	30-42864 30 days ago	33-29604 33 days ago	0-10819 3 hours
34077	kbuzzard author:kbuzzard	perf: increase priority of instSMulOfMul	#31040 deprecated `Mul.toSMul` in place of the core instance `instSMulOfMul`, which is at a lowered priority of 910. This PR undeprecates it and makes it a higher priority instance (1100) which seems better for mathlib. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) This PR follows the philosophy seen in Mathlib's `Algebra.id : Algebra R R`, which also has raised priority. The idea is the same as `Algebra.id`: if you're looking for an instance of `Algebra R S` with R not equal to S then `Algebra.id` is extremely likely to fail quickly in practice, and if you're looking for an instance of `Algebra R R` then `Algebra.id` is unambiguously the right answer so should be tried ASAP. However the instance is defined so early in mathlib that in in practice it is tried last unless the priority is raised. The same philosophy holds here; if you're looking for an instance of `SMul X X` then you absolutely want to try `Mul.toSMul` first and if you're looking for an instance of `SMul X Y` with Y not X then `Mul.toSMul` will in practice be quick to fail. This PR was inspired by #33908 (another "this should be quick to fail and if it fits then it's almost certainly what we want" prio change) which made an instance of `IsScalarTower R A A` high priority and gave a performance boost. This PR also gives a performance boost. Note that the performance in #31040 looks very bad but the radar output is incorrect; there was a hardware change between the two runs. In fact #31040 produced no changes in profiling, as one might expect. I don't know the correct way to change the priority of a core instance in mathlib, and I didn't know if just changing the priority naively would work repo-wide rather than just file-wide, which was why this PR introduces a second instance. Zulip discussion at [#mathlib4 > priority hacks](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/priority.20hacks/with/574353616)	t-algebra awaiting-zulip label:t-algebra$	3/9	Mathlib/Algebra/Group/Action/Defs.lean,Mathlib/Algebra/Group/Action/Units.lean	2	26	['alreadydone', 'github-actions', 'kbuzzard', 'leanprover-radar', 'mathlib-merge-conflicts']	jcommelin assignee:jcommelin	26-72553 26 days ago	63-39648 63 days ago	0-51849 14 hours
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 merge-conflict	10/10	Mathlib/Control/Monad/Cont.lean,Mathlib/Control/Monad/Writer.lean	2	5	['Shreyas4991', 'eric-wieser', 'github-actions', 'mathlib-merge-conflicts']	nobody	26-53339 26 days ago	60-73857 60 days ago	0-18022 5 hours
36087	matthewjasper author:matthewjasper	chore: fix diamonds for Real/Complex Algebra instances	Unfold or make `implicit_reducible` some definitions used to define `Algebra ℝ ℂ` . This should allow reducing use of `set_option backward.isDefEq.respectTransparency false`. --- - [x] depends on: #36694 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	awaiting-zulip	24/19	Mathlib/Algebra/Algebra/Defs.lean,Mathlib/Algebra/Algebra/Pi.lean,Mathlib/Algebra/Algebra/Prod.lean,Mathlib/Analysis/Complex/Basic.lean,Mathlib/Data/Complex/Basic.lean,Mathlib/LinearAlgebra/Complex/Module.lean,MathlibTest/instance_diamonds.lean	7	8	['eric-wieser', 'github-actions', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'matthewjasper']	eric-wieser assignee:eric-wieser	23-73659 23 days ago	27-76246 27 days ago	11-73220 11 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	8	['SnirBroshi', 'TwoFX', 'eric-wieser', 'github-actions', 'linesthatinterlace', 'mathlib-merge-conflicts']	TwoFX assignee:TwoFX	8-24848 8 days ago	146-38249 146 days ago	35-75966 35 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	20	['adomani', 'eric-wieser', 'github-actions', 'grunweg', 'joneugster', 'kim-em', 'leanprover-bot', 'leanprover-radar', 'mathlib-bors', 'mathlib4-merge-conflict-bot']	grunweg assignee:grunweg	5-43563 5 days ago	236-34641 236 days ago	66-67660 66 days
37082	astrainfinita author:astrainfinita	chore(Order/CompleteLatticeIntervals): use different default values for `sSup` and `sInf`	In a subsequent PR, some assumptions will be added to `ordConnectedSubsetConditionallyCompleteLinearOrderOfBotTop`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-order awaiting-zulip	34/25	Mathlib/Order/CompleteLatticeIntervals.lean	1	5	['YaelDillies', 'astrainfinita', 'bryangingechen', 'github-actions']	bryangingechen assignee:bryangingechen	2-39945 2 days ago	2-39945 2 days ago	3-45345 3 days
34963	Parcly-Taxel author:Parcly-Taxel	feat(Archive): proof of the Robbins conjecture	Cf. [#mathlib4 > Alternative axiomatization of boolean algebras @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Alternative.20axiomatization.20of.20boolean.20algebras/near/558900960) and #31924.	t-algebra awaiting-zulip label:t-algebra$	610/0	Archive.lean,Archive/Robbins.lean	2	2	['chrisflav', 'github-actions']	chrisflav assignee:chrisflav	2-4724 2 days ago	2-4724 2 days ago	71-50046 71 days
37934	Thmoas-Guan author:Thmoas-Guan	feat(FieldTheory): definition of transcendental separable field extension	In this PR, we introduce the concept of separably generated field extension and transcendental separable field extension. Further properties will be in #37838 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra awaiting-zulip label:t-algebra$	69/0	Mathlib.lean,Mathlib/FieldTheory/TranscendentalSeparable.lean	2	3	['Thmoas-Guan', 'github-actions', 'robin-carlier']	robin-carlier assignee:robin-carlier	1-30225 1 day ago	1-31641 1 day ago	8-15071 8 days

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

There are currently no PRs on the review queue which are labelled 'tech debt' or 'longest-pole. Congratulations!