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 14, 2026 at 08:19 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	18-40991 18 days ago	18-40991 18 days ago	2-50782 2 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']	nobody	6-32707 6 days ago	6-70653 6 days ago	6-71443 6 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	6-7794 6 days ago	7-55434 7 days ago	4-49805 4 days
37544	SnirBroshi author:SnirBroshi	chore(Combinatorics/SimpleGraph/Coloring): move `ConcreteColorings.lean` and `EdgeLabeling.lean` to `Coloring/`	Moves `SimpleGraph/ConcreteColorings.lean` to `SimpleGraph/Coloring/Constructions.lean` and `SimpleGraph/EdgeLabeling.lean` to `SimpleGraph/Coloring/EdgeLabeling.lean`. See [Zulip](https://leanprover.zulipchat.com/#narrow/channel/252551-graph-theory/topic/Coloring.20module.20names/with/583281500) --- [Zulip](https://leanprover.zulipchat.com/#narrow/channel/252551-graph-theory/topic/Coloring.20module.20names/with/583281500) might want to rename `ConcreteColorings` (Edit: the poll chose `Constructions.lean`) #37546 adds module deprecations [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	file-removed t-combinatorics maintainer-merge	2/2	Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Coloring/Constructions.lean,Mathlib/Combinatorics/SimpleGraph/Coloring/EdgeLabeling.lean	3	2	['YaelDillies', 'github-actions', 'ooovi']	nobody	5-83423 5 days ago	8-63875 8 days ago	8-63966 8 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	5-64181 5 days ago	5-64439 5 days ago	7-5390 7 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/ConcreteColorings.lean	2	2	['Ruben-VandeVelde', 'github-actions']	nobody	4-45365 4 days ago	17-33173 17 days ago	17-33120 17 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	4	['Rida-Hamadani', 'Ruben-VandeVelde', 'github-actions']	nobody	4-44272 4 days ago	14-20168 14 days ago	14-20115 14 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	2	['YaelDillies', 'github-actions', 'ooovi', 'vihdzp']	nobody	4-13186 4 days ago	13-83427 13 days ago	13-83511 13 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	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	4-2209 4 days ago	4-17784 4 days ago	9-83161 9 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	4-2028 4 days ago	4-2187 4 days ago	52-29242 52 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	10	['JovanGerb', 'github-actions', 'hrmacbeth', 'j-loreaux', 'joneugster', 'leanprover-radar']	joneugster assignee:joneugster	3-77130 3 days ago	3-81043 3 days ago	21-51893 21 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	3-24075 3 days ago	3-72695 3 days ago	3-72644 3 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-5756 3 days ago	9-24173 9 days ago	34-13985 34 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	3	['YaelDillies', 'github-actions']	nobody	2-2689 2 days ago	38-5541 38 days ago	38-5488 38 days
36691	Jun2M author:Jun2M	feat(Order/Partition): every partition has `IsRepFun`	This PR expands the API for `Setoid.Partition` (or `Partition`) by introducing definitions and lemmas for working with representatives and specific parts of a partition. ### Key Additions * `Partition.rep`: Noncomputably chooses a representative from a given part of a partition, along with basic membership lemmas (`rep_mem`, `rep_mem'`). * `Partition.partOf`: Defines the part of a partition containing a specific element (evaluates to `∅` if the element is not in the underlying set). * `IsRepFun` extensions: * `exists_extend_partial` / `exists_extend_partial'`: Proves that partially defined representative functions can be extended to complete ones. * `nonempty`: Proves that every partition admits at least one representative function. Co-authored-by: Peter Nelson --- - [x] depends on: #36574 - [x] depends on: #36991 - [x] depends on: #36993 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-order maintainer-merge	111/2	Mathlib/Order/Partition/Basic.lean	1	6	['YaelDillies', 'github-actions', 'mathlib-dependent-issues', 'mathlib-merge-conflicts']	nobody	1-79297 1 day ago	3-30352 3 days ago	3-30532 3 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	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	6	['SnirBroshi', 'YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'vihdzp']	nobody	1-76514 1 day ago	1-76511 1 day ago	45-59230 45 days
37506	wwylele author:wwylele	feat(Analysis/InnerProductSpace): singleton basis for 1d space	This was brought up in #36462. Similar to existing `FiniteDimensional.basisSingleton`, this provides a OrthonormalBasis version. Also adds simp lemma for `∀ (i j : ι), P i j` for subsingleton `ι`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-analysis maintainer-merge	49/4	Mathlib/Analysis/InnerProductSpace/Orthonormal.lean,Mathlib/Analysis/InnerProductSpace/PiL2.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean,Mathlib/Combinatorics/SimpleGraph/Diam.lean,Mathlib/Logic/Basic.lean	5	36	['eric-wieser', 'github-actions', 'leanprover-radar', 'loefflerd', 'themathqueen', 'wwylele']	loefflerd assignee:loefflerd	1-67139 1 day ago	8-68177 8 days ago	12-28375 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	1-62119 1 day ago	7-3346 7 days ago	3-64638 3 days
37278	SnirBroshi author:SnirBroshi	chore(Order/Defs/Unbundled): deprecate `def Reflexive` in favor of `class Std.Refl`	Also adds definitional lemmas `std*_def` for the relation classes, and cleans up things nearby, especially in `Logic/Relation.lean`. --- [Mathlib's `def Reflexive`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Defs/Unbundled.html#Reflexive) [Core's `class Std.Refl`](https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Std.Refl) [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Relation.20properties.20duplication/near/544638270) [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-order maintainer-merge	229/171	Mathlib/Algebra/Group/Semiconj/Defs.lean,Mathlib/CategoryTheory/Abelian/Pseudoelements.lean,Mathlib/CategoryTheory/IsConnected.lean,Mathlib/Computability/Reduce.lean,Mathlib/Data/List/Pairwise.lean,Mathlib/Data/Seq/Computation.lean,Mathlib/Data/Sym/Sym2.lean,Mathlib/Data/WSeq/Relation.lean,Mathlib/GroupTheory/FreeGroup/Basic.lean,Mathlib/Logic/Pairwise.lean,Mathlib/Logic/Relation.lean,Mathlib/ModelTheory/Order.lean,Mathlib/ModelTheory/Semantics.lean,Mathlib/Order/Defs/Unbundled.lean,Mathlib/Order/Directed.lean,Mathlib/Order/Interval/Finset/Basic.lean,Mathlib/Order/Quotient.lean,Mathlib/Order/ScottContinuity.lean,Mathlib/Order/SuccPred/Relation.lean,MathlibTest/abel.lean	20	6	['Ruben-VandeVelde', 'SnirBroshi', 'github-actions', 'leanprover-radar']	bryangingechen assignee:bryangingechen	1-23303 1 day ago	1-23341 1 day ago	17-48884 17 days

All maintainer merge'd PRs

Number	Author	Title	Description	Labels	+/-	Modified files (first 100)	📝	💬	All users who commented or reviewed	Assignee(s)	Updated	Last status change	total time in review
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	18-40991 18 days ago	18-40991 18 days ago	2-50782 2 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']	nobody	6-32707 6 days ago	6-70653 6 days ago	6-71443 6 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	6-7794 6 days ago	7-55434 7 days ago	4-49805 4 days
37544	SnirBroshi author:SnirBroshi	chore(Combinatorics/SimpleGraph/Coloring): move `ConcreteColorings.lean` and `EdgeLabeling.lean` to `Coloring/`	Moves `SimpleGraph/ConcreteColorings.lean` to `SimpleGraph/Coloring/Constructions.lean` and `SimpleGraph/EdgeLabeling.lean` to `SimpleGraph/Coloring/EdgeLabeling.lean`. See [Zulip](https://leanprover.zulipchat.com/#narrow/channel/252551-graph-theory/topic/Coloring.20module.20names/with/583281500) --- [Zulip](https://leanprover.zulipchat.com/#narrow/channel/252551-graph-theory/topic/Coloring.20module.20names/with/583281500) might want to rename `ConcreteColorings` (Edit: the poll chose `Constructions.lean`) #37546 adds module deprecations [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	file-removed t-combinatorics maintainer-merge	2/2	Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Coloring/Constructions.lean,Mathlib/Combinatorics/SimpleGraph/Coloring/EdgeLabeling.lean	3	2	['YaelDillies', 'github-actions', 'ooovi']	nobody	5-83423 5 days ago	8-63875 8 days ago	8-63966 8 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	5-64181 5 days ago	5-64439 5 days ago	7-5390 7 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/ConcreteColorings.lean	2	2	['Ruben-VandeVelde', 'github-actions']	nobody	4-45365 4 days ago	17-33173 17 days ago	17-33120 17 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	4	['Rida-Hamadani', 'Ruben-VandeVelde', 'github-actions']	nobody	4-44272 4 days ago	14-20168 14 days ago	14-20115 14 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	2	['YaelDillies', 'github-actions', 'ooovi', 'vihdzp']	nobody	4-13186 4 days ago	13-83427 13 days ago	13-83511 13 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	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	4-2209 4 days ago	4-17784 4 days ago	9-83161 9 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	4-2028 4 days ago	4-2187 4 days ago	52-29242 52 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	10	['JovanGerb', 'github-actions', 'hrmacbeth', 'j-loreaux', 'joneugster', 'leanprover-radar']	joneugster assignee:joneugster	3-77130 3 days ago	3-81043 3 days ago	21-51893 21 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	3-24075 3 days ago	3-72695 3 days ago	3-72644 3 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-5756 3 days ago	9-24173 9 days ago	34-13985 34 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	3	['YaelDillies', 'github-actions']	nobody	2-2689 2 days ago	38-5541 38 days ago	38-5488 38 days
36691	Jun2M author:Jun2M	feat(Order/Partition): every partition has `IsRepFun`	This PR expands the API for `Setoid.Partition` (or `Partition`) by introducing definitions and lemmas for working with representatives and specific parts of a partition. ### Key Additions * `Partition.rep`: Noncomputably chooses a representative from a given part of a partition, along with basic membership lemmas (`rep_mem`, `rep_mem'`). * `Partition.partOf`: Defines the part of a partition containing a specific element (evaluates to `∅` if the element is not in the underlying set). * `IsRepFun` extensions: * `exists_extend_partial` / `exists_extend_partial'`: Proves that partially defined representative functions can be extended to complete ones. * `nonempty`: Proves that every partition admits at least one representative function. Co-authored-by: Peter Nelson --- - [x] depends on: #36574 - [x] depends on: #36991 - [x] depends on: #36993 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-order maintainer-merge	111/2	Mathlib/Order/Partition/Basic.lean	1	6	['YaelDillies', 'github-actions', 'mathlib-dependent-issues', 'mathlib-merge-conflicts']	nobody	1-79297 1 day ago	3-30352 3 days ago	3-30532 3 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	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	6	['SnirBroshi', 'YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'vihdzp']	nobody	1-76514 1 day ago	1-76511 1 day ago	45-59230 45 days
37506	wwylele author:wwylele	feat(Analysis/InnerProductSpace): singleton basis for 1d space	This was brought up in #36462. Similar to existing `FiniteDimensional.basisSingleton`, this provides a OrthonormalBasis version. Also adds simp lemma for `∀ (i j : ι), P i j` for subsingleton `ι`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-analysis maintainer-merge	49/4	Mathlib/Analysis/InnerProductSpace/Orthonormal.lean,Mathlib/Analysis/InnerProductSpace/PiL2.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean,Mathlib/Combinatorics/SimpleGraph/Diam.lean,Mathlib/Logic/Basic.lean	5	36	['eric-wieser', 'github-actions', 'leanprover-radar', 'loefflerd', 'themathqueen', 'wwylele']	loefflerd assignee:loefflerd	1-67139 1 day ago	8-68177 8 days ago	12-28375 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	1-62119 1 day ago	7-3346 7 days ago	3-64638 3 days
37278	SnirBroshi author:SnirBroshi	chore(Order/Defs/Unbundled): deprecate `def Reflexive` in favor of `class Std.Refl`	Also adds definitional lemmas `std*_def` for the relation classes, and cleans up things nearby, especially in `Logic/Relation.lean`. --- [Mathlib's `def Reflexive`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Order/Defs/Unbundled.html#Reflexive) [Core's `class Std.Refl`](https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Std.Refl) [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Relation.20properties.20duplication/near/544638270) [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-order maintainer-merge	229/171	Mathlib/Algebra/Group/Semiconj/Defs.lean,Mathlib/CategoryTheory/Abelian/Pseudoelements.lean,Mathlib/CategoryTheory/IsConnected.lean,Mathlib/Computability/Reduce.lean,Mathlib/Data/List/Pairwise.lean,Mathlib/Data/Seq/Computation.lean,Mathlib/Data/Sym/Sym2.lean,Mathlib/Data/WSeq/Relation.lean,Mathlib/GroupTheory/FreeGroup/Basic.lean,Mathlib/Logic/Pairwise.lean,Mathlib/Logic/Relation.lean,Mathlib/ModelTheory/Order.lean,Mathlib/ModelTheory/Semantics.lean,Mathlib/Order/Defs/Unbundled.lean,Mathlib/Order/Directed.lean,Mathlib/Order/Interval/Finset/Basic.lean,Mathlib/Order/Quotient.lean,Mathlib/Order/ScottContinuity.lean,Mathlib/Order/SuccPred/Relation.lean,MathlibTest/abel.lean	20	6	['Ruben-VandeVelde', 'SnirBroshi', 'github-actions', 'leanprover-radar']	bryangingechen assignee:bryangingechen	1-23303 1 day ago	1-23341 1 day ago	17-48884 17 days
37678	vihdzp author:vihdzp	chore(Dynamics/FixedPoints/Defs): create `Defs` file	--- I got a large import warning on another PR for simply importing the definition `Function.fixedPoints`, which I found rather silly. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-dynamics tech debt maintainer-merge	67/44	Mathlib.lean,Mathlib/Dynamics/FixedPoints/Basic.lean,Mathlib/Dynamics/FixedPoints/Defs.lean,Mathlib/Logic/Function/Defs.lean	4	2	['Ruben-VandeVelde', 'github-actions']	urkud assignee:urkud	0-84226 23 hours ago	8-34514 8 days ago	8-35039 8 days
36965	vihdzp author:vihdzp	chore(SetTheory/Cardinal): tweak `succ` lemmas	We leave the `SuccOrder` instance unexposed. It doesn't have any particularly good def-eqs, it's simply defined as the infimum of all larger cardinals. We also golf some surrounding theorems. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-set-theory maintainer-merge	54/61	Mathlib/LinearAlgebra/Dimension/Basic.lean,Mathlib/Order/SuccPred/CompleteLinearOrder.lean,Mathlib/SetTheory/Cardinal/Basic.lean,Mathlib/SetTheory/Cardinal/Order.lean,Mathlib/SetTheory/Ordinal/Basic.lean	5	4	['YaelDillies', 'github-actions', 'mathlib-merge-conflicts']	b-mehta assignee:b-mehta	0-80276 22 hours ago	1-11733 1 day ago	23-5890 23 days
37138	dtumad author:dtumad	feat(Data/FinEnum): instances for standard signed and unsigned integer types	Adds `FinEnum` instances for `UIntN`/`IntN` for various `N`, and for platform sized integers. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-data new-contributor maintainer-merge	45/0	Mathlib/Data/FinEnum.lean	1	11	['dtumad', 'github-actions', 'joneugster', 'linesthatinterlace']	joneugster assignee:joneugster	0-78648 21 hours ago	13-60433 13 days ago	18-10213 18 days
37645	joelriou author:joelriou	feat(CategoryTheory/Limits): `sigmaConst` preserves colimits	More precisely `sigmaConst.obj R` commutes with colimits. We also compute the cokernel of `(sigmaConst.obj R).map f` when `f` is a map in `Type*`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-category-theory maintainer-merge	144/48	Mathlib.lean,Mathlib/Algebra/Category/ModuleCat/Sheaf/Free.lean,Mathlib/CategoryTheory/Limits/Preserves/SigmaConst.lean	3	7	['dagurtomas', 'github-actions', 'joelriou', 'robin-carlier']	robin-carlier assignee:robin-carlier	0-78086 21 hours ago	0-78135 21 hours ago	8-77306 8 days
34477	spanning-tree author:spanning-tree	refactor(Order): make CompletePartialOrder extend OrderBot	Make `CompletePartialOrder` extend `OrderBot`, and add a constructor `completePartialOrderOfLubOfDirected`. Previously, `CompletePartialOrder` had an implicit bottom element but did not extend OrderBot explicitly. Breaking change: `CompletePartialOrder` instances must provide `⊥` and `bot_le`, or use the constructor. See discussion in [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.3E.20complete.20partial.20order.20and.20domain.20theory.20formalization). --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-order new-contributor maintainer-merge	16/1	Mathlib/Order/CompletePartialOrder.lean	1	6	['Citronhat', 'YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'vihdzp']	bryangingechen assignee:bryangingechen	0-77013 21 hours ago	3-28344 3 days ago	61-616 61 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	0-64418 17 hours ago	0-64479 17 hours ago	52-44726 52 days
38006	yuanyi-350 author:yuanyi-350	chore(Analysis): golf Basic, Exponential, and ContinuousFunctionalCalculus/Unique	Split from #37987 at reviewer request. This PR contains only the golf changes to: - `Mathlib/Analysis/CStarAlgebra/Basic.lean` - `Mathlib/Analysis/CStarAlgebra/Exponential.lean` - `Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean` Requested in: https://github.com/leanprover-community/mathlib4/pull/37987#discussion_r3073812894	t-analysis maintainer-merge	12/50	Mathlib/Analysis/CStarAlgebra/Basic.lean,Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean,Mathlib/Analysis/CStarAlgebra/Exponential.lean	3	7	['github-actions', 'leanprover-radar', 'themathqueen', 'yuanyi-350']	nobody	0-58451 16 hours ago	0-60020 16 hours ago	0-61135 16 hours
33935	mckoen author:mckoen	feat(CategoryTheory/Monoidal/Arrow): define monoidal structure on arrow category	defines a monoidal category structure on the arrow category of a cartesian closed category. --- - [x] depends on: #33974 - [x] depends on: #34887 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-category-theory maintainer-merge	659/0	Mathlib.lean,Mathlib/CategoryTheory/Monoidal/Arrow.lean,Mathlib/CategoryTheory/Monoidal/Closed/Braided.lean,Mathlib/CategoryTheory/Monoidal/Limits/HasLimits.lean,Mathlib/CategoryTheory/Monoidal/Limits/Shapes/Pullback.lean,Mathlib/CategoryTheory/Monoidal/PushoutProduct.lean	6	42	['dagurtomas', 'github-actions', 'joelriou', 'mathlib-dependent-issues', 'mckoen']	joelriou assignee:joelriou	0-42425 11 hours ago	0-42480 11 hours ago	33-84812 33 days
37937	grunweg author:grunweg	chore: avoid superfluous use of push_neg with contrapose, by_contra o…	…r by_cases Found by the linter in #37907. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge	354/354	Archive/Imo/Imo1988Q6.lean,Archive/Imo/Imo2008Q2.lean,Archive/MiuLanguage/DecisionNec.lean,Archive/Sensitivity.lean,Archive/Wiedijk100Theorems/PerfectNumbers.lean,Archive/Wiedijk100Theorems/SolutionOfCubicQuartic.lean,Mathlib/Algebra/Algebra/Spectrum/Basic.lean,Mathlib/Algebra/GCDMonoid/Basic.lean,Mathlib/Algebra/Group/Irreducible/Indecomposable.lean,Mathlib/Algebra/Group/UniqueProds/Basic.lean,Mathlib/Algebra/GroupWithZero/Associated.lean,Mathlib/Algebra/Lie/Semisimple/Basic.lean,Mathlib/Algebra/Lie/Sl2.lean,Mathlib/Algebra/Lie/Weights/Basic.lean,Mathlib/Algebra/Lie/Weights/Killing.lean,Mathlib/Algebra/Module/Submodule/Union.lean,Mathlib/Algebra/Module/ZLattice/Basic.lean,Mathlib/Algebra/MvPolynomial/Eval.lean,Mathlib/Algebra/MvPolynomial/NoZeroDivisors.lean,Mathlib/Algebra/Order/Archimedean/Hom.lean,Mathlib/Algebra/Order/Module/HahnEmbedding.lean,Mathlib/Algebra/Polynomial/CancelLeads.lean,Mathlib/Algebra/Polynomial/Coeff.lean,Mathlib/Algebra/Polynomial/Derivative.lean,Mathlib/Algebra/Polynomial/Div.lean,Mathlib/Algebra/Polynomial/Eval/Coeff.lean,Mathlib/Algebra/Polynomial/FieldDivision.lean,Mathlib/Algebra/Polynomial/Monic.lean,Mathlib/Algebra/Polynomial/OfFn.lean,Mathlib/Algebra/Tropical/Lattice.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Formula.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Formula.lean,Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean,Mathlib/Analysis/Analytic/IsolatedZeros.lean,Mathlib/Analysis/Analytic/Order.lean,Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean,Mathlib/Analysis/Calculus/FDeriv/Add.lean,Mathlib/Analysis/Calculus/FDeriv/Analytic.lean,Mathlib/Analysis/Calculus/FDeriv/Const.lean,Mathlib/Analysis/Calculus/LagrangeMultipliers.lean,Mathlib/Analysis/Calculus/Rademacher.lean,Mathlib/Analysis/Calculus/TangentCone/Basic.lean,Mathlib/Analysis/Calculus/TangentCone/ProperSpace.lean,Mathlib/Analysis/Complex/Conformal.lean,Mathlib/Analysis/Complex/UpperHalfPlane/MoebiusAction.lean,Mathlib/Analysis/Convex/Between.lean,Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean,Mathlib/Analysis/Convex/Star.lean,Mathlib/Analysis/Convolution.lean,Mathlib/Analysis/Distribution/AEEqOfIntegralContDiff.lean,Mathlib/Analysis/Fourier/AddCircle.lean,Mathlib/Analysis/Fourier/AddCircleMulti.lean,Mathlib/Analysis/Matrix/Order.lean,Mathlib/Analysis/Matrix/Spectrum.lean,Mathlib/Analysis/Meromorphic/Order.lean,Mathlib/Analysis/Normed/Group/AddCircle.lean,Mathlib/Analysis/SpecialFunctions/Complex/Arctan.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean,Mathlib/Analysis/SpecialFunctions/Gamma/Deriv.lean,Mathlib/Analysis/SpecialFunctions/Integrals/Basic.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/ChebyshevGauss.lean,Mathlib/CategoryTheory/Filtered/Basic.lean,Mathlib/Combinatorics/Enumerative/DyckWord.lean,Mathlib/Combinatorics/Enumerative/InclusionExclusion.lean,Mathlib/Combinatorics/Enumerative/Partition/GenFun.lean,Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean,Mathlib/Combinatorics/SimpleGraph/CompleteMultipartite.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean,Mathlib/Combinatorics/SimpleGraph/Diam.lean,Mathlib/Combinatorics/SimpleGraph/Extremal/Basic.lean,Mathlib/Combinatorics/SimpleGraph/Extremal/Turan.lean,Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean,Mathlib/Combinatorics/SimpleGraph/Operations.lean,Mathlib/Combinatorics/SimpleGraph/Subgraph.lean,Mathlib/Combinatorics/SimpleGraph/Walk/Maps.lean,Mathlib/Data/Finset/Insert.lean,Mathlib/Data/Finsupp/Fin.lean,Mathlib/Data/Finsupp/Option.lean,Mathlib/Data/List/Basic.lean,Mathlib/Data/NNReal/Defs.lean,Mathlib/Data/Nat/Count.lean,Mathlib/Data/Nat/Digits/Defs.lean,Mathlib/Data/Nat/Factorization/Basic.lean,Mathlib/Data/Nat/Factorization/LCM.lean,Mathlib/Data/Set/Finite/Basic.lean,Mathlib/Data/Sym/Sym2.lean,Mathlib/FieldTheory/CardinalEmb.lean,Mathlib/FieldTheory/Finite/Basic.lean,Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean,Mathlib/FieldTheory/Minpoly/Field.lean,Mathlib/FieldTheory/PurelyInseparable/Tower.lean,Mathlib/FieldTheory/SeparablyGenerated.lean,Mathlib/Geometry/Euclidean/Angle/Unoriented/TriangleInequality.lean,Mathlib/Geometry/Group/Growth/LinearLowerBound.lean,Mathlib/Geometry/Manifold/ContMDiff/Basic.lean,Mathlib/Geometry/Manifold/MFDeriv/Basic.lean,Mathlib/Geometry/Manifold/PartitionOfUnity.lean,Mathlib/GroupTheory/Coxeter/Inversion.lean,Mathlib/GroupTheory/Coxeter/Length.lean	252	8	['JovanGerb', 'github-actions', 'grunweg', 'leanprover-radar', 'wwylele']	nobody	0-38624 10 hours ago	2-55408 2 days ago	2-55362 2 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 merge-conflict	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	0-35830 9 hours ago	0-35831 9 hours ago	19-41437 19 days
37874	yuanyi-350 author:yuanyi-350	refactor(Analysis/PSeries): simplify `Real.summable_one_div_nat_add_rpow` via asymptotics	## Summary - replace the manual eventual-positivity and limit argument in `Real.summable_one_div_nat_add_rpow` with an asymptotic-equivalence proof - use `IsEquivalent.add_const_of_norm_tendsto_atTop` together with `Asymptotics.IsEquivalent.summable_iff_nat` - add the imports needed for the asymptotics-based proof This also removes the local `set_option linter.unusedSimpArgs false` workaround from the proof.	t-analysis large-import maintainer-merge awaiting-author	14/26	Mathlib/Analysis/PSeries.lean,Mathlib/NumberTheory/LSeries/Nonvanishing.lean	2	11	['YaelDillies', 'github-actions', 'grunweg', 'leanprover-radar', 'yuanyi-350']	ADedecker assignee:ADedecker	0-29619 8 hours ago	0-54470 15 hours ago	3-40896 3 days
36958	JovanGerb author:JovanGerb	chore(Topology/Order/Basic): use `Preorder.topology` in `OrderTopology`	This PR addresses the comment: ``` TODO: define `Preorder.topology` before `OrderTopology` and reuse the def ``` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-topology maintainer-merge	22/19	Mathlib/Topology/Instances/Discrete.lean,Mathlib/Topology/Order/Basic.lean	2	4	['JovanGerb', 'github-actions', 'vihdzp']	nobody	0-26337 7 hours ago	23-18474 23 days ago	23-18756 23 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	43	['JovanGerb', 'github-actions', 'thorimur']	alexjbest and thorimur assignee:alexjbest assignee:thorimur	0-18362 5 hours ago	1-31741 1 day ago	14-59175 14 days
34649	peabrainiac author:peabrainiac	feat(Analysis/Calculus/ContDiff): add notation `ℕ∞ω` for `WithTop ℕ∞`	Add a `ContDiff`-scoped notation `ℕ∞ω` for `WithTop ℕ∞`, accompanying the existing notations `∞` and `ω` for `(⊤ : ℕ∞) : ℕ∞ω` and `⊤ : ℕ∞ω`. --- [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/RFC.3A.20notation.20for.20.60WithTop.20.E2.84.95.E2.88.9E.60/near/573917824) I've also replaced `WithTop ℕ∞` with this new notation already in the files that mention it the most, but not in all files yet; many mention `WithTop ℕ∞` just a couple of times but don't open the `ContDiff` namespace. I'm not sure whether that should be taken as a sign to not make the notation scoped, or whether the solution is just to `open scoped ContDiff` in these files or not use the notation there. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-differential-geometry t-analysis maintainer-merge	276/272	Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean,Mathlib/Analysis/Calculus/ContDiff/Basic.lean,Mathlib/Analysis/Calculus/ContDiff/Bounds.lean,Mathlib/Analysis/Calculus/ContDiff/CPolynomial.lean,Mathlib/Analysis/Calculus/ContDiff/Comp.lean,Mathlib/Analysis/Calculus/ContDiff/Defs.lean,Mathlib/Analysis/Calculus/ContDiff/Deriv.lean,Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean,Mathlib/Analysis/Calculus/ContDiff/Operations.lean,Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean,Mathlib/Analysis/Calculus/ImplicitContDiff.lean,Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean,Mathlib/Analysis/Calculus/IteratedDeriv/FaaDiBruno.lean,Mathlib/Analysis/Calculus/VectorField.lean,Mathlib/Analysis/Complex/UpperHalfPlane/Manifold.lean,Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean,Mathlib/Analysis/Distribution/TestFunction.lean,Mathlib/Analysis/Fourier/FourierTransformDeriv.lean,Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean,Mathlib/Analysis/SpecialFunctions/Trigonometric/InverseDeriv.lean,Mathlib/Geometry/Manifold/Algebra/LeftInvariantDerivation.lean,Mathlib/Geometry/Manifold/Algebra/LieGroup.lean,Mathlib/Geometry/Manifold/Algebra/Monoid.lean,Mathlib/Geometry/Manifold/Algebra/SmoothFunctions.lean,Mathlib/Geometry/Manifold/Algebra/Structures.lean,Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean,Mathlib/Geometry/Manifold/ContMDiff/Basic.lean,Mathlib/Geometry/Manifold/ContMDiff/Defs.lean,Mathlib/Geometry/Manifold/Diffeomorph.lean,Mathlib/Geometry/Manifold/Immersion.lean,Mathlib/Geometry/Manifold/Instances/Real.lean,Mathlib/Geometry/Manifold/Instances/Sphere.lean,Mathlib/Geometry/Manifold/Instances/UnitsOfNormedAlgebra.lean,Mathlib/Geometry/Manifold/IsManifold/Basic.lean,Mathlib/Geometry/Manifold/LocalSourceTargetProperty.lean,Mathlib/Geometry/Manifold/Riemannian/Basic.lean,Mathlib/Geometry/Manifold/Riemannian/PathELength.lean,Mathlib/Geometry/Manifold/SmoothEmbedding.lean,Mathlib/Geometry/Manifold/VectorBundle/Basic.lean,Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/Basic.lean,Mathlib/Geometry/Manifold/VectorBundle/FiberwiseLinear.lean,Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean,Mathlib/Geometry/Manifold/VectorBundle/Riemannian.lean,Mathlib/Geometry/Manifold/VectorBundle/SmoothSection.lean,Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean,Mathlib/Geometry/Manifold/VectorField/LieBracket.lean,Mathlib/Geometry/Manifold/VectorField/Pullback.lean	47	12	['JovanGerb', 'github-actions', 'j-loreaux', 'mathlib-merge-conflicts', 'peabrainiac']	sgouezel assignee:sgouezel	0-18322 5 hours ago	0-18347 5 hours ago	11-81155 11 days
37999	grunweg author:grunweg	chore(AtLocation): clean up backtick handling	Make errors in AtLocation surround the tactic name with backticks by default. This fixes a few error messages to comply with mathlib's style guide. Extracted from #37899. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-meta easy maintainer-merge	19/20	Mathlib/Tactic/Abel.lean,Mathlib/Tactic/FieldSimp.lean,Mathlib/Tactic/Push.lean,Mathlib/Tactic/Ring/RingNF.lean,Mathlib/Util/AtLocation.lean,MathlibTest/abel.lean,MathlibTest/push_neg.lean,MathlibTest/ring.lean	8	7	['github-actions', 'thorimur']	nobody	0-17454 4 hours ago	0-62094 17 hours ago	0-62043 17 hours
31425	robertmaxton42 author:robertmaxton42	feat(Topology): implement delaborators for non-standard topology notation	Add delaborators for unary and binary notation related to non-standard topologies in the TopologicalSpace namespace. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-topology maintainer-merge	265/5	Mathlib.lean,Mathlib/Topology/Defs/Basic.lean,Mathlib/Util/DelabNonCanonical.lean,MathlibTest/Delab/TopologicalSpace.lean	4	52	['eric-wieser', 'github-actions', 'j-loreaux', 'jcommelin', 'kckennylau', 'robertmaxton42']	alreadydone assignee:alreadydone	0-12616 3 hours ago	0-12676 3 hours ago	124-9985 124 days
37785	yuanyi-350 author:yuanyi-350	chore: golf proofs in `FDeriv/Symmetric`	This PR shortens two proofs by using existing lemmas and more standard constructions. * In `Analysis/Calculus/FDeriv/Symmetric`, it replaces a manual construction of the restricted second derivative with `bilinearRestrictScalars`, and streamlines the `ContDiffWithinAt.isSymmSndFDerivWithinAt` argument by passing through the corresponding `ContDiffAt` result. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge	15/63	Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean,Mathlib/Analysis/Calculus/FDeriv/Symmetric.lean	2	25	['github-actions', 'grunweg', 'leanprover-radar', 'loefflerd', 'mathlib-bors', 'tb65536', 'yuanyi-350']	nobody	0-8447 2 hours ago	3-69036 3 days ago	6-17217 6 days

PRs blocked on a zulip discussion

Number	Author	Title	Description	Labels	+/-	Modified files (first 100)	📝	💬	All users who commented or reviewed	Assignee(s)	Updated	Last status change	total time in review
17623	astrainfinita author:astrainfinita	feat(Algebra/Order/GroupWithZero/Unbundled): add some lemmas	Some lemmas in `Algebra.Order.GroupWithZero.Unbundled` have incorrect or unsatisfactory names, or assumptions that can be omitted using `ZeroLEOneClass`. The lemmas added in this PR are versions of existing lemmas that use the correct or better name or `ZeroLEOneClass` to omit an assumption. The original lemmas will be deprecated in #17593. \| New name \| Old name \| \|-------------------------\|-------------------------\| \| `mul_le_one_left₀` \| `Left.mul_le_one_of_le_of_le` \| \| `mul_lt_one_of_le_of_lt_left₀` (`0 ≤ ·` version) / `mul_lt_one_of_le_of_lt_of_pos_left` \| `Left.mul_lt_of_le_of_lt_one_of_pos` \| \| `mul_lt_one_of_lt_of_le_left₀` \| `Left.mul_lt_of_lt_of_le_one_of_nonneg` \| \| `mul_le_one_right₀` \| `Right.mul_le_one_of_le_of_le` \| \| `mul_lt_one_of_lt_of_le_right₀` (`0 ≤ ·` version) / `mul_lt_one_of_lt_of_le_of_pos_right` \| `Right.mul_lt_one_of_lt_of_le_of_pos` \| \| `mul_lt_one_of_le_of_lt_right₀` \| `Right.mul_lt_one_of_le_of_lt_of_nonneg` \| The following lemmas use `ZeroLEOneClass`. \| New name \| Old name \| \|-------------------------\|-------------------------\| \| `(Left.)one_le_mul₀` \| `Left.one_le_mul_of_le_of_le` \| \| `Left.one_lt_mul_of_le_of_lt₀` \| `Left.one_lt_mul_of_le_of_lt_of_pos` \| \| `Left.one_lt_mul_of_lt_of_le₀` \| `Left.lt_mul_of_lt_of_one_le_of_nonneg` / `one_lt_mul_of_lt_of_le` (still there) \| \| `(Left.)one_lt_mul₀` \| \| \| `Right.one_le_mul₀` \| `Right.one_le_mul_of_le_of_le` \| \| `Right.one_lt_mul_of_lt_of_le₀` \| `Right.one_lt_mul_of_lt_of_le_of_pos` \| \| `Right.one_lt_mul_of_le_of_lt₀` \| `Right.one_lt_mul_of_le_of_lt_of_nonneg` / `one_lt_mul_of_le_of_lt` (still there) / `one_lt_mul` (still there) \| \| `Right.one_lt_mul₀` \| `Right.one_lt_mul_of_lt_of_lt` \| --- Split from #17593. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	merge-conflict t-algebra awaiting-zulip t-order label:t-algebra$	146/44	Mathlib/Algebra/Order/GroupWithZero/Canonical.lean,Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean	2	11	['YaelDillies', 'astrainfinita', 'github-actions', 'j-loreaux']	nobody	509-72126 1 year ago	516-64685 516 days ago	33-53295 33 days
15654	TpmKranz author:TpmKranz	feat(Computability): language-preserving maps between NFA and RE	Map REs to NFAs via Thompson's construction and NFAs to REs using GNFAs Last chunk of #12648 --- - [ ] depends on: #15651 - [ ] depends on: #15649 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	blocked-by-other-PR new-contributor t-computability merge-conflict awaiting-zulip	985/2	Mathlib.lean,Mathlib/Computability/GNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean,Mathlib/Computability/RegularExpressions.lean,Mathlib/Data/FinEnum/Option.lean,docs/references.bib	7	3	['github-actions', 'leanprover-community-mathlib4-bot', 'meithecatte']	nobody	343-35403 11 months ago	612-58588 612 days ago	0-179 2 minutes
17458	urkud author:urkud	refactor(Algebra/Group): make `IsUnit` a typeclass	Also change some lemmas to assume `[IsUnit _]` instead of `[Invertible _]`. Motivated by potential non-defeq diamonds in #14986, see also [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Invertible.20and.20data) I no longer plan to merge this PR, but I'm going to cherry-pick some changes to a new PR before closing this one. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	merge-conflict t-algebra awaiting-zulip label:t-algebra$	82/72	Mathlib/Algebra/CharP/Invertible.lean,Mathlib/Algebra/Group/Invertible/Basic.lean,Mathlib/Algebra/Group/Units/Defs.lean,Mathlib/Algebra/GroupWithZero/Invertible.lean,Mathlib/Algebra/GroupWithZero/Units/Basic.lean,Mathlib/Algebra/Polynomial/Degree/Units.lean,Mathlib/Algebra/Polynomial/Splits.lean,Mathlib/Analysis/Convex/Segment.lean,Mathlib/Analysis/Normed/Affine/Isometry.lean,Mathlib/Analysis/Normed/Ring/Units.lean,Mathlib/CategoryTheory/Linear/Basic.lean,Mathlib/FieldTheory/Finite/Basic.lean,Mathlib/FieldTheory/Separable.lean,Mathlib/FieldTheory/SeparableDegree.lean,Mathlib/GroupTheory/Submonoid/Inverses.lean,Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean,Mathlib/LinearAlgebra/AffineSpace/Combination.lean,Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean,Mathlib/LinearAlgebra/CliffordAlgebra/Inversion.lean,Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean,Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean,Mathlib/NumberTheory/MulChar/Basic.lean,Mathlib/RingTheory/Localization/NumDen.lean,Mathlib/RingTheory/Polynomial/Content.lean,Mathlib/RingTheory/Polynomial/GaussLemma.lean,Mathlib/RingTheory/Valuation/Basic.lean	26	12	['MichaelStollBayreuth', 'acmepjz', 'eric-wieser', 'github-actions', 'leanprover-bot', 'leanprover-community-bot-assistant', 'urkud']	nobody	283-15752 9 months ago	554-49795 554 days ago	0-66650 18 hours
25218	kckennylau author:kckennylau	feat(AlgebraicGeometry): Tate normal form of elliptic curves	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	merge-conflict t-algebraic-geometry awaiting-zulip new-contributor	291/26	Mathlib.lean,Mathlib/AlgebraicGeometry/EllipticCurve/IsomOfJ.lean,Mathlib/AlgebraicGeometry/EllipticCurve/Modular/TateNormalForm.lean,Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean,Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean	5	31	['MichaelStollBayreuth', 'Multramate', 'acmepjz', 'github-actions', 'grunweg', 'kckennylau', 'leanprover-community-bot-assistant']	nobody	283-14590 9 months ago	315-76107 315 days ago	6-44784 6 days
28803	astrainfinita author:astrainfinita	refactor: unbundle algebra from `ENormed*`	Further speed up the search in the algebraic typeclass hierarchy by avoiding searching for `TopologicalSpace`. This PR continues the work from #23961. - Change `ESeminormed(Add)Monoid` and `ENormed(Add)Monoid` so they no longer carry algebraic data. - Deprecate `ESeminormed(Add)CommMonoid` and `ENormed(Add)CommMonoid` in favor of `ESeminormed(Add)Monoid` and `ENormed(Add)Monoid` with a commutative algebraic typeclass. \|Old\|New\| \|---\|---\| \| `[ESeminormed(Add)(Comm)Monoid E]` \| `[(Add)(Comm)Monoid E] [ESeminormed(Add)Monoid E]` \| \| `[ENormed(Add)(Comm)Monoid]` \| `[(Add)(Comm)Monoid E] [ENormed(Add)Monoid]` \| See [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2328803.20refactor.3A.20unbundle.20algebra.20from.20.60ENormed*.60/with/536024350) ------------ - [x] depends on: #28813	t-algebra merge-conflict slow-typeclass-synthesis awaiting-zulip t-analysis label:t-algebra$	80/63	Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean,Mathlib/Analysis/Normed/Group/Basic.lean,Mathlib/Analysis/Normed/Group/Continuity.lean,Mathlib/Analysis/Normed/Group/InfiniteSum.lean,Mathlib/Analysis/NormedSpace/IndicatorFunction.lean,Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean,Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean,Mathlib/MeasureTheory/Function/L1Space/Integrable.lean,Mathlib/MeasureTheory/Function/LocallyIntegrable.lean,Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean,Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean,Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean,Mathlib/MeasureTheory/Integral/IntegrableOn.lean,Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean	14	28	['astrainfinita', 'bryangingechen', 'github-actions', 'grunweg', 'kbuzzard', 'leanprover-bot', 'leanprover-community-mathlib4-bot', 'mathlib-bors', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'sgouezel']	grunweg assignee:grunweg	223-30235 7 months ago	231-67789 231 days ago	0-19882 5 hours
28925	grunweg author:grunweg	chore: remove `linear_combination'` tactic	When `linear_combination` was refactored in #15899, the old code was kept as the `linear_combination'` tactic, for easier migration. The consensus of the zulip discussion ([#mathlib4 > Narrowing the scope of `linear_combination` @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Narrowing.20the.20scope.20of.20.60linear_combination.60/near/470237816)) was to wait, and "revisit this once people have experienced the various tactics in practice". One year later, the old tactic has almost no uses: it is unused in mathlib; [searching on github](https://github.com/search?q=linear_combination%27%20path%3A*.lean&type=code) yields 37 hits --- all of which are in various forks of mathlib. Thus, removing this tactic seems appropriate. --- Do not merge before the zulip discussion has concluded! [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	merge-conflict file-removed awaiting-zulip	0/564	Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/LinearCombination'.lean,Mathlib/Tactic/Linter/UnusedTactic.lean,MathlibTest/linear_combination'.lean	5	4	['euprunin', 'github-actions', 'grunweg', 'mathlib4-merge-conflict-bot']	nobody	180-7445 5 months ago	231-39242 231 days ago	0-1 1 second
30150	imbrem author:imbrem	feat(CategoryTheory/Monoidal): to_additive for MonoidalCategory	Add `AddMonoidalCategory`, the additive version of `MonoidalCategory`. To get this to work, I needed to _remove_ the `to_additive` attributes in `Discrete.lean`, since existing code relies on the `AddMonoid M → MonoidalCategory M` instance. For now, we simply implement the additive variants by hand instead. --- As discussed in #28718; I added an `AddMonoidalCategory` struct and tagged `MonoidalCategory` with `to_additive`, along with the lemmas in `Category.lean`. I think this is the right approach, since under this framework the "correct" additive version of `Discrete.lean` would be mapping an `AddMonoid` to an `AddMonoidalCategory`. Next steps would be to: - Make `monoidal_coherence` and `coherence` support `AddMonoidalCategory` - Add `CocartesianMonoidalCategory` extending `AddMonoidalCategory` [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-category-theory large-import new-contributor merge-conflict awaiting-zulip t-meta	444/125	Mathlib/CategoryTheory/Monoidal/Category.lean,Mathlib/CategoryTheory/Monoidal/Discrete.lean,Mathlib/Tactic/ToAdditive/GuessName.lean	3	22	['JovanGerb', 'YaelDillies', 'github-actions', 'imbrem', 'mathlib4-merge-conflict-bot']	nobody	152-18319 5 months ago	191-83385 191 days ago	1-160 1 day
15651	TpmKranz author:TpmKranz	feat(Computability/NFA): operations for Thompson's construction	Lays the groundwork for a proof of equivalence of RE and NFA, w.r.t. described language. Actual connection to REs comes later, after the groundwork for the opposite direction has been laid. Third chunk of #12648 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-computability merge-conflict awaiting-author awaiting-zulip	307/5	Mathlib/Computability/NFA.lean	1	27	['TpmKranz', 'YaelDillies', 'dupuisf', 'github-actions', 'leanprover-community-bot-assistant', 'meithecatte', 'rudynicolop']	nobody	147-35451 4 months ago	566-62839 566 days ago	45-84611 45 days
15649	TpmKranz author:TpmKranz	feat(Computability): introduce Generalised NFA as bridge to Regular Expression	Lays the groundwork for a proof of equivalence of NFA and RE, w.r.t. described language. Actual connection to NFA comes later, after the groundwork for the opposite direction has been laid. Second chunk of #12648 --- - [x] depends on: #15647 [Data.FinEnum.Option unchanged since then] [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-computability merge-conflict awaiting-author awaiting-zulip	298/0	Mathlib.lean,Mathlib/Computability/GNFA.lean,Mathlib/Computability/Language.lean,Mathlib/Computability/RegularExpressions.lean,docs/references.bib	5	7	['github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'meithecatte', 'trivial1711']	nobody	146-51692 4 months ago	492-15222 492 days ago	23-54870 23 days
20648	anthonyde author:anthonyde	feat: formalize regular expression -> εNFA	The file `Computability/RegularExpressionsToEpsilonNFA.lean` contains a formal definition of Thompson's method for constructing an `εNFA` from a `RegularExpression` and a proof of its correctness. --- - [x] depends on: #20644 - [x] depends on: #20645 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	merge-conflict t-computability awaiting-zulip new-contributor	490/0	Mathlib.lean,Mathlib/Computability/RegularExpressionsToEpsilonNFA.lean,docs/references.bib	3	7	['anthonyde', 'github-actions', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'meithecatte', 'qawbecrdtey']	nobody	146-2460 4 months ago	343-35389 343 days ago	75-77754 75 days
11800	JADekker author:JADekker	feat: KappaLindelöf spaces	Define KappaLindelöf spaces by following the first one-third of the API for Lindelöf spaces. The remainder will be added in a future PR. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	please-adopt merge-conflict t-topology awaiting-zulip	301/2	Mathlib.lean,Mathlib/Topology/Compactness/KappaLindelof.lean,Mathlib/Topology/Compactness/Lindelof.lean	3	38	['ADedecker', 'JADekker', 'PatrickMassot', 'StevenClontz', 'adomani', 'github-actions', 'grunweg', 'kim-em', 'urkud']	nobody	145-60726 4 months ago	620-81008 620 days ago	123-25636 123 days
30668	astrainfinita author:astrainfinita	feat: `QuotType`	This typeclass is primarily for use by type synonyms of `Quot` and `Quotient`. Using `QuotType` API for type synonyms of `Quot` and `Quotient` will avoid defeq abuse caused by directly using `Quot` and `Quotient` APIs. This PR also adds some typeclasses to support different ways to find the quotient map that should be used. See the documentation comments of these typeclasses for examples of usage. --- It's not a typical design to use these auxiliary typeclasses and term elaborators, but I haven't found a better way to support these notations. Some of the naming may need to be discussed. For example: - `⟦·⟧` is currently called `mkQ` in names. This distinguishes it from other `.mk`s and makes it possible to write the quotient map as `mkQ` `mkQ'` ~~`mkQ_ h`~~. But this will also require changing the old lemma names. - It would be helpful if the names of new type classes explained their functionality better. [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/migrate.20to.20.60QuotLike.60.20API) This PR continues the work from #16421. Original PR: https://github.com/leanprover-community/mathlib4/pull/16421	RFC t-data awaiting-zulip	629/0	Mathlib.lean,Mathlib/Data/QuotType.lean,MathlibTest/QuotType.lean	3	20	['YaelDillies', 'astrainfinita', 'github-actions', 'mathlib4-merge-conflict-bot', 'plp127', 'vihdzp']	nobody	124-42572 4 months ago	177-11425 177 days ago	0-81 1 minute
33368	urkud author:urkud	feat: define `Complex.UnitDisc.shift`	Also review the existing API UPD: I'm going to define a `PSL(2, Real)` action instead. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-analysis awaiting-zulip merge-conflict	273/39	Mathlib.lean,Mathlib/Analysis/Complex/UnitDisc/Basic.lean,Mathlib/Analysis/Complex/UnitDisc/Shift.lean	3	7	['github-actions', 'j-loreaux', 'mathlib4-merge-conflict-bot', 'sgouezel', 'urkud']	j-loreaux assignee:j-loreaux	97-10885 3 months ago	97-57618 97 days ago	7-33574 7 days
32828	Hagb author:Hagb	feat(Algebra/Order/Group/Defs): add `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid'`	It is similar to `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid`, while with different hypotheses. The conclusion `IsOrderedCancelMonoid α` on `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid` still holds when the hypothesis `CommGroup α` is weakened to `CancelCommMonoid α` while `PartialOrder α` is strengthened to `LinearOrder α`. --- [`IsOrderedAddMonoid.toIsOrderedCancelAddMonoid`](https://leanprover-community.github.io/mathlib4_docs/find/?pattern=IsOrderedAddMonoid.toIsOrderedCancelAddMonoid#doc) and `IsOrderedAddMonoid.toIsOrderedCancelAddMonoid'`: https://github.com/leanprover-community/mathlib4/blob/97f78b1a4311fed1844b94f1c069219a48a098e1/Mathlib/Algebra/Order/Group/Defs.lean#L52-L62 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	awaiting-zulip t-algebra label:t-algebra$	4/0	Mathlib/Algebra/Order/Group/Defs.lean	1	8	['Garmelon', 'Vierkantor', 'artie2000', 'github-actions', 'leanprover-radar']	eric-wieser assignee:eric-wieser	81-59720 2 months ago	81-59720 81 days ago	40-42357 40 days
33031	chiyunhsu author:chiyunhsu	feat(Combinatorics/Enumerative/Partition): add combinatorial proof of Euler's partition theorem	The new file EulerComb.lean contains the combinatorial proof of Euler's partition theorem. The analytic proof of the theorem and its generalization of Glaisher's Theorem has already been formalized in [Glaisher.lean](https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Combinatorics/Enumerative/Partition/Glaisher.lean). The generalization of the combinatorial proof from this file to Glaisher's Theorem is within reach. --- Zulip discussion: [#mathlib4 > Glaisher’s Bijection on integer partitions](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Glaisher.E2.80.99s.20Bijection.20on.20integer.20partitions/with/570808111) [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics new-contributor awaiting-zulip	531/0	Mathlib.lean,Mathlib/Combinatorics/Enumerative/Partition/EulerComb.lean	2	5	['chiyunhsu', 'github-actions', 'tb65536', 'vihdzp']	b-mehta assignee:b-mehta	74-64538 2 months ago	74-64538 74 days ago	42-22427 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	71-76948 2 months ago	97-61080 97 days ago	11-7507 11 days
34720	Paul-Lez author:Paul-Lez	feat(RingTheory/PowerSeries/Composition): define composition of power series	This PR defines the composition of two power series, and adds various pieces of API lemmas (this is mostly fixing up and upstreaming code from [this repo](https://github.com/rmhi/formal_deriv)). This is the first of a series of PRs upstreaming work that was done at the CFT workshop in Oxford last summer, working towards proving some results about the `exp` and `log` power series (and their composition!), and constructing the isomorphism $(\mathfrak{m}_K ^ n, +) \cong (1 + \mathfrak{m}_K ^ n, \times)$ for sufficiently large $n$, where $K$ is a characteristic zero local field. Co-authored-by: Richard Hill Co-authored-by: Calle Sönne --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-ring-theory awaiting-zulip	844/0	Mathlib.lean,Mathlib/RingTheory/PowerSeries/Composition.lean	2	3	['Paul-Lez', 'github-actions', 'vihdzp']	nobody	63-36557 2 months ago	70-74877 70 days ago	0-10 10 seconds
33441	dupuisf author:dupuisf	feat: add `LawfulInv` class for types with an inverse that behaves like `Ring.inverse`	This PR introduces a new typeclass `LawfulInv` for types which have an `Inv` instance that is equal to zero on non-invertible elements. This is meant to replace `Ring.inverse`. The current plan is to do this refactor in several steps: 1. This PR, which only introduces the class and adds instances for matrices and continuous linear maps. 2. Add instances for all C*-algebras, and make `CStarAlgebra` extend this. 3. Deprecate `Ring.inverse`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	awaiting-zulip t-algebra merge-conflict label:t-algebra$	185/27	Mathlib/Algebra/GroupWithZero/Defs.lean,Mathlib/Algebra/GroupWithZero/Invertible.lean,Mathlib/Algebra/GroupWithZero/Units/Basic.lean,Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean,Mathlib/LinearAlgebra/Matrix/PosDef.lean,Mathlib/RingTheory/DividedPowers/Padic.lean,Mathlib/Topology/Algebra/Module/Equiv.lean	7	35	['dupuisf', 'eric-wieser', 'github-actions', 'j-loreaux', 'mathlib-merge-conflicts', 'mathlib4-merge-conflict-bot', 'plp127']	nobody	55-8896 1 month ago	83-42031 83 days ago	7-54141 7 days
26299	adomani author:adomani	perf: the `whitespace` linter only acts on modified files	Introduces an `IO.Ref` to allow the `commandStart` linter to only run on files that git considers modified with respect to `master`. The linter is also active on files that have had some error, as these are likely being modified! The PR should also mitigate the speed-up that the linter introduced: [#mathlib4 > A whitespace linter @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/A.20whitespace.20linter/near/525091877) Assuming that this goes well, a similar mechanism could be applied to several linters that do not need to run on all code, just on the modified code. Implementation detail: the linter is currently either on or off in "whole" files. It may be also a future development to make this more granular and only run the linter on "modifed commands in modified files", but this is not currently the plan for this modification! --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-linter awaiting-zulip awaiting-author	55/7	Mathlib/Tactic/Linter/Whitespace.lean	1	19	['adomani', 'eric-wieser', 'github-actions', 'grunweg', 'joneugster', 'kim-em', 'leanprover-bot', 'leanprover-radar', 'mathlib-bors', 'mathlib4-merge-conflict-bot']	grunweg assignee:grunweg	55-1322 1 month ago	227-84040 227 days ago	66-73556 66 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	46-82094 1 month ago	392-60033 392 days ago	48-67492 48 days
22361	rudynicolop author:rudynicolop	feat(Computability/NFA): nfa closure properties	Add the closure properties union, intersection and reversal for NFA. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	new-contributor t-computability merge-conflict awaiting-author awaiting-zulip	218/2	Mathlib/Computability/Language.lean,Mathlib/Computability/NFA.lean	2	91	['EtienneC30', 'b-mehta', 'ctchou', 'github-actions', 'leanprover-community-bot-assistant', 'meithecatte', 'rudynicolop']	nobody	46-82078 1 month ago	343-63972 343 days ago	39-61332 39 days
23929	meithecatte author:meithecatte	feat(Computability/NFA): improve bound on pumping lemma	--- - [x] depends on: #25321 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-computability awaiting-zulip new-contributor awaiting-author	101/10	Mathlib/Computability/EpsilonNFA.lean,Mathlib/Computability/NFA.lean	2	42	['YaelDillies', 'dagurtomas', 'github-actions', 'leanprover-community-bot-assistant', 'mathlib4-dependent-issues-bot', 'meithecatte']	nobody	46-15707 1 month ago	310-45006 310 days ago	34-10092 34 days
34245	staroperator author:staroperator	feat(Data/Set): add `Set.Uncountable`	There are `Set` specialized shortcuts `Set.Finite`, `Set.Infinite` and `Set.Countable`, but lacking `Set.Uncountable`. I find this useful in #34246. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-data awaiting-zulip	82/4	Mathlib/Analysis/Real/Cardinality.lean,Mathlib/Data/Set/Countable.lean,Mathlib/SetTheory/Cardinal/Basic.lean	3	17	['github-actions', 'joneugster', 'staroperator', 'vihdzp']	joneugster assignee:joneugster	38-80321 1 month ago	69-53568 69 days ago	12-21154 12 days
35524	grunweg author:grunweg	feat: text-based linter against \t followed by tactic mode	Wait for the zulip discussion to converge. If there is consensus in favour of this change, summarise the motivation here. [zulip discuss](https://leanprover.zulipchat.com/#narrow/channel/345428-mathlib-reviewers/topic/proposal.3A.20no.20more.20use.20of.20.60.E2.96.B8.60.20in.20Mathlib.3F/with/574680826) --- There are currently 80 remaining exceptions in mathlib: ideally, these would get fixed before merging this. Works best when combined with #35523. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-linter awaiting-zulip merge-conflict	23/2	Mathlib/Tactic/Linter/TextBased.lean	1	5	['github-actions', 'grunweg', 'joneugster', 'mathlib-merge-conflicts', 'vihdzp']	nobody	27-33459 27 days ago	53-81021 53 days ago	0-187 3 minutes
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	26-54854 26 days ago	112-54045 112 days ago	10-66980 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	22-5863 22 days ago	24-79003 24 days ago	0-10825 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	18-35552 18 days ago	55-2647 55 days ago	0-58585 16 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	18-16338 18 days ago	52-36856 52 days ago	0-18707 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	15-36658 15 days ago	16-52014 16 days ago	11-84307 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	7	['SnirBroshi', 'TwoFX', 'eric-wieser', 'github-actions', 'linesthatinterlace', 'mathlib-merge-conflicts']	TwoFX assignee:TwoFX	14-53777 14 days ago	138-1248 138 days ago	35-84279 35 days

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

Number	Author	Title	Description	Labels	+/-	Modified files (first 100)	📝	💬	All users who commented or reviewed	Assignee(s)	Updated	Last status change	total time in review
37503	Vierkantor author:Vierkantor	chore(*): remove comments mentioning obsolete note `[nolint_ge]`	In Lean 3 times we used to have a `ge_or_gt` linter which complained if theorem statements contained `≥` or `>`, and it would be silenced with a reference to the library note `[nolint_ge]`. But the linter and its note never got ported, so the references are irrelevant and we should drop them. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-linter tech debt	1/6	Mathlib/Algebra/Order/CauSeq/Basic.lean,Mathlib/Order/Basic.lean,Mathlib/Order/Filter/AtTopBot/Finite.lean,Mathlib/Topology/EMetricSpace/Basic.lean,Mathlib/Topology/MetricSpace/Cauchy.lean	5	4	['Vierkantor', 'github-actions', 'grunweg']	nobody	11-80353 11 days ago	12-61265 12 days ago	12-61212 12 days
37358	grunweg author:grunweg	chore(Geometry/Manifold): don't expose definitions depending on choice	Some definitions in `Immersion.lean` still depend on choice, but need to be exposed for subsequent instances using their definition. We leave them alone for now. Also make not exposing definition the default in `LocalDiffeomorph.lean`; four definitions have useful definitional equalities, the others do not. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-differential-geometry tech debt	12/12	Mathlib/Geometry/Manifold/Immersion.lean,Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean,Mathlib/Geometry/Manifold/LocalDiffeomorph.lean,Mathlib/Geometry/Manifold/VectorBundle/Basic.lean	4	1	['github-actions']	PatrickMassot assignee:PatrickMassot	2-25924 2 days ago	3-58118 3 days ago	3-58438 3 days
37678	vihdzp author:vihdzp	chore(Dynamics/FixedPoints/Defs): create `Defs` file	--- I got a large import warning on another PR for simply importing the definition `Function.fixedPoints`, which I found rather silly. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-dynamics tech debt maintainer-merge	67/44	Mathlib.lean,Mathlib/Dynamics/FixedPoints/Basic.lean,Mathlib/Dynamics/FixedPoints/Defs.lean,Mathlib/Logic/Function/Defs.lean	4	2	['Ruben-VandeVelde', 'github-actions']	urkud assignee:urkud	0-84226 23 hours ago	8-34514 8 days ago	8-35039 8 days
38007	JovanGerb author:JovanGerb	perf(Data/Complex/Basic): `no_expose` the `Inv` and `Norm` instance	This PR hides some more implementation details of complex numbers. It would be possible to `no_expose` even more definitions, but this could be at the cost of some proof writing convenience. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	tech debt	11/12	Mathlib/Analysis/Complex/Basic.lean,Mathlib/Analysis/Complex/Norm.lean,Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean,Mathlib/Data/Complex/Basic.lean	4	6	['JovanGerb', 'github-actions', 'grunweg', 'leanprover-radar']	nobody	0-33522 9 hours ago	0-52599 14 hours ago	0-52635 14 hours