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: May 13, 2026 at 06:00 UTC

Stale ready-to-merge'd PRs

Number	Author	Title	Description	Labels	+/-	Modified files (first 100)	📝	💬	All users who commented or reviewed	Assignee(s)	Updated	Last status change	total time in review
37406	vihdzp author:vihdzp	feat(SetTheory/Cardinal): `IsStrongPrelimit` predicate	We introduce a predicate for cardinals `c` such that `x < c` implies `x < 2 ^ c`. This is to `IsStrongLimit` as `IsSuccPrelimit` is to `IsSuccLimit`. We then make use of it in a few places where we were writing down `∀ x < c, x < 2 ^ c` explicitly. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-set-theory ready-to-merge	53/26	Mathlib/SetTheory/Cardinal/Aleph.lean,Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean,Mathlib/SetTheory/Cardinal/Order.lean,Mathlib/SetTheory/Cardinal/Regular.lean	4	6	['YaelDillies', 'github-actions', 'mathlib-bors', 'mathlib-merge-conflicts', 'riccardobrasca', 'vihdzp']	alreadydone assignee:alreadydone	2-33670 2 days ago	2-76467 2 days ago	36-65745 36 days
37625	slavanaprienko author:slavanaprienko	feat(LinearAlgebra/Matrix/Charpoly): general coefficient formula as sum of principal minors	This PR adds a general formula for the coefficients of `det(1 + X • M)` as sums of principal minors, generalizing the existing `coeff_det_one_add_X_smul_one` (k=1, trace) and `det_eq_sign_charpoly_coeff` (k=n, determinant). It also derives the corresponding formula for the coefficients of the characteristic polynomial via `charpolyRev`. New results: - `det_piecewise_one_eq_submatrix_det`: relates piecewise-with-identity to principal submatrix determinants - `coeff_det_one_add_X_smul_eq_sum_minors`: the k-th coefficient of `det(1 + X • M)` equals the sum of k×k principal minors - `charpoly_coeff_eq_sum_minors`: coefficients of the characteristic polynomial as signed sums of principal minors ---	t-algebra new-contributor ready-to-merge label:t-algebra$	105/1	Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean	1	28	['eric-wieser', 'github-actions', 'kim-em', 'mathlib-bors', 'slavanaprienko', 'wwylele']	nobody	1-33288 1 day ago	2-3463 2 days ago	37-2235 37 days

Stale maintainer-merge'd PRs

