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.

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 08, 2026 at 15:43 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
38758 TBUGTB
author:TBUGTB
 feat(LinearAlgebra/ConvexSpace): StdSimplex bind operation Define the monadic bind operation for StdSimplex and add basic API lemmas. This operation is needed for formalising the Komlós lemma used in the construction of Stochastic Integrals (cf. [this PR](https://github.com/RemyDegenne/brownian-motion/pull/399) in the brownian-motion project). - [ ] depends on: #37592 t-algebra new-contributor brownian ready-to-merge blocked-by-other-PR
label:t-algebra$
 40/0 Mathlib/LinearAlgebra/ConvexSpace.lean 1 18 ['EtienneC30', 'RemyDegenne', 'TBUGTB', 'YaelDillies', 'github-actions', 'mathlib-bors', 'mathlib-dependent-issues'] nobody
6-19461
6 days ago
unknown
unknown

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
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
30-34440
1 month ago
unknown
unknown
37053 artie2000
author:artie2000
 refactor(Analysis/Convex/Cone): use `PointedCone` in Riesz extension theorem Change the statement of the Riesz extension theorem to take a `PointedCone` rather than a `ConvexCone`. This PR is part of a series replacing `ConvexCone` with `PointedCone`. https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Replacing.20.60ConvexCone.60.20with.20.60PointedCone.60/near/581184307 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-convex-geometry maintainer-merge 15/12 Mathlib/Analysis/Convex/Cone/Extension.lean,Mathlib/Geometry/Convex/Cone/Pointed.lean 2 8 ['YaelDillies', 'artie2000', 'github-actions', 'mathlib-merge-conflicts', 'ocfnash'] nobody
24-7982
24 days ago
unknown
unknown
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
22-14034
22 days ago
unknown
unknown
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 36/10 Mathlib/Combinatorics/SimpleGraph/Matching.lean,Mathlib/Combinatorics/SimpleGraph/Subgraph.lean 2 13 ['SnirBroshi', 'YaelDillies', 'github-actions', 'mathlib-merge-conflicts'] nobody
14-76413
14 days ago
unknown
unknown
38093 mortarsanjaya
author:mortarsanjaya
 feat(Algebra/Order/Ring/Unbundled/Basic): add a generalization of `two_mul_le_add_of_sq_eq_mul` The equality `r^2 = a * b` in the hypothesis can be weakened to `r^2 ≤ a * b`. The implementation requires adding an appropriate `ZeroLEOneClass` instance. --- [![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$
 16/7 Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean,Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean 2 13 ['github-actions', 'leanprover-radar', 'mortarsanjaya', 'themathqueen'] themathqueen
assignee:themathqueen
11-75287
11 days ago
unknown
unknown
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 45/14 Mathlib/Combinatorics/SimpleGraph/Clique.lean,Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean,Mathlib/Data/Set/Pairwise/Basic.lean 3 13 ['SnirBroshi', 'YaelDillies', 'github-actions'] nobody
9-32223
9 days ago
unknown
unknown
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
9-13282
9 days ago
unknown
unknown
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
9-9045
9 days ago
unknown
unknown
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
8-56018
8 days ago
unknown
unknown
38768 yuanyi-350
author:yuanyi-350
 chore(Condensed/Light/Epi): remove an erw Removes an `erw` that is now handled by `simp`. Extracted from #38415 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) codex t-condensed LLM-generated maintainer-merge 2/8 Mathlib/Condensed/Light/Epi.lean 1 3 ['dagurtomas', 'github-actions'] nobody
8-550
8 days ago
unknown
unknown
38662 joelriou
author:joelriou
 feat(AlgebraicTopology/SimplicialSet): faces of the boundary --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebraic-topology maintainer-merge 67/0 Mathlib/AlgebraicTopology/SimplicialSet/Boundary.lean 1 3 ['dagurtomas', 'github-actions'] dagurtomas
assignee:dagurtomas
7-84184
7 days ago
unknown
unknown
38314 pedroscortes
author:pedroscortes
 feat(CategoryTheory/Monoidal): tensorμ_braid_swap and tensor-product IsCommComonObj ## Summary Two symmetric-monoidal coherence results: 1. `MonoidalCategory.tensorμ_braid_swap` (in `Monoidal/Braided/Basic.lean`) — canonical rearrangement `tensorμ A A Y Y` intertwines the braiding on `A ⊗ Y` with the pair of braidings on `A` and `Y`. Sibling of `CategoryTheory.MonObj.mul_braiding`. 2. Tensor-product instance for `IsCommComonObj` (in `Monoidal/CommComon_.lean`): if `A, B` carry commutative comonoid structures in a symmetric monoidal category, so does `A ⊗ B`. Fills a gap alongside the existing `instCommComonObjUnit` and `instIsCommComonObjOfCartesian`. ## Downstream consumer The `IsCommComonObj` tensor-product instance is load-bearing for an external library (markovcat, formalising Fritz–Klingler Markov categories). t-category-theory new-contributor maintainer-merge 15/0 Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean,Mathlib/CategoryTheory/Monoidal/CommComon_.lean 2 19 ['dagurtomas', 'github-actions', 'joelriou', 'pedroscortes', 'robin-carlier'] riccardobrasca
assignee:riccardobrasca
7-78596
7 days ago
unknown
unknown
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 ((_ : Set _) ⊆ _)]`. This is because `simp_rw`, unlike `rw`, fully elaborates the rewrite rules before using them. A linter warns you whever there is such an ambiguity. 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 364/0 Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/SetNotationForOrder.lean,MathlibTest/SetNotationForOrder.lean 4 51 ['JovanGerb', 'Vierkantor', 'github-actions', 'thorimur'] alexjbest and dwrensha
assignee:dwrensha assignee:alexjbest
7-51814
7 days ago
unknown
unknown
38597 kim-em
author:kim-em
 chore: backport robustness changes from bump/nightly-2026-04-27 See [#nightly-testing > nightly#213 adaptations for nightly-2026-04-27 @ 💬](https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/nightly.23213.20adaptations.20for.20nightly-2026-04-27/near/591262169). t-category-theory maintainer-merge 91/26 Mathlib/AlgebraicTopology/SimplexCategory/Augmented/Monoidal.lean,Mathlib/CategoryTheory/Bicategory/Coherence.lean,Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean,Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean,Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean,Mathlib/CategoryTheory/Sites/DenseSubsite/OneHypercoverDense.lean,Mathlib/CategoryTheory/Sites/Hypercover/One.lean 7 8 ['github-actions', 'kim-em', 'robin-carlier'] joelriou
assignee:joelriou
7-51810
7 days ago
unknown
unknown
37675 vihdzp
author:vihdzp
 feat: `Order.cof Ordinal = univ` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-set-theory t-order maintainer-merge 11/0 Mathlib/SetTheory/Cardinal/Cofinality.lean 1 4 ['YaelDillies', 'github-actions', 'vihdzp'] nobody
7-24288
7 days ago
unknown
unknown
37171 SnirBroshi
author:SnirBroshi
 chore(Data/Int/Init): generalize `le_induction` from `Prop` to `Sort*` + def lemmas --- - Generallise `le_induction` from `Prop` to `Sort*` and rename to `leInduction` - Add a few lemmas - Simplify proofs using `lia` - Move `inductionOn'_add_one` [Zulip 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Add.20note.20to.20help.20search.20similar.20thms/near/535331432) [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data large-import maintainer-merge 56/48 Mathlib/Data/Int/Basic.lean,Mathlib/Data/Int/Init.lean,Mathlib/GroupTheory/CoprodI.lean 3 9 ['SnirBroshi', 'github-actions', 'joneugster', 'mathlib-merge-conflicts', 'plp127'] joneugster
assignee:joneugster
7-21366
7 days ago
unknown
unknown
34015 erdOne
author:erdOne
 feat(AlgebraicGeometry): category of schemes affine over a base --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebraic-geometry maintainer-merge 522/11 Mathlib.lean,Mathlib/AlgebraicGeometry/AffineOver.lean,Mathlib/AlgebraicGeometry/Limits.lean,Mathlib/AlgebraicGeometry/Morphisms/Affine.lean,Mathlib/AlgebraicGeometry/OpenImmersion.lean,Mathlib/AlgebraicGeometry/RelativeGluing.lean,Mathlib/AlgebraicGeometry/Sites/SmallAffineZariski.lean,Mathlib/CategoryTheory/Sites/Hypercover/Subcanonical.lean 8 50 ['chrisflav', 'dagurtomas', 'erdOne', 'github-actions', 'mathlib-merge-conflicts', 'mathlib4-merge-conflict-bot'] chrisflav
assignee:chrisflav
7-3418
7 days ago
unknown
unknown
38665 joelriou
author:joelriou
 feat(AlgebraicTopology/SimplicialSet): characterization of Kan complexes --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebraic-topology maintainer-merge 92/2 Mathlib/AlgebraicTopology/SimplicialSet/CategoryWithFibrations.lean,Mathlib/AlgebraicTopology/SimplicialSet/KanComplex.lean 2 4 ['dagurtomas', 'github-actions', 'joelriou'] robin-carlier
assignee:robin-carlier
6-52274
6 days ago
unknown
unknown
38827 eric-wieser
author:eric-wieser
 feat: `IsEquiv` is equivalent to `Equivalence` Ideally we would have only one spelling of this, but in the meantime we should at least have a lemma to transport between the two spellings. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) easy t-logic t-order maintainer-merge 10/0 Mathlib/Order/Defs/Unbundled.lean 1 4 ['SnirBroshi', 'YaelDillies', 'github-actions'] nobody
6-34516
6 days ago
unknown
unknown
37831 EtienneC30
author:EtienneC30
 feat: the cardinal of a finset is an ite sum over a bigger finset If `s ⊆ t` then `s.card = ∑ i ∈ t, if i ∈ s then 1 else 0`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data t-algebra maintainer-merge
label:t-algebra$
 9/2 Mathlib/Algebra/BigOperators/Ring/Finset.lean,Mathlib/Data/Finset/BooleanAlgebra.lean,Mathlib/Data/Finset/Filter.lean 3 7 ['EtienneC30', 'github-actions', 'robin-carlier'] nobody
6-30083
6 days ago
unknown
unknown
38794 YaelDillies
author:YaelDillies
 feat(Algebra/Order): stronger positivity criterion for `expect` From AddCombi --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebra maintainer-merge
label:t-algebra$
 9/10 Mathlib/Algebra/Order/BigOperators/Expect.lean 1 6 ['YaelDillies', 'b-mehta', 'eric-wieser', 'github-actions', 'grunweg', 'mathlib-merge-conflicts'] nobody
5-31381
5 days ago
unknown
unknown
38854 SnirBroshi
author:SnirBroshi
 feat(Order/ConditionallyCompleteLattice/Indexed): `ciSup_mono'` for `ConditionallyCompleteLattice` Usually a primed version of a sup/inf theorem is the like the unprimed version but for `ConditionallyCompleteLinearOrderBot` which can remove `Nonempty` assumptions. `ciSup_mono'` is different from its unprimed version and it's missing `ConditionallyCompleteLattice` versions. We add these and rename `ciSup_mono'` to `ciSup_mono_of_forall_exists'`. --- I think we should also rename the `CompleteLattice` theorems `iSup_mono'`/`iInf_mono'`/`iSup₂_mono'`/`iInf₂_mono'` to not have a prime, but that'll cause a big diff so maybe later. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-order maintainer-merge 16/6 Mathlib/LinearAlgebra/Dimension/Basic.lean,Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean,Mathlib/SetTheory/Cardinal/Basic.lean 3 2 ['YaelDillies', 'github-actions'] nobody
5-21933
5 days ago
unknown
unknown
38858 SnirBroshi
author:SnirBroshi
 feat(Order/ConditionallyCompleteLattice/Basic): `ConditionallyCompleteLinearOrderBot` versions of `csSup_union`/`csSup_inter_le`/`csSup_insert` `ConditionallyCompleteLinearOrderBot` lets us drop all the `Set.Nonempty` assumptions. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-order maintainer-merge 23/0 Mathlib/Order/ConditionallyCompleteLattice/Basic.lean 1 2 ['YaelDillies', 'github-actions'] nobody
5-21089
5 days ago
unknown
unknown
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
5-21036
5 days ago
unknown
unknown
38857 SnirBroshi
author:SnirBroshi
 feat(Order/ConditionallyCompleteLattice/Indexed): conditional versions of `iSup_exists`/`iSup_and` For `iSup_exists` we can only get `≤` in `ConditionallyCompleteLattice`, and equality in `ConditionallyCompleteLinearOrderBot`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-order maintainer-merge 24/0 Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean 1 3 ['YaelDillies', 'github-actions'] nobody
5-15336
5 days ago
unknown
unknown
38835 yuanyi-350
author:yuanyi-350
 refactor(NumberTheory): golf `Mathlib/NumberTheory/Zsqrtd/GaussianInt` - rewrites `normSq_le_normSq_of_re_le_of_im_le` to reduce to the squared-coordinate inequalities and finish with `nlinarith` Extracted from #38144 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) codex t-number-theory LLM-generated maintainer-merge 3/5 Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean 1 9 ['MichaelStollBayreuth', 'github-actions', 'yuanyi-350'] MichaelStollBayreuth
assignee:MichaelStollBayreuth
5-7301
5 days ago
unknown
unknown
38832 yuanyi-350
author:yuanyi-350
 refactor(NumberTheory): golf `Mathlib/NumberTheory/FrobeniusNumber` - rewrites `frobeniusNumber_pair` to use `Nat.exists_add_mul_eq_of_gcd_dvd_of_mul_pred_le` instead of constructing the witnesses via the Chinese remainder argument - closes the final witness equality by applying `succ_inj` to the resulting additive decomposition Extracted from #38144 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) codex t-number-theory LLM-generated maintainer-merge 3/12 Mathlib/NumberTheory/FrobeniusNumber.lean 1 3 ['YaelDillies', 'github-actions', 'yuanyi-350'] tb65536
assignee:tb65536
4-9613
4 days ago
unknown
unknown
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 201/0 Mathlib.lean,Mathlib/Topology/Algebra/Order/PiecewiseLinear.lean 2 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
3-76608
3 days ago
unknown
unknown
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
3-75127
3 days ago
unknown
unknown
37676 IvanRenison
author:IvanRenison
 feat(Data/Finset/Preimage): add lemmas about `Equiv.symm` --- `Finset` version of lemmas already existing for `Set`. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data maintainer-merge 8/0 Mathlib/Data/Finset/Preimage.lean 1 3 ['github-actions', 'robin-carlier'] joneugster
assignee:joneugster
3-52286
3 days ago
unknown
unknown
36913 joelriou
author:joelriou
 feat(CategoryTheory/Monoidal): Yoneda embedding of ring objects (This series of PR mostly builds on previous work by the Toric project.) --- - [x] depends on: #38366 - [x] depends on: #37587 - [x] depends on: #37167 - [x] depends on: #37265 - [x] depends on: #37263 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-category-theory maintainer-merge 84/0 Mathlib.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/Ring.lean 2 14 ['dagurtomas', 'github-actions', 'joelriou', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'robin-carlier'] robin-carlier
assignee:robin-carlier
3-31773
3 days ago
unknown
unknown
38954 joelriou
author:joelriou
 feat(AlgebraicTopology/DoldKan): the homotopy equivalence given by a splitting --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebraic-topology maintainer-merge 77/4 Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean,Mathlib/AlgebraicTopology/DoldKan/SplitSimplicialObject.lean 2 4 ['github-actions', 'joelriou', 'robin-carlier'] nobody
3-13507
3 days ago
unknown
unknown
37858 tb65536
author:tb65536
 feat(RingTheory/LocalRing/ResidueField/Fiber): `Ideal.Fiber` is a quotient of a localization This PR proves that `Ideal.Fiber` is a quotient of a localization. This is needed for #37130. --- - [x] depends on: #37380 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-ring-theory t-algebra maintainer-merge
label:t-algebra$
 16/0 Mathlib/RingTheory/LocalRing/ResidueField/Fiber.lean 1 4 ['github-actions', 'mariainesdff', 'mathlib-dependent-issues'] mariainesdff
assignee:mariainesdff
3-8146
3 days ago
unknown
unknown
38925 yuanyi-350
author:yuanyi-350
 chore(ModelTheory/ElementaryMaps): remove an erw - rewrites `map_boundedFormula` by avoiding the `iff_eq_eq` detour and using the restricted free-variable realization lemma directly - shortens `isElementary_of_exists` by replacing the `map_rel` `erw` with explicit `simp_rw` and `rw` Extracted from #38415 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) codex LLM-generated t-logic maintainer-merge 9/7 Mathlib/ModelTheory/ElementaryMaps.lean 1 3 ['github-actions', 'j-loreaux', 'loefflerd'] nobody
3-7776
3 days ago
unknown
unknown
38005 robin-carlier
author:robin-carlier
 chore(Algebra): remove simps projections for structures of bundled objects I noticed that currently, adding a `@[simps]` tag to a `ModuleCat`-valued definition will generate projections for the `isModule` fields. These projections are removed. Same in `BialgCat` and `HopfAlgCat`. --- I did not look very hard for all cases of this, but those three should be a starter. Renaming `carrier` to `coe` will break a few things, so I opted for keeping it like this for now, feel free to disagree, but this will make the diff bigger. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebra maintainer-merge
label:t-algebra$
 4/0 Mathlib/Algebra/Category/BialgCat/Basic.lean,Mathlib/Algebra/Category/HopfAlgCat/Basic.lean,Mathlib/Algebra/Category/ModuleCat/Basic.lean,Mathlib/Algebra/Category/ModuleCat/Semi.lean 4 5 ['dagurtomas', 'github-actions', 'leanprover-radar'] dagurtomas
assignee:dagurtomas
3-4518
3 days ago
unknown
unknown
38833 yuanyi-350
author:yuanyi-350
 refactor(NumberTheory): golf `Mathlib/NumberTheory/EllipticDivisibilitySequence` - rewrites `complEDS₂_mul_b` by evaluating the parity split directly with `simp_rw` and `split_ifs`, removing the separate `Int.negInduction` proof Extracted from #38144 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) codex t-number-theory LLM-generated maintainer-merge 3/8 Mathlib/NumberTheory/EllipticDivisibilitySequence.lean 1 3 ['github-actions', 'loefflerd', 'yuanyi-350'] loefflerd
assignee:loefflerd
3-3215
3 days ago
unknown
unknown
37869 mckoen
author:mckoen
 feat(AlgebraicTopology/Quasicategory): inner fibrations and inner anodyne morphisms Defines inner fibrations, inner anodyne morphisms, and immediate results. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebraic-topology maintainer-merge 220/0 Mathlib.lean,Mathlib/AlgebraicTopology/Quasicategory/Basic.lean,Mathlib/AlgebraicTopology/Quasicategory/InnerFibration.lean,Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Inner/Basic.lean 4 18 ['github-actions', 'joelriou', 'mckoen', 'robin-carlier'] nobody
2-74858
2 days ago
unknown
unknown
38414 chrisflav
author:chrisflav
 chore(RingTheory): move `IsLocalizedModule.Away` to the `Basic` file and use it everywhere --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-ring-theory maintainer-merge 42/48 Mathlib/Algebra/Module/FinitePresentation.lean,Mathlib/Algebra/Module/LocalizedModule/Away.lean,Mathlib/Algebra/Module/LocalizedModule/Basic.lean,Mathlib/AlgebraicGeometry/Modules/Tilde.lean,Mathlib/AlgebraicGeometry/StructureSheaf.lean,Mathlib/RingTheory/LocalProperties/Exactness.lean,Mathlib/RingTheory/LocalProperties/Submodule.lean,Mathlib/RingTheory/Localization/Finiteness.lean,Mathlib/RingTheory/Localization/Free.lean,Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean,Mathlib/RingTheory/Spectrum/Prime/Module.lean,Mathlib/RingTheory/Support.lean 12 8 ['chrisflav', 'dagurtomas', 'github-actions', 'grunweg', 'mathlib-merge-conflicts'] nobody
2-70383
2 days ago
unknown
unknown
37840 tb65536
author:tb65536
 chore(RingTheory/Localization/AtPrime/Basic): use `under` instead of `comap (algebraMap R S)` This PR switches over from `comap (algebraMap R S)` to `under`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-ring-theory t-algebra maintainer-merge awaiting-CI
label:t-algebra$
 172/149 Mathlib/AlgebraicGeometry/Noetherian.lean,Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean,Mathlib/RingTheory/DedekindDomain/Dvr.lean,Mathlib/RingTheory/Etale/QuasiFinite.lean,Mathlib/RingTheory/Frobenius.lean,Mathlib/RingTheory/Ideal/AssociatedPrime/Localization.lean,Mathlib/RingTheory/Ideal/GoingUp.lean,Mathlib/RingTheory/Ideal/Height.lean,Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean,Mathlib/RingTheory/Ideal/MinimalPrime/Localization.lean,Mathlib/RingTheory/Ideal/Over.lean,Mathlib/RingTheory/IntegralClosure/GoingDown.lean,Mathlib/RingTheory/Jacobson/Ring.lean,Mathlib/RingTheory/KrullDimension/Polynomial.lean,Mathlib/RingTheory/LocalProperties/Injective.lean,Mathlib/RingTheory/Localization/AtPrime/Basic.lean,Mathlib/RingTheory/Localization/AtPrime/Extension.lean,Mathlib/RingTheory/Localization/Ideal.lean,Mathlib/RingTheory/QuasiFinite/Basic.lean,Mathlib/RingTheory/Spectrum/Prime/Topology.lean 20 14 ['chrisflav', 'github-actions', 'mathlib-merge-conflicts', 'robin-carlier', 'tb65536'] chrisflav and erdOne
assignee:erdOne assignee:chrisflav
2-70246
2 days ago
unknown
unknown
38656 NoahW314
author:NoahW314
 feat(Data/Finsupp/Weight): add `Finsupp.degree_mapDomain` Generalize a result by removing an unnecessary hypothesis. Also simplifies the proof. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data maintainer-merge 9/8 Mathlib/Data/Finsupp/Weight.lean,Mathlib/Order/Filter/TendstoCofinite.lean 2 4 ['NoahW314', 'dagurtomas', 'github-actions'] nobody
2-66721
2 days ago
unknown
unknown
38971 homeowmorphism
author:homeowmorphism
 chore(FinitelyPresentedGroup): Use dot notation by default whenever possible and typo fix * Changing the usage of `IsNormalClosureFG N` to `N.IsNormalClosureFG` as the idiomatic use of the latter seems easier to read ("N is finitely generated under normal closure") and is in line with using dot notation for terms. * Fix a typo in the main definition docstring regarding the usage of `map`: it should be `.map` instead of `_map`. --- I used Copilot + Gemini Pro 3.1 to query about usage and took some of its suggestions. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-group-theory 7/7 Mathlib/GroupTheory/FinitelyPresentedGroup.lean 1 2 ['github-actions', 'tb65536'] tb65536
assignee:tb65536
2-52287
2 days ago
unknown
unknown
37355 Thmoas-Guan
author:Thmoas-Guan
 feat(RingTheory): refactor `smulShortComplex` Use `LinearMap.lsmul` for the `f` of `ModuleCat.smulShortComplex`, also providing new APIs for it. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-ring-theory maintainer-merge 18/21 Mathlib/RingTheory/Regular/Category.lean 1 21 ['Thmoas-Guan', 'chrisflav', 'github-actions', 'robin-carlier'] chrisflav
assignee:chrisflav
2-49833
2 days ago
unknown
unknown
38743 eric-wieser
author:eric-wieser
 feat: `Finite` instances for `Sym` We already have the `Fintype` instances. I take the liberty of moving these into namespaces in order to produce nicer auto-generated instance names. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data maintainer-merge 25/3 Mathlib/Data/Fintype/Vector.lean 1 3 ['YaelDillies', 'github-actions'] nobody
2-38712
2 days ago
unknown
unknown
38525 AntoineChambert-Loir
author:AntoineChambert-Loir
 feat(Tactic/Translate/ToAdditive.lean): add conGen/AddConGen to the to_additive tactic This PR adds the pair "conGen", "AddConGen" to the additive tactic and capitalizes the second of some pairs that should have been. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-meta maintainer-merge 11/10 Mathlib/Algebra/Exact.lean,Mathlib/GroupTheory/Congruence/Defs.lean,Mathlib/Tactic/Translate/ToAdditive.lean 3 15 ['AntoineChambert-Loir', 'JovanGerb', 'github-actions', 'mathlib-merge-conflicts', 'robin-carlier'] JovanGerb and dwrensha
assignee:dwrensha assignee:JovanGerb
2-17441
2 days ago
2-20137
2 days ago
12-27319
12 days
38949 YaelDillies
author:YaelDillies
 chore: untag duplicated `gcongr` lemmas Follow-up to #38793 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge 11/9 Mathlib/Algebra/Module/Submodule/Basic.lean,Mathlib/Algebra/Module/Submodule/RestrictScalars.lean,Mathlib/Algebra/Order/Ring/Ordering/Basic.lean,Mathlib/Analysis/SpecialFunctions/Sigmoid.lean,Mathlib/Data/Finset/Density.lean,Mathlib/RingTheory/Localization/Submodule.lean 6 3 ['JovanGerb', 'github-actions'] nobody
2-11391
2 days ago
2-11478
2 days ago
3-33868
3 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 75 ['SnirBroshi', 'YaelDillies', 'github-actions', 'jessealama', 'mathlib-dependent-issues', 'mathlib-merge-conflicts'] YaelDillies
assignee:YaelDillies
2-9142
2 days ago
2-20534
2 days ago
40-25585
40 days
38889 emlis42
author:emlis42
 chore(NumberTheory/Divisors): golf `Int.mem_divisorsAntidiag` This PR merges the case split and removes duplicated proofs in `Int.mem_divisorsAntidiag`. t-number-theory new-contributor maintainer-merge 7/36 Mathlib/NumberTheory/Divisors.lean 1 14 ['MichaelStollBayreuth', 'SnirBroshi', 'emlis42', 'github-actions'] MichaelStollBayreuth
assignee:MichaelStollBayreuth
2-6784
2 days ago
3-57788
3 days ago
4-14668
4 days
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 47/0 Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean 1 18 ['dagurtomas', 'github-actions', 'joelriou', 'michaellee94'] robin-carlier
assignee:robin-carlier
1-82432
1 day ago
1-82459
1 day ago
4-46878
4 days
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 maintainer-merge 53/26 Mathlib/SetTheory/Cardinal/Aleph.lean,Mathlib/SetTheory/Cardinal/Cofinality.lean,Mathlib/SetTheory/Cardinal/Order.lean,Mathlib/SetTheory/Cardinal/Regular.lean 4 4 ['YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'vihdzp'] alreadydone
assignee:alreadydone
1-60868
1 day ago
3-48782
3 days ago
35-15429
35 days
37545 vihdzp
author:vihdzp
 feat(SetTheory): ℵ_ univ = univ --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-set-theory maintainer-merge 73/7 Mathlib/SetTheory/Cardinal/Aleph.lean,Mathlib/SetTheory/Cardinal/Regular.lean 2 16 ['YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'mattdiamond', 'plp127', 'vihdzp'] nobody
1-60197
1 day ago
1-60233
1 day ago
35-77839
35 days
38846 YanYablonovskiy
author:YanYablonovskiy
 feat(Order): OrderType cardinality lemmas Adding some basic lemmas for the cardinality of an order type. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) new-contributor t-order large-import maintainer-merge 28/4 Mathlib/Order/Types/Arithmetic.lean 1 10 ['YaelDillies', 'YanYablonovskiy', 'github-actions', 'plp127', 'vihdzp', 'wwylele'] YaelDillies
assignee:YaelDillies
1-42825
1 day ago
5-55804
5 days ago
6-12712
6 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
1-40860
1 day ago
38-46814
38 days ago
38-46803
38 days
38907 YaelDillies
author:YaelDillies
 chore(Geometry): move `ConvexSpace` out of `LinearAlgebra` `ConvexSpace` is convex geometry, not linear algebra --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-convex-geometry file-removed maintainer-merge 6/7 Mathlib.lean,Mathlib/Analysis/Convex/MetricSpace.lean,Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean,Mathlib/Geometry/Convex/ConvexSpace/Defs.lean,Mathlib/Geometry/Convex/README.md 5 5 ['YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'themathqueen'] nobody
1-36840
1 day ago
1-36879
1 day ago
3-83475
3 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 329/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
1-11161
1 day ago
4-53126
4 days ago
64-61857
64 days
38370 FordUniver
author:FordUniver
 feat(Data/Finset/Powerset): add `filter_powersetCard_subset` Adds `Finset.filter_powersetCard_subset` and derives `Finset.card_filter_powersetCard_subset` from it. The hypothesis `s.card ≤ n` is necessary: without it, natural subtraction silently gives `Nat.choose k 0 = 1 ≠ 0`. Co-authored-by: Malte Jackisch --- We ran into this while formalizing Goodman's formula on triangle densities in graphs as part of an ongoing flag algebras project in Lean, and it seemed worth upstreaming. **Disclosure.** *This PR was developed with assistance from LLM code tools, used for Mathlib style alignment and proof compactness. The mathematical content and proof strategy originate from formalization work by Malte Jackisch (co-author) and myself; the final code has been reviewed and vouched for by both of us.* t-data new-contributor maintainer-merge 30/0 Mathlib/Data/Finset/Powerset.lean 1 20 ['FordUniver', 'YaelDillies', 'github-actions', 'mathlib-bors', 'wwylele'] YaelDillies
assignee:YaelDillies
1-9611
1 day ago
2-31907
2 days ago
15-8429
15 days
38963 linesthatinterlace
author:linesthatinterlace
 fix: rename `Pi.prod` to `Function.prod` Renames `Pi.prod` to `Function.prod` in order to allow for dot notation to work in the non-dependent case. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) large-import maintainer-merge 88/74 Archive/Sensitivity.lean,Mathlib/Algebra/Algebra/NonUnitalHom.lean,Mathlib/Algebra/Algebra/Prod.lean,Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Algebra/Exact.lean,Mathlib/Algebra/Group/Prod.lean,Mathlib/Algebra/Lie/Prod.lean,Mathlib/Algebra/MvPolynomial/Equiv.lean,Mathlib/Algebra/MvPolynomial/Eval.lean,Mathlib/Algebra/Notation/Pi/Defs.lean,Mathlib/Algebra/Star/StarAlgHom.lean,Mathlib/Combinatorics/Nullstellensatz.lean,Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean,Mathlib/LinearAlgebra/Dimension/DivisionRing.lean,Mathlib/LinearAlgebra/Goursat.lean,Mathlib/LinearAlgebra/Prod.lean,Mathlib/LinearAlgebra/QuadraticForm/Dual.lean,Mathlib/Logic/Function/Defs.lean,Mathlib/MeasureTheory/Integral/Prod.lean,Mathlib/MeasureTheory/Measure/Prod.lean,Mathlib/NumberTheory/Height/Basic.lean,Mathlib/SetTheory/Cardinal/Finite.lean,Mathlib/Topology/Algebra/ContinuousAffineMap.lean,Mathlib/Topology/Algebra/InfiniteSum/Basic.lean,Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean,Mathlib/Topology/Inseparable.lean,Mathlib/Topology/UniformSpace/LocallyUniformConvergence.lean 27 4 ['fpvandoorn', 'github-actions'] nobody
1-7141
1 day ago
2-86353
2 days ago
3-4904
3 days
38604 wwylele
author:wwylele
 chore(Algebra/Module): remove some `backward.privateInPublic` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebra tech debt maintainer-merge
label:t-algebra$
 14/30 Mathlib/Algebra/Module/GradedModule.lean,Mathlib/Algebra/Module/Submodule/Lattice.lean 2 7 ['dagurtomas', 'github-actions', 'wwylele'] dagurtomas
assignee:dagurtomas
1-3322
1 day ago
2-69117
2 days ago
10-42520
10 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
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
30-34440
1 month ago
unknown
unknown
37053 artie2000
author:artie2000
 refactor(Analysis/Convex/Cone): use `PointedCone` in Riesz extension theorem Change the statement of the Riesz extension theorem to take a `PointedCone` rather than a `ConvexCone`. This PR is part of a series replacing `ConvexCone` with `PointedCone`. https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Replacing.20.60ConvexCone.60.20with.20.60PointedCone.60/near/581184307 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-convex-geometry maintainer-merge 15/12 Mathlib/Analysis/Convex/Cone/Extension.lean,Mathlib/Geometry/Convex/Cone/Pointed.lean 2 8 ['YaelDillies', 'artie2000', 'github-actions', 'mathlib-merge-conflicts', 'ocfnash'] nobody
24-7982
24 days ago
unknown
unknown
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
22-14034
22 days ago
unknown
unknown
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 36/10 Mathlib/Combinatorics/SimpleGraph/Matching.lean,Mathlib/Combinatorics/SimpleGraph/Subgraph.lean 2 13 ['SnirBroshi', 'YaelDillies', 'github-actions', 'mathlib-merge-conflicts'] nobody
14-76413
14 days ago
unknown
unknown
38093 mortarsanjaya
author:mortarsanjaya
 feat(Algebra/Order/Ring/Unbundled/Basic): add a generalization of `two_mul_le_add_of_sq_eq_mul` The equality `r^2 = a * b` in the hypothesis can be weakened to `r^2 ≤ a * b`. The implementation requires adding an appropriate `ZeroLEOneClass` instance. --- [![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$
 16/7 Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean,Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean 2 13 ['github-actions', 'leanprover-radar', 'mortarsanjaya', 'themathqueen'] themathqueen
assignee:themathqueen
11-75287
11 days ago
unknown
unknown
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 45/14 Mathlib/Combinatorics/SimpleGraph/Clique.lean,Mathlib/Combinatorics/SimpleGraph/Coloring/VertexColoring.lean,Mathlib/Data/Set/Pairwise/Basic.lean 3 13 ['SnirBroshi', 'YaelDillies', 'github-actions'] nobody
9-32223
9 days ago
unknown
unknown
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
9-13282
9 days ago
unknown
unknown
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
9-9045
9 days ago
unknown
unknown
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
8-56018
8 days ago
unknown
unknown
38768 yuanyi-350
author:yuanyi-350
 chore(Condensed/Light/Epi): remove an erw Removes an `erw` that is now handled by `simp`. Extracted from #38415 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) codex t-condensed LLM-generated maintainer-merge 2/8 Mathlib/Condensed/Light/Epi.lean 1 3 ['dagurtomas', 'github-actions'] nobody
8-550
8 days ago
unknown
unknown
38662 joelriou
author:joelriou
 feat(AlgebraicTopology/SimplicialSet): faces of the boundary --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebraic-topology maintainer-merge 67/0 Mathlib/AlgebraicTopology/SimplicialSet/Boundary.lean 1 3 ['dagurtomas', 'github-actions'] dagurtomas
assignee:dagurtomas
7-84184
7 days ago
unknown
unknown
38314 pedroscortes
author:pedroscortes
 feat(CategoryTheory/Monoidal): tensorμ_braid_swap and tensor-product IsCommComonObj ## Summary Two symmetric-monoidal coherence results: 1. `MonoidalCategory.tensorμ_braid_swap` (in `Monoidal/Braided/Basic.lean`) — canonical rearrangement `tensorμ A A Y Y` intertwines the braiding on `A ⊗ Y` with the pair of braidings on `A` and `Y`. Sibling of `CategoryTheory.MonObj.mul_braiding`. 2. Tensor-product instance for `IsCommComonObj` (in `Monoidal/CommComon_.lean`): if `A, B` carry commutative comonoid structures in a symmetric monoidal category, so does `A ⊗ B`. Fills a gap alongside the existing `instCommComonObjUnit` and `instIsCommComonObjOfCartesian`. ## Downstream consumer The `IsCommComonObj` tensor-product instance is load-bearing for an external library (markovcat, formalising Fritz–Klingler Markov categories). t-category-theory new-contributor maintainer-merge 15/0 Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean,Mathlib/CategoryTheory/Monoidal/CommComon_.lean 2 19 ['dagurtomas', 'github-actions', 'joelriou', 'pedroscortes', 'robin-carlier'] riccardobrasca
assignee:riccardobrasca
7-78596
7 days ago
unknown
unknown
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 ((_ : Set _) ⊆ _)]`. This is because `simp_rw`, unlike `rw`, fully elaborates the rewrite rules before using them. A linter warns you whever there is such an ambiguity. 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 364/0 Mathlib.lean,Mathlib/Tactic.lean,Mathlib/Tactic/SetNotationForOrder.lean,MathlibTest/SetNotationForOrder.lean 4 51 ['JovanGerb', 'Vierkantor', 'github-actions', 'thorimur'] alexjbest and dwrensha
assignee:dwrensha assignee:alexjbest
7-51814
7 days ago
unknown
unknown
38597 kim-em
author:kim-em
 chore: backport robustness changes from bump/nightly-2026-04-27 See [#nightly-testing > nightly#213 adaptations for nightly-2026-04-27 @ 💬](https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/nightly.23213.20adaptations.20for.20nightly-2026-04-27/near/591262169). t-category-theory maintainer-merge 91/26 Mathlib/AlgebraicTopology/SimplexCategory/Augmented/Monoidal.lean,Mathlib/CategoryTheory/Bicategory/Coherence.lean,Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean,Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean,Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean,Mathlib/CategoryTheory/Sites/DenseSubsite/OneHypercoverDense.lean,Mathlib/CategoryTheory/Sites/Hypercover/One.lean 7 8 ['github-actions', 'kim-em', 'robin-carlier'] joelriou
assignee:joelriou
7-51810
7 days ago
unknown
unknown
37675 vihdzp
author:vihdzp
 feat: `Order.cof Ordinal = univ` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-set-theory t-order maintainer-merge 11/0 Mathlib/SetTheory/Cardinal/Cofinality.lean 1 4 ['YaelDillies', 'github-actions', 'vihdzp'] nobody
7-24288
7 days ago
unknown
unknown
37171 SnirBroshi
author:SnirBroshi
 chore(Data/Int/Init): generalize `le_induction` from `Prop` to `Sort*` + def lemmas --- - Generallise `le_induction` from `Prop` to `Sort*` and rename to `leInduction` - Add a few lemmas - Simplify proofs using `lia` - Move `inductionOn'_add_one` [Zulip 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Add.20note.20to.20help.20search.20similar.20thms/near/535331432) [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data large-import maintainer-merge 56/48 Mathlib/Data/Int/Basic.lean,Mathlib/Data/Int/Init.lean,Mathlib/GroupTheory/CoprodI.lean 3 9 ['SnirBroshi', 'github-actions', 'joneugster', 'mathlib-merge-conflicts', 'plp127'] joneugster
assignee:joneugster
7-21366
7 days ago
unknown
unknown
34015 erdOne
author:erdOne
 feat(AlgebraicGeometry): category of schemes affine over a base --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebraic-geometry maintainer-merge 522/11 Mathlib.lean,Mathlib/AlgebraicGeometry/AffineOver.lean,Mathlib/AlgebraicGeometry/Limits.lean,Mathlib/AlgebraicGeometry/Morphisms/Affine.lean,Mathlib/AlgebraicGeometry/OpenImmersion.lean,Mathlib/AlgebraicGeometry/RelativeGluing.lean,Mathlib/AlgebraicGeometry/Sites/SmallAffineZariski.lean,Mathlib/CategoryTheory/Sites/Hypercover/Subcanonical.lean 8 50 ['chrisflav', 'dagurtomas', 'erdOne', 'github-actions', 'mathlib-merge-conflicts', 'mathlib4-merge-conflict-bot'] chrisflav
assignee:chrisflav
7-3418
7 days ago
unknown
unknown
38665 joelriou
author:joelriou
 feat(AlgebraicTopology/SimplicialSet): characterization of Kan complexes --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebraic-topology maintainer-merge 92/2 Mathlib/AlgebraicTopology/SimplicialSet/CategoryWithFibrations.lean,Mathlib/AlgebraicTopology/SimplicialSet/KanComplex.lean 2 4 ['dagurtomas', 'github-actions', 'joelriou'] robin-carlier
assignee:robin-carlier
6-52274
6 days ago
unknown
unknown
38827 eric-wieser
author:eric-wieser
 feat: `IsEquiv` is equivalent to `Equivalence` Ideally we would have only one spelling of this, but in the meantime we should at least have a lemma to transport between the two spellings. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) easy t-logic t-order maintainer-merge 10/0 Mathlib/Order/Defs/Unbundled.lean 1 4 ['SnirBroshi', 'YaelDillies', 'github-actions'] nobody
6-34516
6 days ago
unknown
unknown
37831 EtienneC30
author:EtienneC30
 feat: the cardinal of a finset is an ite sum over a bigger finset If `s ⊆ t` then `s.card = ∑ i ∈ t, if i ∈ s then 1 else 0`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data t-algebra maintainer-merge
label:t-algebra$
 9/2 Mathlib/Algebra/BigOperators/Ring/Finset.lean,Mathlib/Data/Finset/BooleanAlgebra.lean,Mathlib/Data/Finset/Filter.lean 3 7 ['EtienneC30', 'github-actions', 'robin-carlier'] nobody
6-30083
6 days ago
unknown
unknown
38794 YaelDillies
author:YaelDillies
 feat(Algebra/Order): stronger positivity criterion for `expect` From AddCombi --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebra maintainer-merge
label:t-algebra$
 9/10 Mathlib/Algebra/Order/BigOperators/Expect.lean 1 6 ['YaelDillies', 'b-mehta', 'eric-wieser', 'github-actions', 'grunweg', 'mathlib-merge-conflicts'] nobody
5-31381
5 days ago
unknown
unknown
38854 SnirBroshi
author:SnirBroshi
 feat(Order/ConditionallyCompleteLattice/Indexed): `ciSup_mono'` for `ConditionallyCompleteLattice` Usually a primed version of a sup/inf theorem is the like the unprimed version but for `ConditionallyCompleteLinearOrderBot` which can remove `Nonempty` assumptions. `ciSup_mono'` is different from its unprimed version and it's missing `ConditionallyCompleteLattice` versions. We add these and rename `ciSup_mono'` to `ciSup_mono_of_forall_exists'`. --- I think we should also rename the `CompleteLattice` theorems `iSup_mono'`/`iInf_mono'`/`iSup₂_mono'`/`iInf₂_mono'` to not have a prime, but that'll cause a big diff so maybe later. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-order maintainer-merge 16/6 Mathlib/LinearAlgebra/Dimension/Basic.lean,Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean,Mathlib/SetTheory/Cardinal/Basic.lean 3 2 ['YaelDillies', 'github-actions'] nobody
5-21933
5 days ago
unknown
unknown
38858 SnirBroshi
author:SnirBroshi
 feat(Order/ConditionallyCompleteLattice/Basic): `ConditionallyCompleteLinearOrderBot` versions of `csSup_union`/`csSup_inter_le`/`csSup_insert` `ConditionallyCompleteLinearOrderBot` lets us drop all the `Set.Nonempty` assumptions. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-order maintainer-merge 23/0 Mathlib/Order/ConditionallyCompleteLattice/Basic.lean 1 2 ['YaelDillies', 'github-actions'] nobody
5-21089
5 days ago
unknown
unknown
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
5-21036
5 days ago
unknown
unknown
38857 SnirBroshi
author:SnirBroshi
 feat(Order/ConditionallyCompleteLattice/Indexed): conditional versions of `iSup_exists`/`iSup_and` For `iSup_exists` we can only get `≤` in `ConditionallyCompleteLattice`, and equality in `ConditionallyCompleteLinearOrderBot`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-order maintainer-merge 24/0 Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean 1 3 ['YaelDillies', 'github-actions'] nobody
5-15336
5 days ago
unknown
unknown
38835 yuanyi-350
author:yuanyi-350
 refactor(NumberTheory): golf `Mathlib/NumberTheory/Zsqrtd/GaussianInt` - rewrites `normSq_le_normSq_of_re_le_of_im_le` to reduce to the squared-coordinate inequalities and finish with `nlinarith` Extracted from #38144 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) codex t-number-theory LLM-generated maintainer-merge 3/5 Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean 1 9 ['MichaelStollBayreuth', 'github-actions', 'yuanyi-350'] MichaelStollBayreuth
assignee:MichaelStollBayreuth
5-7301
5 days ago
unknown
unknown
38832 yuanyi-350
author:yuanyi-350
 refactor(NumberTheory): golf `Mathlib/NumberTheory/FrobeniusNumber` - rewrites `frobeniusNumber_pair` to use `Nat.exists_add_mul_eq_of_gcd_dvd_of_mul_pred_le` instead of constructing the witnesses via the Chinese remainder argument - closes the final witness equality by applying `succ_inj` to the resulting additive decomposition Extracted from #38144 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) codex t-number-theory LLM-generated maintainer-merge 3/12 Mathlib/NumberTheory/FrobeniusNumber.lean 1 3 ['YaelDillies', 'github-actions', 'yuanyi-350'] tb65536
assignee:tb65536
4-9613
4 days ago
unknown
unknown
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 201/0 Mathlib.lean,Mathlib/Topology/Algebra/Order/PiecewiseLinear.lean 2 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
3-76608
3 days ago
unknown
unknown
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
3-75127
3 days ago
unknown
unknown
37676 IvanRenison
author:IvanRenison
 feat(Data/Finset/Preimage): add lemmas about `Equiv.symm` --- `Finset` version of lemmas already existing for `Set`. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data maintainer-merge 8/0 Mathlib/Data/Finset/Preimage.lean 1 3 ['github-actions', 'robin-carlier'] joneugster
assignee:joneugster
3-52286
3 days ago
unknown
unknown
36913 joelriou
author:joelriou
 feat(CategoryTheory/Monoidal): Yoneda embedding of ring objects (This series of PR mostly builds on previous work by the Toric project.) --- - [x] depends on: #38366 - [x] depends on: #37587 - [x] depends on: #37167 - [x] depends on: #37265 - [x] depends on: #37263 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-category-theory maintainer-merge 84/0 Mathlib.lean,Mathlib/CategoryTheory/Monoidal/Cartesian/Ring.lean 2 14 ['dagurtomas', 'github-actions', 'joelriou', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'robin-carlier'] robin-carlier
assignee:robin-carlier
3-31773
3 days ago
unknown
unknown
38954 joelriou
author:joelriou
 feat(AlgebraicTopology/DoldKan): the homotopy equivalence given by a splitting --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebraic-topology maintainer-merge 77/4 Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean,Mathlib/AlgebraicTopology/DoldKan/SplitSimplicialObject.lean 2 4 ['github-actions', 'joelriou', 'robin-carlier'] nobody
3-13507
3 days ago
unknown
unknown
37858 tb65536
author:tb65536
 feat(RingTheory/LocalRing/ResidueField/Fiber): `Ideal.Fiber` is a quotient of a localization This PR proves that `Ideal.Fiber` is a quotient of a localization. This is needed for #37130. --- - [x] depends on: #37380 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-ring-theory t-algebra maintainer-merge
label:t-algebra$
 16/0 Mathlib/RingTheory/LocalRing/ResidueField/Fiber.lean 1 4 ['github-actions', 'mariainesdff', 'mathlib-dependent-issues'] mariainesdff
assignee:mariainesdff
3-8146
3 days ago
unknown
unknown
38925 yuanyi-350
author:yuanyi-350
 chore(ModelTheory/ElementaryMaps): remove an erw - rewrites `map_boundedFormula` by avoiding the `iff_eq_eq` detour and using the restricted free-variable realization lemma directly - shortens `isElementary_of_exists` by replacing the `map_rel` `erw` with explicit `simp_rw` and `rw` Extracted from #38415 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) codex LLM-generated t-logic maintainer-merge 9/7 Mathlib/ModelTheory/ElementaryMaps.lean 1 3 ['github-actions', 'j-loreaux', 'loefflerd'] nobody
3-7776
3 days ago
unknown
unknown
38005 robin-carlier
author:robin-carlier
 chore(Algebra): remove simps projections for structures of bundled objects I noticed that currently, adding a `@[simps]` tag to a `ModuleCat`-valued definition will generate projections for the `isModule` fields. These projections are removed. Same in `BialgCat` and `HopfAlgCat`. --- I did not look very hard for all cases of this, but those three should be a starter. Renaming `carrier` to `coe` will break a few things, so I opted for keeping it like this for now, feel free to disagree, but this will make the diff bigger. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebra maintainer-merge
label:t-algebra$
 4/0 Mathlib/Algebra/Category/BialgCat/Basic.lean,Mathlib/Algebra/Category/HopfAlgCat/Basic.lean,Mathlib/Algebra/Category/ModuleCat/Basic.lean,Mathlib/Algebra/Category/ModuleCat/Semi.lean 4 5 ['dagurtomas', 'github-actions', 'leanprover-radar'] dagurtomas
assignee:dagurtomas
3-4518
3 days ago
unknown
unknown
38833 yuanyi-350
author:yuanyi-350
 refactor(NumberTheory): golf `Mathlib/NumberTheory/EllipticDivisibilitySequence` - rewrites `complEDS₂_mul_b` by evaluating the parity split directly with `simp_rw` and `split_ifs`, removing the separate `Int.negInduction` proof Extracted from #38144 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) codex t-number-theory LLM-generated maintainer-merge 3/8 Mathlib/NumberTheory/EllipticDivisibilitySequence.lean 1 3 ['github-actions', 'loefflerd', 'yuanyi-350'] loefflerd
assignee:loefflerd
3-3215
3 days ago
unknown
unknown
37869 mckoen
author:mckoen
 feat(AlgebraicTopology/Quasicategory): inner fibrations and inner anodyne morphisms Defines inner fibrations, inner anodyne morphisms, and immediate results. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebraic-topology maintainer-merge 220/0 Mathlib.lean,Mathlib/AlgebraicTopology/Quasicategory/Basic.lean,Mathlib/AlgebraicTopology/Quasicategory/InnerFibration.lean,Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Inner/Basic.lean 4 18 ['github-actions', 'joelriou', 'mckoen', 'robin-carlier'] nobody
2-74858
2 days ago
unknown
unknown
38414 chrisflav
author:chrisflav
 chore(RingTheory): move `IsLocalizedModule.Away` to the `Basic` file and use it everywhere --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-ring-theory maintainer-merge 42/48 Mathlib/Algebra/Module/FinitePresentation.lean,Mathlib/Algebra/Module/LocalizedModule/Away.lean,Mathlib/Algebra/Module/LocalizedModule/Basic.lean,Mathlib/AlgebraicGeometry/Modules/Tilde.lean,Mathlib/AlgebraicGeometry/StructureSheaf.lean,Mathlib/RingTheory/LocalProperties/Exactness.lean,Mathlib/RingTheory/LocalProperties/Submodule.lean,Mathlib/RingTheory/Localization/Finiteness.lean,Mathlib/RingTheory/Localization/Free.lean,Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean,Mathlib/RingTheory/Spectrum/Prime/Module.lean,Mathlib/RingTheory/Support.lean 12 8 ['chrisflav', 'dagurtomas', 'github-actions', 'grunweg', 'mathlib-merge-conflicts'] nobody
2-70383
2 days ago
unknown
unknown
37840 tb65536
author:tb65536
 chore(RingTheory/Localization/AtPrime/Basic): use `under` instead of `comap (algebraMap R S)` This PR switches over from `comap (algebraMap R S)` to `under`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-ring-theory t-algebra maintainer-merge awaiting-CI
label:t-algebra$
 172/149 Mathlib/AlgebraicGeometry/Noetherian.lean,Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean,Mathlib/RingTheory/DedekindDomain/Dvr.lean,Mathlib/RingTheory/Etale/QuasiFinite.lean,Mathlib/RingTheory/Frobenius.lean,Mathlib/RingTheory/Ideal/AssociatedPrime/Localization.lean,Mathlib/RingTheory/Ideal/GoingUp.lean,Mathlib/RingTheory/Ideal/Height.lean,Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean,Mathlib/RingTheory/Ideal/MinimalPrime/Localization.lean,Mathlib/RingTheory/Ideal/Over.lean,Mathlib/RingTheory/IntegralClosure/GoingDown.lean,Mathlib/RingTheory/Jacobson/Ring.lean,Mathlib/RingTheory/KrullDimension/Polynomial.lean,Mathlib/RingTheory/LocalProperties/Injective.lean,Mathlib/RingTheory/Localization/AtPrime/Basic.lean,Mathlib/RingTheory/Localization/AtPrime/Extension.lean,Mathlib/RingTheory/Localization/Ideal.lean,Mathlib/RingTheory/QuasiFinite/Basic.lean,Mathlib/RingTheory/Spectrum/Prime/Topology.lean 20 14 ['chrisflav', 'github-actions', 'mathlib-merge-conflicts', 'robin-carlier', 'tb65536'] chrisflav and erdOne
assignee:erdOne assignee:chrisflav
2-70246
2 days ago
unknown
unknown
38656 NoahW314
author:NoahW314
 feat(Data/Finsupp/Weight): add `Finsupp.degree_mapDomain` Generalize a result by removing an unnecessary hypothesis. Also simplifies the proof. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data maintainer-merge 9/8 Mathlib/Data/Finsupp/Weight.lean,Mathlib/Order/Filter/TendstoCofinite.lean 2 4 ['NoahW314', 'dagurtomas', 'github-actions'] nobody
2-66721
2 days ago
unknown
unknown
38971 homeowmorphism
author:homeowmorphism
 chore(FinitelyPresentedGroup): Use dot notation by default whenever possible and typo fix * Changing the usage of `IsNormalClosureFG N` to `N.IsNormalClosureFG` as the idiomatic use of the latter seems easier to read ("N is finitely generated under normal closure") and is in line with using dot notation for terms. * Fix a typo in the main definition docstring regarding the usage of `map`: it should be `.map` instead of `_map`. --- I used Copilot + Gemini Pro 3.1 to query about usage and took some of its suggestions. [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge t-group-theory 7/7 Mathlib/GroupTheory/FinitelyPresentedGroup.lean 1 2 ['github-actions', 'tb65536'] tb65536
assignee:tb65536
2-52287
2 days ago
unknown
unknown
37355 Thmoas-Guan
author:Thmoas-Guan
 feat(RingTheory): refactor `smulShortComplex` Use `LinearMap.lsmul` for the `f` of `ModuleCat.smulShortComplex`, also providing new APIs for it. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-ring-theory maintainer-merge 18/21 Mathlib/RingTheory/Regular/Category.lean 1 21 ['Thmoas-Guan', 'chrisflav', 'github-actions', 'robin-carlier'] chrisflav
assignee:chrisflav
2-49833
2 days ago
unknown
unknown
38743 eric-wieser
author:eric-wieser
 feat: `Finite` instances for `Sym` We already have the `Fintype` instances. I take the liberty of moving these into namespaces in order to produce nicer auto-generated instance names. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data maintainer-merge 25/3 Mathlib/Data/Fintype/Vector.lean 1 3 ['YaelDillies', 'github-actions'] nobody
2-38712
2 days ago
unknown
unknown
38525 AntoineChambert-Loir
author:AntoineChambert-Loir
 feat(Tactic/Translate/ToAdditive.lean): add conGen/AddConGen to the to_additive tactic This PR adds the pair "conGen", "AddConGen" to the additive tactic and capitalizes the second of some pairs that should have been. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-meta maintainer-merge 11/10 Mathlib/Algebra/Exact.lean,Mathlib/GroupTheory/Congruence/Defs.lean,Mathlib/Tactic/Translate/ToAdditive.lean 3 15 ['AntoineChambert-Loir', 'JovanGerb', 'github-actions', 'mathlib-merge-conflicts', 'robin-carlier'] JovanGerb and dwrensha
assignee:dwrensha assignee:JovanGerb
2-17441
2 days ago
2-20137
2 days ago
12-27319
12 days
38949 YaelDillies
author:YaelDillies
 chore: untag duplicated `gcongr` lemmas Follow-up to #38793 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge 11/9 Mathlib/Algebra/Module/Submodule/Basic.lean,Mathlib/Algebra/Module/Submodule/RestrictScalars.lean,Mathlib/Algebra/Order/Ring/Ordering/Basic.lean,Mathlib/Analysis/SpecialFunctions/Sigmoid.lean,Mathlib/Data/Finset/Density.lean,Mathlib/RingTheory/Localization/Submodule.lean 6 3 ['JovanGerb', 'github-actions'] nobody
2-11391
2 days ago
2-11478
2 days ago
3-33868
3 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 75 ['SnirBroshi', 'YaelDillies', 'github-actions', 'jessealama', 'mathlib-dependent-issues', 'mathlib-merge-conflicts'] YaelDillies
assignee:YaelDillies
2-9142
2 days ago
2-20534
2 days ago
40-25585
40 days
38889 emlis42
author:emlis42
 chore(NumberTheory/Divisors): golf `Int.mem_divisorsAntidiag` This PR merges the case split and removes duplicated proofs in `Int.mem_divisorsAntidiag`. t-number-theory new-contributor maintainer-merge 7/36 Mathlib/NumberTheory/Divisors.lean 1 14 ['MichaelStollBayreuth', 'SnirBroshi', 'emlis42', 'github-actions'] MichaelStollBayreuth
assignee:MichaelStollBayreuth
2-6784
2 days ago
3-57788
3 days ago
4-14668
4 days
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 47/0 Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean 1 18 ['dagurtomas', 'github-actions', 'joelriou', 'michaellee94'] robin-carlier
assignee:robin-carlier
1-82432
1 day ago
1-82459
1 day ago
4-46878
4 days
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 maintainer-merge 53/26 Mathlib/SetTheory/Cardinal/Aleph.lean,Mathlib/SetTheory/Cardinal/Cofinality.lean,Mathlib/SetTheory/Cardinal/Order.lean,Mathlib/SetTheory/Cardinal/Regular.lean 4 4 ['YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'vihdzp'] alreadydone
assignee:alreadydone
1-60868
1 day ago
3-48782
3 days ago
35-15429
35 days
37545 vihdzp
author:vihdzp
 feat(SetTheory): ℵ_ univ = univ --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-set-theory maintainer-merge 73/7 Mathlib/SetTheory/Cardinal/Aleph.lean,Mathlib/SetTheory/Cardinal/Regular.lean 2 16 ['YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'mattdiamond', 'plp127', 'vihdzp'] nobody
1-60197
1 day ago
1-60233
1 day ago
35-77839
35 days
38846 YanYablonovskiy
author:YanYablonovskiy
 feat(Order): OrderType cardinality lemmas Adding some basic lemmas for the cardinality of an order type. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) new-contributor t-order large-import maintainer-merge 28/4 Mathlib/Order/Types/Arithmetic.lean 1 10 ['YaelDillies', 'YanYablonovskiy', 'github-actions', 'plp127', 'vihdzp', 'wwylele'] YaelDillies
assignee:YaelDillies
1-42825
1 day ago
5-55804
5 days ago
6-12712
6 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
1-40860
1 day ago
38-46814
38 days ago
38-46803
38 days
38907 YaelDillies
author:YaelDillies
 chore(Geometry): move `ConvexSpace` out of `LinearAlgebra` `ConvexSpace` is convex geometry, not linear algebra --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-convex-geometry file-removed maintainer-merge 6/7 Mathlib.lean,Mathlib/Analysis/Convex/MetricSpace.lean,Mathlib/Geometry/Convex/ConvexSpace/AffineSpace.lean,Mathlib/Geometry/Convex/ConvexSpace/Defs.lean,Mathlib/Geometry/Convex/README.md 5 5 ['YaelDillies', 'github-actions', 'mathlib-merge-conflicts', 'themathqueen'] nobody
1-36840
1 day ago
1-36879
1 day ago
3-83475
3 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 329/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
1-11161
1 day ago
4-53126
4 days ago
64-61857
64 days
38370 FordUniver
author:FordUniver
 feat(Data/Finset/Powerset): add `filter_powersetCard_subset` Adds `Finset.filter_powersetCard_subset` and derives `Finset.card_filter_powersetCard_subset` from it. The hypothesis `s.card ≤ n` is necessary: without it, natural subtraction silently gives `Nat.choose k 0 = 1 ≠ 0`. Co-authored-by: Malte Jackisch --- We ran into this while formalizing Goodman's formula on triangle densities in graphs as part of an ongoing flag algebras project in Lean, and it seemed worth upstreaming. **Disclosure.** *This PR was developed with assistance from LLM code tools, used for Mathlib style alignment and proof compactness. The mathematical content and proof strategy originate from formalization work by Malte Jackisch (co-author) and myself; the final code has been reviewed and vouched for by both of us.* t-data new-contributor maintainer-merge 30/0 Mathlib/Data/Finset/Powerset.lean 1 20 ['FordUniver', 'YaelDillies', 'github-actions', 'mathlib-bors', 'wwylele'] YaelDillies
assignee:YaelDillies
1-9611
1 day ago
2-31907
2 days ago
15-8429
15 days
38963 linesthatinterlace
author:linesthatinterlace
 fix: rename `Pi.prod` to `Function.prod` Renames `Pi.prod` to `Function.prod` in order to allow for dot notation to work in the non-dependent case. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) large-import maintainer-merge 88/74 Archive/Sensitivity.lean,Mathlib/Algebra/Algebra/NonUnitalHom.lean,Mathlib/Algebra/Algebra/Prod.lean,Mathlib/Algebra/BigOperators/Finprod.lean,Mathlib/Algebra/Exact.lean,Mathlib/Algebra/Group/Prod.lean,Mathlib/Algebra/Lie/Prod.lean,Mathlib/Algebra/MvPolynomial/Equiv.lean,Mathlib/Algebra/MvPolynomial/Eval.lean,Mathlib/Algebra/Notation/Pi/Defs.lean,Mathlib/Algebra/Star/StarAlgHom.lean,Mathlib/Combinatorics/Nullstellensatz.lean,Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean,Mathlib/LinearAlgebra/Dimension/DivisionRing.lean,Mathlib/LinearAlgebra/Goursat.lean,Mathlib/LinearAlgebra/Prod.lean,Mathlib/LinearAlgebra/QuadraticForm/Dual.lean,Mathlib/Logic/Function/Defs.lean,Mathlib/MeasureTheory/Integral/Prod.lean,Mathlib/MeasureTheory/Measure/Prod.lean,Mathlib/NumberTheory/Height/Basic.lean,Mathlib/SetTheory/Cardinal/Finite.lean,Mathlib/Topology/Algebra/ContinuousAffineMap.lean,Mathlib/Topology/Algebra/InfiniteSum/Basic.lean,Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean,Mathlib/Topology/Inseparable.lean,Mathlib/Topology/UniformSpace/LocallyUniformConvergence.lean 27 4 ['fpvandoorn', 'github-actions'] nobody
1-7141
1 day ago
2-86353
2 days ago
3-4904
3 days
38604 wwylele
author:wwylele
 chore(Algebra/Module): remove some `backward.privateInPublic` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebra tech debt maintainer-merge
label:t-algebra$
 14/30 Mathlib/Algebra/Module/GradedModule.lean,Mathlib/Algebra/Module/Submodule/Lattice.lean 2 7 ['dagurtomas', 'github-actions', 'wwylele'] dagurtomas
assignee:dagurtomas
1-3322
1 day ago
2-69117
2 days ago
10-42520
10 days
38999 joelriou
author:joelriou
 feat(Algebra/Homology): homology sequence and acyclic complexes This PR adds lemmas `ShortComplex.ShortExact.acyclic_X₁/₂/₃` which allow to deduce that certain homological complexes in a short exact sequence are acyclic. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-category-theory t-algebra maintainer-merge
label:t-algebra$
 61/2 Mathlib/Algebra/Homology/HomologySequenceLemmas.lean 1 6 ['dagurtomas', 'github-actions', 'joelriou'] nobody
0-81927
22 hours ago
0-82729
22 hours ago
2-12775
2 days
39025 joelriou
author:joelriou
 feat(CategoryTheory/Localization): LocalizerMorphism.IsInduced If `Φ : LocalizerMorphism W₁ W₂`, the typeclass `Φ.IsInduced` says that `W₂.inverseImage Φ.functor = W₁`. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-category-theory maintainer-merge 67/1 Mathlib/CategoryTheory/Equivalence.lean,Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean 2 10 ['dagurtomas', 'github-actions', 'joelriou'] nobody
0-78616
21 hours ago
0-79534
22 hours ago
1-18471
1 day
39024 joelriou
author:joelriou
 feat(CategoryTheory): horizontal composition of Guitart exact squares --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-category-theory maintainer-merge 201/0 Mathlib.lean,Mathlib/CategoryTheory/GuitartExact/Basic.lean,Mathlib/CategoryTheory/GuitartExact/HorizontalComposition.lean,Mathlib/CategoryTheory/GuitartExact/VerticalComposition.lean 4 9 ['dagurtomas', 'github-actions', 'joelriou'] nobody
0-76596
21 hours ago
0-77137
21 hours ago
1-17935
1 day
38997 joelriou
author:joelriou
 feat(Algebra/Homology): the homotopy fiber and the path object --- - [x] depends on: #38996 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-category-theory maintainer-merge 228/1 Mathlib.lean,Mathlib/Algebra/Homology/ComplexShape.lean,Mathlib/Algebra/Homology/HomotopyCofiber.lean,Mathlib/Algebra/Homology/HomotopyFiber.lean,Mathlib/Algebra/Homology/Opposite.lean 5 4 ['dagurtomas', 'github-actions', 'mathlib-dependent-issues'] nobody
0-69832
19 hours ago
0-75156
20 hours ago
0-77338
21 hours
38442 Parcly-Taxel
author:Parcly-Taxel
 feat: arbitrary-order induction on `Nat` This can be used as e.g. ```lean induction n using stepInduction 3 with | base n hn => ... | step n ih => ... ``` The test file's examples are from a term project I did for an NUS module taught by Olivier Danvy himself. t-data maintainer-merge 61/2 Mathlib/Data/Nat/Init.lean,MathlibTest/StepInduction.lean 2 7 ['Parcly-Taxel', 'SnirBroshi', 'dagurtomas', 'github-actions'] nobody
0-67728
18 hours ago
1-44522
1 day ago
13-21767
13 days
39020 urkud
author:urkud
 chore(*): golf while reducing defeq abuse `Set α = α → Prop` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) maintainer-merge 14/30 Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean,Mathlib/Algebra/Ring/Subring/MulOpposite.lean,Mathlib/Analysis/Meromorphic/IsolatedZeros.lean,Mathlib/Analysis/Polynomial/MahlerMeasure.lean,Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean,Mathlib/Data/Nat/Count.lean,Mathlib/Data/Set/Function.lean 7 8 ['github-actions', 'grunweg', 'leanprover-radar', 'urkud'] nobody
0-64548
17 hours ago
0-84441
23 hours ago
1-695
1 day
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 maintainer-merge 5/12 Mathlib/GroupTheory/DivisibleHull.lean 1 3 ['github-actions', 'grunweg', 'wwylele'] jcommelin
assignee:jcommelin
0-52025
14 hours ago
2-70301
2 days ago
3-5798
3 days
39036 ajhendel
author:ajhendel
 doc: fix Lean 3 namespace in DiophantineApproximation The implementation notes section references the Lean 3 namespace \`real.contfrac_legendre\`, but this was renamed to \`Real.ContfracLegendre\` during the port. This fixes the reference. --- Co-Authored-By: Claude Opus 4.6 t-number-theory new-contributor maintainer-merge 1/1 Mathlib/NumberTheory/DiophantineApproximation/Basic.lean 1 4 ['github-actions', 'tb65536'] MichaelStollBayreuth
assignee:MichaelStollBayreuth
0-52023
14 hours ago
1-5851
1 day ago
1-5840
1 day
39014 vihdzp
author:vihdzp
 feat(Order/SuccPred/LinearLocallyFinite): `StrictMono toZ` We prove that `toZ` is strictly monotonic, and golf/deprecate other theorems in this file using this. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-order maintainer-merge 31/57 Mathlib/Order/SuccPred/LinearLocallyFinite.lean 1 5 ['YaelDillies', 'github-actions'] nobody
0-33437
9 hours ago
0-48447
13 hours ago
1-10903
1 day
37441 lecopivo
author:lecopivo
 fix(FunProp): be less strict about the shape of morphism theorems Don't be so restrictive about the shape of morphism theorems Right now, `fun_prop` has a problem with a bundled morphism `Foo α` that coerces to `α → α → α` . The coerced function has two arguments and there is an unnecessary restriction about this. This PR lifts that restriction. [Zulip discussion](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60fun_prop.60.20in.20.60FunLike.60.20with.20multiple.20arguments/with/582731349) --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-meta delegated maintainer-merge 46/12 Mathlib/Tactic/FunProp/Core.lean,Mathlib/Tactic/FunProp/Theorems.lean,MathlibTest/fun_prop_dev.lean 3 10 ['Vierkantor', 'github-actions', 'joneugster', 'mathlib-bors'] joneugster
assignee:joneugster
0-31035
8 hours ago
11-5149
11 days ago
26-84724
26 days
37808 JovanGerb
author:JovanGerb
 feat(Translate): locally modify name guessing dictionaries This PR adds the feature to `to_dual` and `to_additive` that you can now locally modify the name translation dictionary. With this change, we run the risk of having the automated translations being harder to predict. For this reason, the changes to the dictionary do not persisted through imports. Instead, the change lasts until the end of the file (though it ignores sections). See https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Order.20dual.20tactic/near/580834166 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-meta maintainer-merge 111/39 Mathlib/Order/GaloisConnection/Basic.lean,Mathlib/Order/GaloisConnection/Defs.lean,Mathlib/Order/Interval/Set/Basic.lean,Mathlib/Order/Interval/Set/Disjoint.lean,Mathlib/Tactic/Translate/Core.lean,Mathlib/Tactic/Translate/GuessName.lean,Mathlib/Tactic/Translate/ToAdditive.lean,Mathlib/Tactic/Translate/ToDual.lean,MathlibTest/ToDual.lean 9 7 ['JovanGerb', 'bryangingechen', 'github-actions', 'joneugster', 'mathlib-merge-conflicts'] joneugster
assignee:joneugster
0-27193
7 hours ago
0-27233
7 hours ago
23-17416
23 days
37573 vihdzp
author:vihdzp
 feat: supremum of `≤ c` ordinals of cardinal `≤ c` has cardinal `≤ c` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-set-theory maintainer-merge 47/13 Mathlib/SetTheory/Cardinal/Ordinal.lean 1 5 ['YaelDillies', 'github-actions', 'mathlib-merge-conflicts'] nobody
0-24473
6 hours ago
0-54570
15 hours ago
34-80736
34 days
37561 IvanRenison
author:IvanRenison
 feat(Data/List): add lemma `List.notMem_subset` --- Zulip question: https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/List.2EnotMem_subset/with/583146215 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data maintainer-merge 2/0 Mathlib/Data/List/Basic.lean 1 3 ['github-actions', 'joneugster'] joneugster
assignee:joneugster
0-24368
6 hours ago
6-65011
6 days ago
35-37971
35 days
38807 vihdzp
author:vihdzp
 feat: `DirSupClosedOn` is preserved under union --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-order maintainer-merge 81/0 Mathlib/Order/DirSupClosed.lean 1 10 ['YaelDillies', 'github-actions', 'vihdzp'] nobody
0-24353
6 hours ago
1-62450
1 day ago
6-47431
6 days
35632 SnirBroshi
author:SnirBroshi
 feat(Data/List/TakeDrop): `take`/`drop` + `tail`/`dropLast` almost commute RFC to lean4: https://github.com/leanprover/lean4/issues/12910 --- [Zulip](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/List.2Etail.2FList.2EdropLast.20.2B.20List.2Etake/with/572294698) [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-data maintainer-merge 22/0 Mathlib/Data/List/TakeDrop.lean 1 10 ['SnirBroshi', 'github-actions', 'joneugster', 'mathlib-merge-conflicts'] nobody
0-23938
6 hours ago
0-23954
6 hours ago
24-33583
24 days
38998 joelriou
author:joelriou
 feat(AlgebraicTopology/ModelCategory): precylinders in full subcategories This PR adds basic API for constructing precylinder or pre-path objects in full subcategories and study left/right homotopies in full subcategories. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebraic-topology maintainer-merge 80/0 Mathlib/AlgebraicTopology/ModelCategory/Cylinder.lean,Mathlib/AlgebraicTopology/ModelCategory/LeftHomotopy.lean,Mathlib/AlgebraicTopology/ModelCategory/PathObject.lean,Mathlib/AlgebraicTopology/ModelCategory/RightHomotopy.lean 4 2 ['github-actions', 'robin-carlier'] nobody
0-23736
6 hours ago
2-15429
2 days ago
2-15418
2 days
38090 chrisflav
author:chrisflav
 feat(AlgebraicGeometry): rank of finite flat morphism From Pi1. --- - [x] depends on: #38084 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebraic-geometry maintainer-merge 484/2 Mathlib.lean,Mathlib/Algebra/Algebra/Tower.lean,Mathlib/AlgebraicGeometry/AffineScheme.lean,Mathlib/AlgebraicGeometry/Morphisms/Affine.lean,Mathlib/AlgebraicGeometry/Morphisms/Finite.lean,Mathlib/AlgebraicGeometry/Morphisms/FinitePresentation.lean,Mathlib/AlgebraicGeometry/Morphisms/Flat.lean,Mathlib/AlgebraicGeometry/Morphisms/FlatRank.lean,Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean,Mathlib/RingTheory/Flat/Rank.lean,Mathlib/RingTheory/Localization/BaseChange.lean 11 27 ['chrisflav', 'github-actions', 'mathlib-dependent-issues', 'robin-carlier'] kim-em and robin-carlier
assignee:kim-em assignee:robin-carlier
0-20521
5 hours ago
0-20525
5 hours ago
16-17445
16 days
38651 joelriou
author:joelriou
 feat(CategoryTheory/Triangulated): localizing subcategories We show that the functor from the Verdier quotient `A/(A ⊓ B)` to `C/B` is fully faithful when `A` is a `B`-right- or left-localizing triangulated subcategory in the sense of Verdier. --- - [x] depends on: #38987 - [x] depends on: #38804 - [x] depends on: #38803 - [x] depends on: #38802 - [x] depends on: #38650 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-category-theory maintainer-merge 194/3 Mathlib/CategoryTheory/Triangulated/LocalizingSubcategory.lean 1 10 ['dagurtomas', 'github-actions', 'joelriou', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'robin-carlier'] nobody
0-11326
3 hours ago
0-11395
3 hours ago
0-69636
19 hours
36553 j-loreaux
author:j-loreaux
 feat: add IsMulCommutative instances for directed families of commutative subobjects --- - [ ] depends on: #36549 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebra maintainer-merge
label:t-algebra$
 169/1 Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean,Mathlib/Algebra/Algebra/Subalgebra/Directed.lean,Mathlib/Algebra/Group/Subgroup/Lattice.lean,Mathlib/Algebra/Group/Submonoid/Membership.lean,Mathlib/Algebra/Group/Subsemigroup/Membership.lean,Mathlib/Algebra/Ring/Subring/Basic.lean,Mathlib/Algebra/Ring/Subsemiring/Basic.lean,Mathlib/Algebra/Star/NonUnitalSubalgebra.lean,Mathlib/Algebra/Star/Subalgebra.lean,Mathlib/RingTheory/NonUnitalSubring/Basic.lean,Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean 11 7 ['github-actions', 'j-loreaux', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'robin-carlier', 'themathqueen'] kim-em
assignee:kim-em
0-10743
2 hours ago
14-83357
14 days ago
36-75960
36 days
39015 vihdzp
author:vihdzp
 chore(Order/SuccPred/LinearLocallyFinite): no expose The definitions in this file don't give any useful def-eqs, so we opt to not expose them. --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-order maintainer-merge 1/2 Mathlib/Order/SuccPred/LinearLocallyFinite.lean 1 3 ['github-actions', 'robin-carlier'] nobody
0-9313
2 hours ago
1-58418
1 day ago
1-58413
1 day
39079 joelriou
author:joelriou
 feat(AlgebraicTopology/SimplicialObject): iterations of δ 0 and σ 0 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebraic-topology maintainer-merge 149/0 Mathlib.lean,Mathlib/AlgebraicTopology/SimplicialObject/DeltaZeroIter.lean 2 2 ['github-actions', 'robin-carlier'] nobody
0-7051
1 hour ago
0-7230
2 hours ago
0-10120
2 hours
37988 chrisflav
author:chrisflav
 feat(AlgebraicGeometry): geometrically reduced group scheme over a field is smooth --- - [x] depends on: #37982 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebraic-geometry maintainer-merge 80/6 Mathlib.lean,Mathlib/AlgebraicGeometry/Group/Smooth.lean,Mathlib/AlgebraicGeometry/Morphisms/FlatDescent.lean,Mathlib/AlgebraicGeometry/Morphisms/LocalFlatDescent.lean 4 8 ['chrisflav', 'github-actions', 'mathlib-dependent-issues', 'mathlib-merge-conflicts', 'robin-carlier'] robin-carlier
assignee:robin-carlier
0-3312
55 minutes ago
0-19763
5 hours ago
3-20386
3 days
38176 chrisflav
author:chrisflav
 feat(RingTheory): local isomorphisms We add the class of algebras that are locally (on the geometric source) standard open immersions. This will be used to define ind-Zariski algebras, which are an important tool to study ind-étale algebras. From Proetale. --- - [x] depends on: #38177 [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-ring-theory maintainer-merge 217/3 Mathlib.lean,Mathlib/RingTheory/LocalIso.lean,Mathlib/RingTheory/RingHom/OpenImmersion.lean 3 8 ['chrisflav', 'github-actions', 'mathlib-dependent-issues', 'robin-carlier'] nobody
0-2480
41 minutes ago
0-3482
57 minutes ago
1-80389
1 day
38962 sharky564
author:sharky564
 refactor(Topology/Algebra/Module/LinearMap): rename subtypeL companion lemmas This PR renames the companion lemmas of `Submodule.subtypeL` for consistency with `Submodule.mkQL` (introduced in PR #38811). Specifically, `Submodule.coe_subtypeL` is renamed to `Submodule.toLinearMap_subtypeL` (to accurately reflect that it projects to the underlying LinearMap, not a function-level coercion), and `Submodule.coe_subtypeL'` is renamed to `Submodule.coe_subtypeL` (since this is the genuine function-level coercion lemma). --- This brings the `subtypeL` API in line with the `mkQL` naming convention established in PR #38811. No behavioural changes. t-topology new-contributor maintainer-merge 38/32 Mathlib/Analysis/Calculus/Implicit.lean,Mathlib/Analysis/Normed/Operator/Banach.lean,Mathlib/Topology/Algebra/Module/LinearMap.lean,scripts/nolints_prime_decls.txt 4 15 ['ADedecker', 'github-actions', 'sharky564', 'themathqueen'] nobody
0-1458
24 minutes ago
2-8478
2 days ago
2-21282
2 days
38814 sharky564
author:sharky564
 refactor(LinearAlgebra/Projection): refactor `quotientEquivOfIsCompl` via `LinearEquiv.ofLinear` This PR refactors `Submodule.quotientEquivOfIsCompl` to use `LinearEquiv.ofLinear` rather than `LinearEquiv.symm <| LinearEquiv.ofBijective`. The new definition makes both directions of the equivalence explicit: the forward idirection is `Submodule.liftQ` of the projection onto `q` along `p`, and the backward direction is `Submodule.mkQ` composed with the inclusion `q` in `E`. --- The motivation is work on topological complements of submodules in PR #38547. The proof of `IsCompl.isTopCompl_iff_continuous_quotientEquiv` reduces, via the quotient-map property of `mkQ`, to identifying the composite `quotientEquivOfIsCompl ∘ mkQ` with the linear projection. This identifications feels like it should belong at the algebraic level and not mixed in with the topological reasoning. Additionally, these lemmas seem useful independently. t-algebra new-contributor maintainer-merge
label:t-algebra$
 43/22 Mathlib/LinearAlgebra/Projection.lean 1 27 ['ADedecker', 'github-actions', 'sharky564', 'themathqueen'] nobody
0-1450
24 minutes ago
2-1360
2 days ago
6-31912
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
534-12372
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
367-62049
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
307-42398
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
307-41236
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
247-56881
8 months ago
unknown
unknown
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
204-34091
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
176-44965
5 months ago
unknown
unknown
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
171-62097
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
170-78338
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
170-29106
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
170-972
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
121-37531
4 months ago
unknown
unknown
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
87-63203
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
71-22340
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
71-22324
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
70-42353
2 months ago
unknown
unknown
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
51-60105
1 month ago
unknown
unknown
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
46-32509
1 month 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
42-42984
1 month ago
unknown
unknown
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
24-14493
24 days ago
unknown
unknown
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
21-33208
21 days ago
unknown
unknown
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
17-80769
17 days ago
unknown
unknown
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
11-67458
11 days ago
unknown
unknown
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
9-13282
9 days ago
unknown
unknown
37934 Thmoas-Guan
author:Thmoas-Guan
 feat(FieldTheory): definition of transcendental separable field extension In this PR, we introduce the concept of separably generated field extension and transcendental separable field extension. Further properties will be in #37838 --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebra awaiting-zulip
label:t-algebra$
 69/0 Mathlib.lean,Mathlib/FieldTheory/TranscendentalSeparable.lean 2 3 ['Thmoas-Guan', 'github-actions', 'robin-carlier'] robin-carlier
assignee:robin-carlier
3-11104
3 days ago
unknown
unknown
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
1-8095
1 day ago
1-8401
1 day ago
0-10603
2 hours
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 awaiting-author
label:t-algebra$
 300/2 Mathlib.lean,Mathlib/LinearAlgebra/PiTensorProduct.lean,Mathlib/LinearAlgebra/PiTensorProduct/Set.lean 3 29 ['PrParadoxy', 'dagurtomas', 'eric-wieser', 'github-actions', 'goliath-klein', 'leanprover-radar', 'mathlib4-dependent-issues-bot', 'mathlib4-merge-conflict-bot'] nobody
0-69479
19 hours ago
136-80691
136 days ago
10-66980
10 days
32742 LTolDe
author:LTolDe
 feat(MeasureTheory/Constructions/Polish/Basic): add class SuslinSpace add new class `SuslinSpace` for a topological space that is an analytic set in itself This will be useful to prove the **Effros Theorem**, see [zulip thread](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Effros.20Theorem/with/558712441). --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) new-contributor awaiting-zulip t-measure-probability awaiting-author 4/0 Mathlib/MeasureTheory/Constructions/Polish/Basic.lean 1 10 ['ADedecker', 'LTolDe', 'dagurtomas', 'dupuisf', 'github-actions', 'jcommelin'] PatrickMassot
assignee:PatrickMassot
0-68325
18 hours ago
122-1326
122 days ago
11-7507
11 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
0-67157
18 hours ago
99-4784
99 days ago
42-22427
42 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 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
0-55626
15 hours ago
201-38071
201 days ago
0-81
1 minute
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
0-12829
3 hours ago
1-20865
1 day ago
0-1
1 second
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 11 ['Garmelon', 'Hagb', 'Vierkantor', 'artie2000', 'dagurtomas', 'github-actions', 'leanprover-radar'] eric-wieser
assignee:eric-wieser
0-5978
1 hour ago
105-86366
105 days ago
40-42357
40 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
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'] nobody
1-80965
1 day ago
1-81049
1 day ago
1-81038
1 day
38604 wwylele
author:wwylele
 chore(Algebra/Module): remove some `backward.privateInPublic` --- [![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/) t-algebra tech debt maintainer-merge
label:t-algebra$
 14/30 Mathlib/Algebra/Module/GradedModule.lean,Mathlib/Algebra/Module/Submodule/Lattice.lean 2 7 ['dagurtomas', 'github-actions', 'wwylele'] dagurtomas
assignee:dagurtomas
1-3322
1 day ago
2-69117
2 days ago
10-42520
10 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 16/15 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 1 ['github-actions'] nobody
0-61829
17 hours ago
1-38167
1 day ago
1-38156
1 day
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 maintainer-merge 5/12 Mathlib/GroupTheory/DivisibleHull.lean 1 3 ['github-actions', 'grunweg', 'wwylele'] jcommelin
assignee:jcommelin
0-52025
14 hours ago
2-70301
2 days ago
3-5798
3 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'] nobody
0-22267
6 hours ago
2-22383
2 days ago
2-23401
2 days