Number	Author	Title	Description	Labels	+/-	Modified files (first 100)	📝	💬	All users who commented or reviewed	Assignee(s)	Updated	Last status change	total time in review
34633	mitchell-horner author:mitchell-horner	feat(Combinatorics/SimpleGraph): define the Zarankiewicz function	Defines the Zarankiewicz function $z(m, n; s, t)$ in terms of bipartite graphs. --- - [x] depends on: #34632 This comes from splitting up #25841 into smaller PRs. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics maintainer-merge blocked-by-other-PR	247/0	Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Extremal/Zarankiewicz.lean,Mathlib/Combinatorics/SimpleGraph/Maps.lean	4	30	['SnirBroshi', 'YaelDillies', 'b-mehta', 'github-actions', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'mitchell-horner']	nobody	101-7849 3 months ago	2-20744 2 days ago	47-31366 47 days
31141	peabrainiac author:peabrainiac	feat(Analysis/Calculus): parametric integrals over smooth functions are smooth	Show that for any smooth function `f : H × ℝ → E`, the parametric integral `fun x ↦ ∫ t in a..b, f (x, t) ∂μ` is smooth too. The argument proceeds inductively, using the fact that derivatives of parametric integrals can themselves be computed as parametric integrals. The necessary lemmas on derivatives of parametric integrals already existed, but took some work to apply due to their generality; we state some convenient special cases. --- - [x] depends on: #31077 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-analysis awaiting-author maintainer-merge	470/12	Mathlib/Analysis/Calculus/ParametricIntegral.lean,Mathlib/Analysis/Calculus/ParametricIntervalIntegral.lean,Mathlib/MeasureTheory/Integral/DominatedConvergence.lean,Mathlib/Topology/NhdsWithin.lean,Mathlib/Topology/Separation/Regular.lean	5	36	['fpvandoorn', 'github-actions', 'j-loreaux', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'peabrainiac', 'sgouezel']	j-loreaux assignee:j-loreaux	90-67010 3 months ago	90-67010 90 days ago	22-14837 22 days
35619	SnirBroshi author:SnirBroshi	feat(Combinatorics/SimpleGraph/Clique): intersection and union of cliques	Plus a couple of lemmas. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics maintainer-merge	29/0	Mathlib/Combinatorics/SimpleGraph/Clique.lean,Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean,Mathlib/Data/Set/Pairwise/Basic.lean	1	13	['SnirBroshi', 'YaelDillies', 'github-actions']	nobody	80-19400 2 months ago	13-80780 13 days ago	19-70642 19 days
28685	mitchell-horner author:mitchell-horner	feat(Combinatorics/SimpleGraph): prove the minimal-degree version of the Erdős-Stone theorem	Proves the minimal degree-version of the Erdős-Stone theorem: If `G` has a minimal degree of at least `(1 - 1 / r + o(1)) * card V`, then `G` contains a copy of a `completeEquipartiteGraph` in `r + 1` parts each of size `t`. The double-counting construction from the proof is available in `namespace ErdosStone`. --- - [x] depends on: #25843 - [x] depends on: #27597 - [x] depends on: #27599 - [x] depends on: #28443 - [x] depends on: #28445 - [x] depends on: #28446 - [x] depends on: #28447 This is the first of several pull requests towards the full Erdős-Stone(-Simonovits) theorem, hence the name of the file. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics maintainer-merge	323/0	Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Extremal/ErdosStoneSimonovits.lean	2	19	['YaelDillies', 'b-mehta', 'github-actions', 'mathlib-dependent-issues', 'mathlib4-merge-conflict-bot', 'mitchell-horner', 'robin-carlier']	b-mehta assignee:b-mehta	71-83924 2 months ago	8-21442 8 days ago	69-23808 69 days
35753	Vilin97 author:Vilin97	feat(Topology/Algebra/Order): regular grid helpers and piecewise linear interpolation	Make API for piecewise linear interpolation on regular grids. I need these to for ODE time-stepping methods, like forward Euler, and later Runge–Kutta methods. Follow-up PR: #35755 (forward Euler method convergence). I don't know if these numerical analysis ODE-solving methods even belong in mathlib. If someone could advise me on it, I would appreciate it. --- The initial proof was produced by [Aristotle](https://aristotle.harmonic.fun). The code was iteratively refined (factoring out lemmas, golfing, simplifying proofs) using Claude Code. - [ ] depends on: #38091	t-topology new-contributor LLM-generated maintainer-merge awaiting-author	151/0	Mathlib.lean,Mathlib/Topology/Algebra/Order/PiecewiseLinear.lean	3	58	['Vilin97', 'YanYablonovskiy', 'adomani', 'botbaki-review', 'copilot-pull-request-reviewer', 'dagurtomas', 'eric-wieser', 'github-actions', 'grunweg', 'j-loreaux', 'mathlib-dependent-issues', 'wwylele']	j-loreaux assignee:j-loreaux	68-48403 2 months ago	11-28124 11 days ago	43-67974 43 days
36451	SnirBroshi author:SnirBroshi	feat(Combinatorics/SimpleGraph/Matching): `edgeSet` is injective and strictly monotonic on matchings, and more API	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics maintainer-merge	45/11	Mathlib/Combinatorics/SimpleGraph/Matching.lean,Mathlib/Combinatorics/SimpleGraph/Subgraph.lean	3	13	['SnirBroshi', 'YaelDillies', 'github-actions', 'mathlib-merge-conflicts']	b-mehta assignee:b-mehta	63-40174 2 months ago	19-45896 19 days ago	47-81335 47 days
33506	Rida-Hamadani author:Rida-Hamadani	feat(SimpleGraph): construct a cycle of two distinct paths with same start and end	Co-authored-by: Vlad Tsyrklevich Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> --- - [x] depends on: #33249 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics maintainer-merge	109/1	Mathlib/Combinatorics/SimpleGraph/Paths.lean,Mathlib/Combinatorics/SimpleGraph/Walk/Basic.lean,Mathlib/Combinatorics/SimpleGraph/Walk/Decomp.lean,Mathlib/Data/List/Basic.lean,Mathlib/Data/List/Nodup.lean	4	60	['Rida-Hamadani', 'SnirBroshi', 'YaelDillies', 'github-actions', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'mathlib4-merge-conflict-bot', 'vlad902']	nobody	59-63397 1 month ago	4-39533 4 days ago	22-54786 22 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	34-85900 1 month ago	36-47140 36 days ago	4-43742 4 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	26-65494 26 days ago	26-64742 26 days ago	41-84090 41 days
37346	euprunin author:euprunin	chore: golf using `grind`	The goal of this PR is to decrease the number of times lemmas are called explicitly. Any decrease in compilation time is a welcome side effect, although it is not a primary objective. Trace profiling results (differences <30 ms considered measurement noise): * `✅️ SimpleGraph.Walk.IsPath.getVert_injOn`: unchanged 🎉 * `✅️ SimpleGraph.Walk.length_bypass_le`: unchanged 🎉 * `✅️ Rat.floor_intCast_div_natCast`: unchanged 🎉 * `✅️ InnerProductGeometry.norm_eq_of_angle_sub_eq_angle_sub_rev_of_angle_ne_pi`: unchanged 🎉 * `✅️ padicNorm.zero_of_padicNorm_eq_zero`: unchanged 🎉 Profiled using `set_option trace.profiler true in`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge awaiting-zulip	7/45	Mathlib/Combinatorics/SimpleGraph/Paths.lean,Mathlib/Data/Rat/Floor.lean,Mathlib/Geometry/Euclidean/Triangle.lean,Mathlib/NumberTheory/Padics/PadicNorm.lean	4	22	['FernandoChu', 'bryangingechen', 'chenson2018', 'euprunin', 'faenuccio', 'github-actions', 'grunweg']	nobody	13-64742 13 days ago	13-64773 13 days ago	30-45859 30 days
38269	b-mehta author:b-mehta	feat(Combinatorics/Additive): link Freiman homs and Freiman isos tighter	--- Some work I had lying around in a forgotten branch, recently resurrected. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics maintainer-merge	118/76	Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean,Mathlib/Combinatorics/Additive/AP/Three/Defs.lean,Mathlib/Combinatorics/Additive/FreimanHom.lean	3	15	['YaelDillies', 'b-mehta', 'github-actions', 'mathlib-merge-conflicts']	nobody	13-60505 13 days ago	13-59013 13 days ago	14-56004 14 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 merge-conflict	120/165	Mathlib/Algebra/Algebra/Operations.lean,Mathlib/Data/Set/Semiring.lean	2	42	['Parcly-Taxel', 'YaelDillies', 'eric-wieser', 'github-actions', 'mathlib-merge-conflicts', 'sgouezel']	nobody	13-21078 13 days ago	13-21079 13 days ago	22-34679 22 days
38358	yuanyi-350 author:yuanyi-350	doc(1000.yaml): note more formalised theorems	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	documentation maintainer-merge	9/2	docs/1000.yaml	1	12	['YaelDillies', 'github-actions', 'grunweg', 'vihdzp', 'yuanyi-350']	nobody	9-72496 9 days ago	9-71937 9 days ago	20-68604 20 days
37295	wwylele author:wwylele	feat(Analysis/InnerProductSpace): generalized determinant of a rectangle matrix / linear map	This is the volume factor of a linear map --- I have encountered the expression `sqrt(det(T' * T))` a few times in various places but it doesn't look like it has a standard name and entry in mathlib, so this adds it. Zulip thread [#Is there code for X? > (norm of) "determinant" of map between inner product spaces](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/.28norm.20of.29.20.22determinant.22.20of.20map.20between.20inner.20product.20spaces/with/581776873) One motivation to define this is to state volume formula under transformations. From Measure theory and fine properties of functions: - Lemma 3.1: for linear map $L : \mathbb{R}^n \to \mathbb{R}^m$, we have $\mathcal{H}^n(L(A)) = [ L ] \mathcal{L}^n(A)$. This is proved in this PR at `euclideanHausdorffMeasure_image_eq_normDet_mul_volume` - Theorem 3.8, for (not necessarily linear) $f : \mathbb{R}^n \to \mathbb{R}^m$ ($n \le m$) and $\mathcal{L}^n$-measurable set $A \subset \mathbb{R}^n$, we have $\int_A J f dx = \int_{\mathbb{R}^m} \mathcal{H}^0(A \cap f\^{-1}\{y\}) d\mathcal{H}^n(y)$, where $J f$ is the `normDet` of the rectangular Jacobian matrix AI usage disclosure: AI was used in the following parts - searching for related literature for an appropriate name - generate draft proofs for some lemma to verify their correctness, though the final code has been completely rewritten by me. - [ ] depends on: #37918 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-analysis maintainer-merge	480/0	Mathlib.lean,Mathlib/Analysis/InnerProductSpace/Adjoint.lean,Mathlib/Analysis/InnerProductSpace/NormDet.lean,docs/references.bib	4	18	['copilot-pull-request-reviewer', 'github-actions', 'j-loreaux', 'mathlib-dependent-issues', 'themathqueen', 'wwylele']	j-loreaux assignee:j-loreaux	8-40187 8 days ago	8-39187 8 days ago	42-18991 42 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	6	['Rida-Hamadani', 'Ruben-VandeVelde', 'SnirBroshi', 'bryangingechen', 'github-actions']	nobody	2-77427 2 days ago	40-58757 40 days ago	43-10186 43 days
37443	SnirBroshi author:SnirBroshi	feat(Combinatorics/SimpleGraph/Walk/Operations): permutations of support	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics maintainer-merge	17/0	Mathlib/Combinatorics/SimpleGraph/Paths.lean,Mathlib/Combinatorics/SimpleGraph/Walk/Operations.lean	2	6	['YaelDillies', 'github-actions', 'mathlib-merge-conflicts']	YaelDillies assignee:YaelDillies	1-75468 1 day ago	1-75840 1 day ago	41-59215 41 days
37464	martinwintermath author:martinwintermath	feat(Geometry/Convex/Cone): Minor additions to pointed cones	Minor additions to pointed cones: * `PointedCone.ofSubmodule_le_ofSubmodule` and `PointedCone.ofSubmodule_lt_ofSubmodule`. These are not made simp lemmas, instead the underlying `Submodule.restrictScalars_le` and `Submodule.restrictScalars_lt` have been changed into simp lemmas. * `PointedCone.hull_le_span` as a short form of `Submodule.span_le_restrictScalars R≥0 R s` Co-authored by: Artie Khovanov --- In preparation of #36605. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-convex-geometry maintainer-merge	22/16	Mathlib/Algebra/Module/Submodule/RestrictScalars.lean,Mathlib/Geometry/Convex/Cone/Pointed.lean	2	24	['YaelDillies', 'artie2000', 'github-actions', 'justus-springer', 'martinwintermath', 'mathlib-merge-conflicts', 'ooovi', 'vihdzp']	nobody	1-54278 1 day ago	1-51984 1 day ago	40-78917 40 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	9	['YaelDillies', 'artie2000', 'github-actions', 'mathlib-merge-conflicts', 'ocfnash']	nobody	1-29291 1 day ago	1-29292 1 day ago	46-64967 46 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
34633	mitchell-horner author:mitchell-horner	feat(Combinatorics/SimpleGraph): define the Zarankiewicz function	Defines the Zarankiewicz function $z(m, n; s, t)$ in terms of bipartite graphs. --- - [x] depends on: #34632 This comes from splitting up #25841 into smaller PRs. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics maintainer-merge blocked-by-other-PR	247/0	Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Extremal/Zarankiewicz.lean,Mathlib/Combinatorics/SimpleGraph/Maps.lean	4	30	['SnirBroshi', 'YaelDillies', 'b-mehta', 'github-actions', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'mitchell-horner']	nobody	101-7849 3 months ago	2-20744 2 days ago	47-31366 47 days
31141	peabrainiac author:peabrainiac	feat(Analysis/Calculus): parametric integrals over smooth functions are smooth	Show that for any smooth function `f : H × ℝ → E`, the parametric integral `fun x ↦ ∫ t in a..b, f (x, t) ∂μ` is smooth too. The argument proceeds inductively, using the fact that derivatives of parametric integrals can themselves be computed as parametric integrals. The necessary lemmas on derivatives of parametric integrals already existed, but took some work to apply due to their generality; we state some convenient special cases. --- - [x] depends on: #31077 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-analysis awaiting-author maintainer-merge	470/12	Mathlib/Analysis/Calculus/ParametricIntegral.lean,Mathlib/Analysis/Calculus/ParametricIntervalIntegral.lean,Mathlib/MeasureTheory/Integral/DominatedConvergence.lean,Mathlib/Topology/NhdsWithin.lean,Mathlib/Topology/Separation/Regular.lean	5	36	['fpvandoorn', 'github-actions', 'j-loreaux', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot', 'peabrainiac', 'sgouezel']	j-loreaux assignee:j-loreaux	90-67010 3 months ago	90-67010 90 days ago	22-14837 22 days
35619	SnirBroshi author:SnirBroshi	feat(Combinatorics/SimpleGraph/Clique): intersection and union of cliques	Plus a couple of lemmas. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics maintainer-merge	29/0	Mathlib/Combinatorics/SimpleGraph/Clique.lean,Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean,Mathlib/Data/Set/Pairwise/Basic.lean	1	13	['SnirBroshi', 'YaelDillies', 'github-actions']	nobody	80-19400 2 months ago	13-80780 13 days ago	19-70642 19 days
28685	mitchell-horner author:mitchell-horner	feat(Combinatorics/SimpleGraph): prove the minimal-degree version of the Erdős-Stone theorem	Proves the minimal degree-version of the Erdős-Stone theorem: If `G` has a minimal degree of at least `(1 - 1 / r + o(1)) * card V`, then `G` contains a copy of a `completeEquipartiteGraph` in `r + 1` parts each of size `t`. The double-counting construction from the proof is available in `namespace ErdosStone`. --- - [x] depends on: #25843 - [x] depends on: #27597 - [x] depends on: #27599 - [x] depends on: #28443 - [x] depends on: #28445 - [x] depends on: #28446 - [x] depends on: #28447 This is the first of several pull requests towards the full Erdős-Stone(-Simonovits) theorem, hence the name of the file. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics maintainer-merge	323/0	Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Extremal/ErdosStoneSimonovits.lean	2	19	['YaelDillies', 'b-mehta', 'github-actions', 'mathlib-dependent-issues', 'mathlib4-merge-conflict-bot', 'mitchell-horner', 'robin-carlier']	b-mehta assignee:b-mehta	71-83924 2 months ago	8-21442 8 days ago	69-23808 69 days
35753	Vilin97 author:Vilin97	feat(Topology/Algebra/Order): regular grid helpers and piecewise linear interpolation	Make API for piecewise linear interpolation on regular grids. I need these to for ODE time-stepping methods, like forward Euler, and later Runge–Kutta methods. Follow-up PR: #35755 (forward Euler method convergence). I don't know if these numerical analysis ODE-solving methods even belong in mathlib. If someone could advise me on it, I would appreciate it. --- The initial proof was produced by [Aristotle](https://aristotle.harmonic.fun). The code was iteratively refined (factoring out lemmas, golfing, simplifying proofs) using Claude Code. - [ ] depends on: #38091	t-topology new-contributor LLM-generated maintainer-merge awaiting-author	151/0	Mathlib.lean,Mathlib/Topology/Algebra/Order/PiecewiseLinear.lean	3	58	['Vilin97', 'YanYablonovskiy', 'adomani', 'botbaki-review', 'copilot-pull-request-reviewer', 'dagurtomas', 'eric-wieser', 'github-actions', 'grunweg', 'j-loreaux', 'mathlib-dependent-issues', 'wwylele']	j-loreaux assignee:j-loreaux	68-48403 2 months ago	11-28124 11 days ago	43-67974 43 days
36451	SnirBroshi author:SnirBroshi	feat(Combinatorics/SimpleGraph/Matching): `edgeSet` is injective and strictly monotonic on matchings, and more API	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics maintainer-merge	45/11	Mathlib/Combinatorics/SimpleGraph/Matching.lean,Mathlib/Combinatorics/SimpleGraph/Subgraph.lean	3	13	['SnirBroshi', 'YaelDillies', 'github-actions', 'mathlib-merge-conflicts']	b-mehta assignee:b-mehta	63-40174 2 months ago	19-45896 19 days ago	47-81335 47 days
33506	Rida-Hamadani author:Rida-Hamadani	feat(SimpleGraph): construct a cycle of two distinct paths with same start and end	Co-authored-by: Vlad Tsyrklevich Co-authored-by: Snir Broshi <26556598+SnirBroshi@users.noreply.github.com> --- - [x] depends on: #33249 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics maintainer-merge	109/1	Mathlib/Combinatorics/SimpleGraph/Paths.lean,Mathlib/Combinatorics/SimpleGraph/Walk/Basic.lean,Mathlib/Combinatorics/SimpleGraph/Walk/Decomp.lean,Mathlib/Data/List/Basic.lean,Mathlib/Data/List/Nodup.lean	4	60	['Rida-Hamadani', 'SnirBroshi', 'YaelDillies', 'github-actions', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'mathlib4-merge-conflict-bot', 'vlad902']	nobody	59-63397 1 month ago	4-39533 4 days ago	22-54786 22 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	34-85900 1 month ago	36-47140 36 days ago	4-43742 4 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	26-65494 26 days ago	26-64742 26 days ago	41-84090 41 days
37346	euprunin author:euprunin	chore: golf using `grind`	The goal of this PR is to decrease the number of times lemmas are called explicitly. Any decrease in compilation time is a welcome side effect, although it is not a primary objective. Trace profiling results (differences <30 ms considered measurement noise): * `✅️ SimpleGraph.Walk.IsPath.getVert_injOn`: unchanged 🎉 * `✅️ SimpleGraph.Walk.length_bypass_le`: unchanged 🎉 * `✅️ Rat.floor_intCast_div_natCast`: unchanged 🎉 * `✅️ InnerProductGeometry.norm_eq_of_angle_sub_eq_angle_sub_rev_of_angle_ne_pi`: unchanged 🎉 * `✅️ padicNorm.zero_of_padicNorm_eq_zero`: unchanged 🎉 Profiled using `set_option trace.profiler true in`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge awaiting-zulip	7/45	Mathlib/Combinatorics/SimpleGraph/Paths.lean,Mathlib/Data/Rat/Floor.lean,Mathlib/Geometry/Euclidean/Triangle.lean,Mathlib/NumberTheory/Padics/PadicNorm.lean	4	22	['FernandoChu', 'bryangingechen', 'chenson2018', 'euprunin', 'faenuccio', 'github-actions', 'grunweg']	nobody	13-64742 13 days ago	13-64773 13 days ago	30-45859 30 days
38269	b-mehta author:b-mehta	feat(Combinatorics/Additive): link Freiman homs and Freiman isos tighter	--- Some work I had lying around in a forgotten branch, recently resurrected. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics maintainer-merge	118/76	Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean,Mathlib/Combinatorics/Additive/AP/Three/Defs.lean,Mathlib/Combinatorics/Additive/FreimanHom.lean	3	15	['YaelDillies', 'b-mehta', 'github-actions', 'mathlib-merge-conflicts']	nobody	13-60505 13 days ago	13-59013 13 days ago	14-56004 14 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 merge-conflict	120/165	Mathlib/Algebra/Algebra/Operations.lean,Mathlib/Data/Set/Semiring.lean	2	42	['Parcly-Taxel', 'YaelDillies', 'eric-wieser', 'github-actions', 'mathlib-merge-conflicts', 'sgouezel']	nobody	13-21078 13 days ago	13-21079 13 days ago	22-34679 22 days
38358	yuanyi-350 author:yuanyi-350	doc(1000.yaml): note more formalised theorems	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	documentation maintainer-merge	9/2	docs/1000.yaml	1	12	['YaelDillies', 'github-actions', 'grunweg', 'vihdzp', 'yuanyi-350']	nobody	9-72496 9 days ago	9-71937 9 days ago	20-68604 20 days
37295	wwylele author:wwylele	feat(Analysis/InnerProductSpace): generalized determinant of a rectangle matrix / linear map	This is the volume factor of a linear map --- I have encountered the expression `sqrt(det(T' * T))` a few times in various places but it doesn't look like it has a standard name and entry in mathlib, so this adds it. Zulip thread [#Is there code for X? > (norm of) "determinant" of map between inner product spaces](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/.28norm.20of.29.20.22determinant.22.20of.20map.20between.20inner.20product.20spaces/with/581776873) One motivation to define this is to state volume formula under transformations. From Measure theory and fine properties of functions: - Lemma 3.1: for linear map $L : \mathbb{R}^n \to \mathbb{R}^m$, we have $\mathcal{H}^n(L(A)) = [ L ] \mathcal{L}^n(A)$. This is proved in this PR at `euclideanHausdorffMeasure_image_eq_normDet_mul_volume` - Theorem 3.8, for (not necessarily linear) $f : \mathbb{R}^n \to \mathbb{R}^m$ ($n \le m$) and $\mathcal{L}^n$-measurable set $A \subset \mathbb{R}^n$, we have $\int_A J f dx = \int_{\mathbb{R}^m} \mathcal{H}^0(A \cap f\^{-1}\{y\}) d\mathcal{H}^n(y)$, where $J f$ is the `normDet` of the rectangular Jacobian matrix AI usage disclosure: AI was used in the following parts - searching for related literature for an appropriate name - generate draft proofs for some lemma to verify their correctness, though the final code has been completely rewritten by me. - [ ] depends on: #37918 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-analysis maintainer-merge	480/0	Mathlib.lean,Mathlib/Analysis/InnerProductSpace/Adjoint.lean,Mathlib/Analysis/InnerProductSpace/NormDet.lean,docs/references.bib	4	18	['copilot-pull-request-reviewer', 'github-actions', 'j-loreaux', 'mathlib-dependent-issues', 'themathqueen', 'wwylele']	j-loreaux assignee:j-loreaux	8-40187 8 days ago	8-39187 8 days ago	42-18991 42 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	6	['Rida-Hamadani', 'Ruben-VandeVelde', 'SnirBroshi', 'bryangingechen', 'github-actions']	nobody	2-77427 2 days ago	40-58757 40 days ago	43-10186 43 days
37443	SnirBroshi author:SnirBroshi	feat(Combinatorics/SimpleGraph/Walk/Operations): permutations of support	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics maintainer-merge	17/0	Mathlib/Combinatorics/SimpleGraph/Paths.lean,Mathlib/Combinatorics/SimpleGraph/Walk/Operations.lean	2	6	['YaelDillies', 'github-actions', 'mathlib-merge-conflicts']	YaelDillies assignee:YaelDillies	1-75468 1 day ago	1-75840 1 day ago	41-59215 41 days
37464	martinwintermath author:martinwintermath	feat(Geometry/Convex/Cone): Minor additions to pointed cones	Minor additions to pointed cones: * `PointedCone.ofSubmodule_le_ofSubmodule` and `PointedCone.ofSubmodule_lt_ofSubmodule`. These are not made simp lemmas, instead the underlying `Submodule.restrictScalars_le` and `Submodule.restrictScalars_lt` have been changed into simp lemmas. * `PointedCone.hull_le_span` as a short form of `Submodule.span_le_restrictScalars R≥0 R s` Co-authored by: Artie Khovanov --- In preparation of #36605. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-convex-geometry maintainer-merge	22/16	Mathlib/Algebra/Module/Submodule/RestrictScalars.lean,Mathlib/Geometry/Convex/Cone/Pointed.lean	2	24	['YaelDillies', 'artie2000', 'github-actions', 'justus-springer', 'martinwintermath', 'mathlib-merge-conflicts', 'ooovi', 'vihdzp']	nobody	1-54278 1 day ago	1-51984 1 day ago	40-78917 40 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	9	['YaelDillies', 'artie2000', 'github-actions', 'mathlib-merge-conflicts', 'ocfnash']	nobody	1-29291 1 day ago	1-29292 1 day ago	46-64967 46 days
36376	jessealama author:jessealama	feat(SimpleGraph): hamiltonian cycle from cyclic permutation	This PR provides `IsHamiltonian.of_perm`, a bridge from `Equiv.Perm.IsCycle` to `SimpleGraph.IsHamiltonian`: if σ is a permutation that is a single cycle with full support on at least 3 elements, and each step `v → σ v` is an edge of `G`, then `G` is Hamiltonian. ### New definitions and lemmas `Mathlib/Data/List/Chain.lean`: - `IsChain.iterate`: `List.iterate f a n` is a chain under `r` whenever `r a (f a)` holds for all `a` `Mathlib/Data/List/Iterate.lean`: - `getLast_iterate`: the last element of `List.iterate f a n` is `f^[n - 1] a` `Mathlib/Combinatorics/SimpleGraph/Walk/Iterate.lean` (new file): - `Walk.iterate`: builds a walk of length `n` from `x` to `f^[n] x` for any function `f` with `G.Adj x (f x)` for all `x`, defined via `Walk.ofSupport` - `Walk.length_iterate`, `Walk.support_iterate`, `Walk.edges_iterate`: basic API `Mathlib/GroupTheory/Perm/Cycle/Basic.lean`: - `IsCycleOn.injOn_pow_apply`: the map `n ↦ (f ^ n) a` is injective on `Finset.range #s` `Mathlib/GroupTheory/Perm/Cycle/Concrete.lean`: - `IsCycleOn.injOn_sym2_pow_apply`: the unordered-pair edge map `k ↦ s((f ^ k) a, (f ^ (k + 1)) a)` is injective on `[0, #s)` when `#s ≠ 2` - `IsCycleOn.sym2_pow_apply_ne`: edge distinctness for cycle-on permutations — `s((f ^ k) a, (f ^ (k + 1)) a) ≠ s(a, f a)` when `k ≠ 0`, `k < #s`, and `#s ≠ 2` - `Perm.toList_eq_range_map_pow`: expresses `toList` as a range map over powers `Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean`: - `cons_isHamiltonianCycle_iff`: a Hamiltonian path closed by an edge outside its support is a Hamiltonian cycle, and conversely - `IsHamiltonian.of_perm`: the main theorem --- - [x] depends on: #36307	t-combinatorics maintainer-merge	182/0	Mathlib.lean,Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean,Mathlib/Combinatorics/SimpleGraph/Hamiltonian/Perm.lean,Mathlib/Combinatorics/SimpleGraph/Walk/Iterate.lean,Mathlib/Data/List/Chain.lean,Mathlib/Data/List/Iterate.lean,Mathlib/GroupTheory/Perm/Cycle/Basic.lean,Mathlib/GroupTheory/Perm/Cycle/Concrete.lean	8	76	['SnirBroshi', 'YaelDillies', 'github-actions', 'jessealama', 'mathlib-dependent-issues', 'mathlib-merge-conflicts']	nobody	0-62907 17 hours ago	0-63042 17 hours ago	43-62724 43 days
37577	SnirBroshi author:SnirBroshi	feat(Combinatorics/SimpleGraph/Walk): upgrade subset theorems to sublist/prefix/suffix	Upgrades theorems about `p.support ⊆ q.support` / `p.darts ⊆ q.darts` / `p.edges ⊆ q.edges` to `List.IsInfix`/`List.IsSuffix`/`List.Sublist`, which imply the subset versions. Also adds `cycleBypass` sublist lemmas that were missing, and golfs `length_bypass_le` and `bypass_eq_self_of_length_le` using the new sublist theorems. Co-authored-by: Iván Renison <85908989+IvanRenison@users.noreply.github.com> --- Except for a couple of `cycleBypass` ones, I did not add such theorems where there was no subset theorem to begin with (e.g. `(p.take n).darts <+: p.darts`), as they are usually not worth stating since they're trivial and simp proves them. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics maintainer-merge	112/81	Mathlib/Combinatorics/SimpleGraph/Acyclic.lean,Mathlib/Combinatorics/SimpleGraph/Paths.lean,Mathlib/Combinatorics/SimpleGraph/Walk/Basic.lean,Mathlib/Combinatorics/SimpleGraph/Walk/Decomp.lean,Mathlib/Combinatorics/SimpleGraph/Walk/Operations.lean	5	4	['YaelDillies', 'github-actions']	YaelDillies assignee:YaelDillies	0-48148 13 hours ago	0-55062 15 hours ago	39-84178 39 days
39218	SnirBroshi author:SnirBroshi	feat(Combinatorics/SimpleGraph/Walk): make `p.Nil` the simpNF of `p = nil` and `p.length = 0`	These are equivalent, and `p.Nil` works even when the endpoints of the walk aren't defeq. [#graph theory > Deprecate `p = nil` in favor of `p.Nil`?](https://leanprover.zulipchat.com/#narrow/channel/252551-graph-theory/topic/Deprecate.20.60p.20.3D.20nil.60.20in.20favor.20of.20.60p.2ENil.60.3F/with/538017334) The main event is `Walk/Basic.lean`: - Swapped sides of `nil_iff_eq_nil` to create `eq_nil_iff_nil`, tagged `@[simp]` and deprecated the original - Changed the RHS of `length_eq_zero_iff` from `p = nil` to `p.Nil`, and generalized to non-closed walks - Deprecated `nil_iff_length_eq` which is the symmetric iff - Added `Nil.length_eq_zero` alias - Untagged `exists_length_eq_zero_iff` with `@[simp]` and added `exists_nil_iff` to replace it The rest is fixing everything that broke (or uses of now-deprecated lemmas), and: - [`Walk/Maps`] Added `nil_map_iff` to replace `map_eq_nil_iff` which is the same but with `.Nil` instead of `= nil` - [`Walk/Decomp`] Added `nil_rotate` to replace `rotate_eq_nil` which is the same but with `.Nil` instead of `= nil` --- Also renamed `set_walk_*` in `Counting.lean` to follow the naming convention. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-combinatorics maintainer-merge	70/54	Mathlib/Combinatorics/SimpleGraph/Acyclic.lean,Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean,Mathlib/Combinatorics/SimpleGraph/Metric.lean,Mathlib/Combinatorics/SimpleGraph/Paths.lean,Mathlib/Combinatorics/SimpleGraph/Walk/Basic.lean,Mathlib/Combinatorics/SimpleGraph/Walk/Counting.lean,Mathlib/Combinatorics/SimpleGraph/Walk/Decomp.lean,Mathlib/Combinatorics/SimpleGraph/Walk/Maps.lean,Mathlib/Combinatorics/SimpleGraph/Walk/Operations.lean,Mathlib/Combinatorics/SimpleGraph/Walk/Traversal.lean	10	10	['SnirBroshi', 'YaelDillies', 'github-actions']	YaelDillies assignee:YaelDillies	0-24118 6 hours ago	0-57301 15 hours ago	1-6198 1 day
39201	b-mehta author:b-mehta	chore(SpecificGroups/Alternating/Simple): remove a convert	As mentioned here https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/support.20of.20permutations.20on.20Type.20instead.20of.20Fintype/with/593547821 I misdiagnosed the issue in that thread, and this PR only fixes one of the issues. The "issue" in this case was that the lemma `cycleType_ofSubtype` contains a non-variable instance of `Fintype (Subtype p)`, which means that when applying the lemma, the "wrong" instance could be picked. The correct pattern is that if a lemma requires `Fintype _`, then it should be stated explicitly in the type, even if that instance is derivable from other hypotheses. (An existing example is https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Fintype/Sets.html#Set.toFinset_union). --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-group-theory maintainer-merge	5/10	Mathlib/GroupTheory/Perm/Cycle/Type.lean,Mathlib/GroupTheory/SpecificGroups/Alternating/Simple.lean	2	10	['AntoineChambert-Loir', 'adomani', 'b-mehta', 'github-actions', 'tb65536']	tb65536 assignee:tb65536	0-16834 4 hours ago	0-53009 14 hours ago	1-7327 1 day
39019	urkud author:urkud	chore(*): reduce defeq abuse of `Set α = α → Prop`	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	tech debt maintainer-merge	17/16	Mathlib/Analysis/Complex/CoveringMap.lean,Mathlib/Analysis/Normed/Group/FunctionSeries.lean,Mathlib/Data/Nat/Order/Lemmas.lean,Mathlib/NumberTheory/EulerProduct/ExpLog.lean,Mathlib/NumberTheory/NumberField/Ideal/Asymptotics.lean,Mathlib/NumberTheory/NumberField/Ideal/KummerDedekind.lean,Mathlib/Topology/Algebra/InfiniteSum/Group.lean,Mathlib/Topology/FiberBundle/Basic.lean	8	5	['JovanGerb', 'github-actions', 'urkud']	JovanGerb assignee:JovanGerb	0-15239 4 hours ago	1-49210 1 day ago	5-74877 5 days
39276	JovanGerb author:JovanGerb	chore(Analysis/Asymptotics/Defs): add missing `@[refl]` tags	`gcongr`/`grw` use `rfl` to close reflexive subgoals, so we need these `@[refl]` tags. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-analysis easy maintainer-merge	2/0	Mathlib/Analysis/Asymptotics/Defs.lean	1	2	['github-actions', 'grunweg']	nobody	0-15096 4 hours ago	0-17224 4 hours ago	0-16953 4 hours
36840	SnirBroshi author:SnirBroshi	feat(SetTheory/Ordinal/Arithmetic): a few ordinal division lemmas	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-set-theory maintainer-merge	27/9	Mathlib/SetTheory/Ordinal/Arithmetic.lean	1	9	['SnirBroshi', 'YaelDillies', 'github-actions', 'vihdzp']	nobody	0-7108 1 hour ago	0-14602 3 hours ago	39-34818 39 days
39262	Paul-Lez author:Paul-Lez	chore(Algebra/Ring/CharZero): document `scoped simp` design choice	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra maintainer-merge label:t-algebra$	1/0	Mathlib/Algebra/Ring/CharZero.lean	1	6	['Paul-Lez', 'YaelDillies', 'github-actions']	nobody	0-6989 1 hour ago	0-11945 3 hours ago	0-11674 3 hours
38555	SnirBroshi author:SnirBroshi	feat(Order/Hom/Basic): `OrderEmbedding.id` and `OrderEmbedding.comp`	Define `OrderEmbedding.id` and `OrderEmbedding.comp`, and add missing associativity lemmas for `OrderHom` and `OrderIso`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-order maintainer-merge	53/1	Mathlib/Order/Hom/Basic.lean	1	12	['SnirBroshi', 'YaelDillies', 'github-actions']	nobody	0-6838 1 hour ago	0-19235 5 hours ago	10-41597 10 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	FR-vdash-bot author:FR-vdash-bot	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	538-63832 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	372-27109 1 year 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	312-7458 10 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	312-6296 10 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	252-21941 8 months ago	260-59495 260 days ago	0-19244 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	208-85551 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	181-10025 6 months ago	220-75091 220 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	176-27157 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	175-43398 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	174-80566 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	174-52432 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 awaiting-author	629/0	Mathlib.lean,Mathlib/Data/QuotType.lean,MathlibTest/QuotType.lean	3	22	['SnirBroshi', 'YaelDillies', 'astrainfinita', 'dagurtomas', 'github-actions', 'mathlib4-merge-conflict-bot', 'plp127', 'vihdzp']	nobody	153-34278 5 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	126-2591 4 months ago	126-49324 126 days ago	5-72484 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 awaiting-author label:t-algebra$	4/0	Mathlib/Algebra/Order/Group/Defs.lean	1	13	['Garmelon', 'Hagb', 'Vierkantor', 'artie2000', 'dagurtomas', 'github-actions', 'leanprover-radar']	eric-wieser assignee:eric-wieser	110-51426 3 months ago	110-51426 110 days ago	40-39215 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 awaiting-author	531/0	Mathlib.lean,Mathlib/Combinatorics/Enumerative/Partition/EulerComb.lean	2	7	['chiyunhsu', 'dagurtomas', 'github-actions', 'tb65536', 'vihdzp']	b-mehta assignee:b-mehta	103-56244 3 months ago	103-56244 103 days ago	42-20793 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 awaiting-author	4/0	Mathlib/MeasureTheory/Constructions/Polish/Basic.lean	1	10	['ADedecker', 'LTolDe', 'dagurtomas', 'dupuisf', 'github-actions', 'jcommelin']	PatrickMassot assignee:PatrickMassot	100-68654 3 months ago	126-52786 126 days ago	11-7478 11 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	83-79428 2 months ago	256-75746 256 days ago	51-56273 51 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	81-50047 2 months ago	unknown	unknown
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	81-28561 2 months ago	unknown	unknown
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	75-73800 2 months 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	75-73784 2 months 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	75-7413 2 months ago	339-36712 339 days ago	0-37135 10 hours
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	73-45854 2 months ago	22-45829 22 days ago	71-51176 71 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	70-76014 2 months ago	166-79354 166 days ago	35-80039 35 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	50-83969 1 month ago	53-70709 53 days ago	0-10819 3 hours
38546	yhx-12243 author:yhx-12243	fix: universe issue in injective module	Change the definition of ```lean class Module.Injective : Prop where out : ∀ ⦃X Y : Type v⦄ [AddCommGroup X] [AddCommGroup Y] [Module R X] [Module R Y] (f : X →ₗ[R] Y) (_ : Function.Injective f) (g : X →ₗ[R] Q), ∃ h : Y →ₗ[R] Q, ∀ x, h (f x) = g x ``` into ```lean class Module.Injective : Prop where out : ∀ ⦃X Y : Type u⦄ [AddCommGroup X] [AddCommGroup Y] [Module R X] [Module R Y] (f : X →ₗ[R] Y) (_ : Function.Injective f) (g : X →ₗ[R] Q), ∃ h : Y →ₗ[R] Q, ∀ x, h (f x) = g x ``` to make it agree with `Module.Baer` and real mathematical definition, without universe issues. Since the criterion `Module.Flat` also uses `Type u` on testing modules. See discussions in https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Universe.20issue.20about.20injective.20module . --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra new-contributor awaiting-zulip label:t-algebra$	57/43	Mathlib/Algebra/Category/ModuleCat/Injective.lean,Mathlib/Algebra/Category/ModuleCat/Ulift.lean,Mathlib/Algebra/Module/Injective.lean,Mathlib/RepresentationTheory/FinGroupCharZero.lean,Mathlib/RingTheory/Flat/Tensor.lean,Mathlib/RingTheory/LocalProperties/Injective.lean	6	5	['github-actions', 'grunweg', 'mathlib-bors', 'wwylele']	nobody	16-32518 16 days ago	16-32529 16 days ago	0-24433 6 hours
37346	euprunin author:euprunin	chore: golf using `grind`	The goal of this PR is to decrease the number of times lemmas are called explicitly. Any decrease in compilation time is a welcome side effect, although it is not a primary objective. Trace profiling results (differences <30 ms considered measurement noise): * `✅️ SimpleGraph.Walk.IsPath.getVert_injOn`: unchanged 🎉 * `✅️ SimpleGraph.Walk.length_bypass_le`: unchanged 🎉 * `✅️ Rat.floor_intCast_div_natCast`: unchanged 🎉 * `✅️ InnerProductGeometry.norm_eq_of_angle_sub_eq_angle_sub_rev_of_angle_ne_pi`: unchanged 🎉 * `✅️ padicNorm.zero_of_padicNorm_eq_zero`: unchanged 🎉 Profiled using `set_option trace.profiler true in`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	maintainer-merge awaiting-zulip	7/45	Mathlib/Combinatorics/SimpleGraph/Paths.lean,Mathlib/Data/Rat/Floor.lean,Mathlib/Geometry/Euclidean/Triangle.lean,Mathlib/NumberTheory/Padics/PadicNorm.lean	4	22	['FernandoChu', 'bryangingechen', 'chenson2018', 'euprunin', 'faenuccio', 'github-actions', 'grunweg']	nobody	13-64742 13 days ago	13-64773 13 days ago	30-45859 30 days
39027	fpvandoorn author:fpvandoorn	feat: delaborators for inequalities in big operators	`∏ i < n, f i` was already accepted as valid syntax, but this PR now also prints appropriate sums/products using this notation. --- [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/missing.20delaborator.20for.20finsum) [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra t-meta awaiting-zulip label:t-algebra$	132/49	Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean,MathlibTest/BigOps.lean	2	1	['github-actions']	nobody	5-59555 5 days ago	5-59861 5 days ago	0-7955 2 hours
39026	fpvandoorn author:fpvandoorn	feat: add assume tactic	Teaching tactic: `assume p, q, r` is short for `intro (_ : p) (_ : q) (_ : r)`. --- [Zulip thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Assume.20tactic/with/593477478) [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	awaiting-zulip t-meta awaiting-author	123/0	Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/Assume.lean,MathlibTest/Assume.lean	4	5	['fpvandoorn', 'github-actions', 'joneugster']	joneugster assignee:joneugster	4-64289 4 days 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 WIP label:t-algebra$	300/2	Mathlib.lean,Mathlib/LinearAlgebra/PiTensorProduct.lean,Mathlib/LinearAlgebra/PiTensorProduct/Set.lean	3	31	['PrParadoxy', 'dagurtomas', 'eric-wieser', 'github-actions', 'goliath-klein', 'leanprover-radar', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot']	nobody	1-35029 1 day ago	141-45751 141 days ago	10-64694 10 days
39233	linesthatinterlace author:linesthatinterlace	feat: `Pi.map` rename to `Function.map`	This PR renames `Pi.map` to `Function.map` and makes the changes necessary to support this. In particular this means that Mathlib.Logic.Function.Defs now only contains the Function namespace. Zulip thread: [#PR reviews > #39233 - rename Pi.map to Function.map @ 💬](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2339233.20-.20rename.20Pi.2Emap.20to.20Function.2Emap/near/594605689) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	awaiting-zulip	131/122	Mathlib/Algebra/Category/Grp/AB.lean,Mathlib/Algebra/Notation/Pi/Defs.lean,Mathlib/Algebra/Order/Antidiag/Nat.lean,Mathlib/Algebra/Regular/Pi.lean,Mathlib/Analysis/InnerProductSpace/Coalgebra.lean,Mathlib/Analysis/SpecialFunctions/PolarCoord.lean,Mathlib/Condensed/Discrete/LocallyConstant.lean,Mathlib/Control/Bifunctor.lean,Mathlib/Data/Finset/Powerset.lean,Mathlib/Data/Prod/Basic.lean,Mathlib/Data/Set/Prod.lean,Mathlib/Dynamics/Ergodic/MeasurePreserving.lean,Mathlib/Dynamics/PeriodicPts/Defs.lean,Mathlib/Dynamics/PeriodicPts/Lemmas.lean,Mathlib/Dynamics/TopologicalEntropy/Semiconj.lean,Mathlib/FieldTheory/Perfect.lean,Mathlib/Geometry/Manifold/IsManifold/Basic.lean,Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean,Mathlib/GroupTheory/MonoidLocalization/Lemmas.lean,Mathlib/LinearAlgebra/Multilinear/Basis.lean,Mathlib/LinearAlgebra/Pi.lean,Mathlib/Logic/Equiv/Basic.lean,Mathlib/Logic/Equiv/PartialEquiv.lean,Mathlib/Logic/Function/Basic.lean,Mathlib/Logic/Function/Defs.lean,Mathlib/Logic/Function/Iterate.lean,Mathlib/Order/Filter/Cofinite.lean,Mathlib/Order/Filter/Pi.lean,Mathlib/RingTheory/Coalgebra/Basic.lean,Mathlib/Topology/Algebra/FilterBasis.lean,Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean,Mathlib/Topology/Algebra/RestrictedProduct/TopologicalSpace.lean,Mathlib/Topology/Constructions.lean,Mathlib/Topology/Maps/Basic.lean,Mathlib/Topology/MetricSpace/HausdorffAlexandroff.lean,Mathlib/Topology/MetricSpace/Isometry.lean,Mathlib/Topology/NhdsWithin.lean	37	1	['github-actions']	nobody	0-51864 14 hours ago	0-51865 14 hours ago	0-701 11 minutes

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

Number	Author	Title	Description	Labels	+/-	Modified files (first 100)	📝	💬	All users who commented or reviewed	Assignee(s)	Updated	Last status change	total time in review
39150	wwylele author:wwylele	chore(Algebra/LinearRecurrence): remove a defeq abuse	The previous code abuses defeq between `Subtype E.IsSolution` (coming from `← Subtype.mk.injEq` rewrite) and `Subtype (· ∈ E.solSpace)` (coming from coercing submodule). --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra tech debt easy label:t-algebra$	2/2	Mathlib/Algebra/LinearRecurrence.lean	1	1	['github-actions']	nobody	2-36476 2 days ago	2-35687 2 days ago	2-35416 2 days
39152	wwylele author:wwylele	chore(Algebra/BigOperators): remove a defeq abuse	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra tech debt easy label:t-algebra$	1/2	Mathlib/Algebra/BigOperators/Ring/Finset.lean	1	1	['github-actions']	nobody	2-36027 2 days ago	2-34392 2 days ago	2-34121 2 days
38990	Vierkantor author:Vierkantor	chore(Algebra/DirectSum): workaround for `backward.inferInstanceAs`	This PR works around a `backward.inferInstanceAs` compatibility flag introduced by identifying `DirectSum` with `DFinsupp` in our definitions. We introduce a new dsimp lemma `funLike_eq` that transfers the `FunLike` instances, and now we can use `DirectSum`'s `FunLike` instance, instead of the custom `CoeFun` instance. I unsqueezed a few `simp`s, which all ran pretty much instant on my machine so it shouldn't cause much slowdown. Also we fix two porting notes. This is not a great approach, but it seems the least painful for the short term. The alternative would be to strictly enforce the defeq barrier between `DirectSum` and `DFinsupp`, which would mean a substantial rewrite of this corner of Mathlib. We can't make `DirectSum` an `@[implicit_reducible]`, because we need different multiplication on it than `DFinsupp` has. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra tech debt t-ring-theory label:t-algebra$	36/38	Mathlib/Algebra/DirectSum/Basic.lean,Mathlib/Algebra/DirectSum/Internal.lean,Mathlib/Algebra/DirectSum/Ring.lean,Mathlib/Algebra/Lie/DirectSum.lean,Mathlib/Algebra/Order/Module/HahnEmbedding.lean,Mathlib/Analysis/InnerProductSpace/Projection/FiniteDimensional.lean,Mathlib/Analysis/InnerProductSpace/Subspace.lean,Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean,Mathlib/RingTheory/Spectrum/Prime/RingHom.lean	9	2	['JovanGerb', 'github-actions']	joneugster assignee:joneugster	1-17163 1 day ago	6-72780 6 days ago	6-72509 6 days
39011	Vierkantor author:Vierkantor	chore(Algebra/Polynomial/Module): workaround for backward.inferInstanceAs	This PR, like #38990, works around a `backward.inferInstanceAs` compatibility flag introduced by identifying `PolynomialModule` with `Finsupp` in our definitions. We introduce a new dsimp lemma `funLike_eq` that transfers the `FunLike` instances, and now we can use `PolynomialModule`'s `FunLike` instance, instead of the custom `CoeFun` instance. This is not a great approach, but it seems the least painful for the short term. The alternative would be to strictly enforce the defeq barrier between `PolynomialModule` and `Finsupp`, which would mean a substantial rewrite of this corner of Mathlib. We can't make `PolynomialModule` an `@[implicit_reducible]`, because we need different multiplication on it than `Finsupp` has. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	t-algebra tech debt label:t-algebra$	8/5	Mathlib/Algebra/Polynomial/Module/Basic.lean	1	1	['github-actions']	jcommelin assignee:jcommelin	1-17158 1 day ago	6-45172 6 days ago	6-44901 6 days
38957	wwylele author:wwylele	chore(GroupTheory/DivisibleHull): remove `backward.privateInPublic`	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	tech debt t-group-theory	12/19	Mathlib/GroupTheory/DivisibleHull.lean	1	7	['github-actions', 'grunweg', 'jcommelin', 'wwylele']	jcommelin assignee:jcommelin	0-25584 7 hours ago	0-24958 6 hours ago	7-33037 7 days
39019	urkud author:urkud	chore(*): reduce defeq abuse of `Set α = α → Prop`	--- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)	tech debt maintainer-merge	17/16	Mathlib/Analysis/Complex/CoveringMap.lean,Mathlib/Analysis/Normed/Group/FunctionSeries.lean,Mathlib/Data/Nat/Order/Lemmas.lean,Mathlib/NumberTheory/EulerProduct/ExpLog.lean,Mathlib/NumberTheory/NumberField/Ideal/Asymptotics.lean,Mathlib/NumberTheory/NumberField/Ideal/KummerDedekind.lean,Mathlib/Topology/Algebra/InfiniteSum/Group.lean,Mathlib/Topology/FiberBundle/Basic.lean	8	5	['JovanGerb', 'github-actions', 'urkud']	JovanGerb assignee:JovanGerb	0-15239 4 hours ago	1-49210 1 day ago	5-74877 5 days