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: November 23, 2024 at 22:43 UTC

Stale ready-to-merge'd PRs

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

Stale maintainer-merge'd PRs

Number Author Title Labels +/- 📝 💬 Assignee(s) Updated
16769 Command-Master feat(Combinatorics/SimpleGraph/Walk): add `penultimate` and `snd` maintainer-merge t-combinatorics 68/25 4 7 nobody 2024-11-10 14:56 (13 days ago)
18239 vihdzp chore(SetTheory/ZFC/Rank): clean up file t-set-theory maintainer-merge 42/37 1 7 nobody 2024-11-15 09:26 (8 days ago)
19060 vihdzp feat(Algebra/Order/SuccPred): `IsSuccLimit` theorems for `SuccAddOrder` maintainer-merge t-order 47/1 2 2 nobody 2024-11-15 11:19 (8 days ago)
15991 vihdzp feat(SetTheory/Ordinal/CantorNormalForm): alternate CNF recursion principle t-set-theory maintainer-merge t-logic 43/0 3 8 nobody 2024-11-18 23:17 (4 days ago)
19066 vihdzp feat(SetTheory/Ordinal/Nimber/Field): Nimber division t-set-theory maintainer-merge 127/2 2 9 nobody 2024-11-19 08:48 (4 days ago)
19236 vihdzp refactor(SetTheory/Ordinal/NaturalOps): redefine natural addition without `blsub` t-set-theory maintainer-merge 74/45 4 2 nobody 2024-11-19 12:31 (4 days ago)
18238 vihdzp refactor(Order/WellFounded): deprecate `WellFounded.succ` maintainer-merge t-order 12/4 1 2 nobody 2024-11-19 14:37 (4 days ago)
18469 vihdzp chore(SetTheory/Game/PGame): deprecate primed lemmas t-set-theory maintainer-merge 39/27 5 2 nobody 2024-11-19 14:40 (4 days ago)
19053 vihdzp feat(Order/InitialSeg): initial segments preserve successor limits maintainer-merge t-order 92/5 4 11 nobody 2024-11-19 21:07 (4 days ago)
18235 vihdzp feat(SetTheory/Ordinal/Basic): notation `typeLT α = type (α := α) (· < ·)` t-set-theory maintainer-merge 13/10 2 2 nobody 2024-11-19 21:58 (4 days ago)
18208 vihdzp chore(SetTheory/Ordinal/Basic): deprecate results on `WellOrder` t-set-theory maintainer-merge awaiting-author 10/13 1 4 nobody 2024-11-20 11:23 (3 days ago)
19250 pimotte feat(Combinatorics/SimpleGraph/Matching): add `IsCycles` and `IsAlternating` with basic results maintainer-merge t-combinatorics 83/0 1 15 nobody 2024-11-20 14:05 (3 days ago)
16020 adomani feat: compare PR `olean`s size with `master` maintainer-merge CI 120/0 5 49 nobody 2024-11-20 14:27 (3 days ago)

Maintainer merge'd PRs

Number Author Title Labels +/- 📝 💬 Assignee(s) Updated
16769 Command-Master feat(Combinatorics/SimpleGraph/Walk): add `penultimate` and `snd` maintainer-merge t-combinatorics 68/25 4 7 nobody 2024-11-10 14:56 (13 days ago)
18239 vihdzp chore(SetTheory/ZFC/Rank): clean up file t-set-theory maintainer-merge 42/37 1 7 nobody 2024-11-15 09:26 (8 days ago)
19060 vihdzp feat(Algebra/Order/SuccPred): `IsSuccLimit` theorems for `SuccAddOrder` maintainer-merge t-order 47/1 2 2 nobody 2024-11-15 11:19 (8 days ago)
15991 vihdzp feat(SetTheory/Ordinal/CantorNormalForm): alternate CNF recursion principle t-set-theory maintainer-merge t-logic 43/0 3 8 nobody 2024-11-18 23:17 (4 days ago)
19066 vihdzp feat(SetTheory/Ordinal/Nimber/Field): Nimber division t-set-theory maintainer-merge 127/2 2 9 nobody 2024-11-19 08:48 (4 days ago)
19236 vihdzp refactor(SetTheory/Ordinal/NaturalOps): redefine natural addition without `blsub` t-set-theory maintainer-merge 74/45 4 2 nobody 2024-11-19 12:31 (4 days ago)
18238 vihdzp refactor(Order/WellFounded): deprecate `WellFounded.succ` maintainer-merge t-order 12/4 1 2 nobody 2024-11-19 14:37 (4 days ago)
18469 vihdzp chore(SetTheory/Game/PGame): deprecate primed lemmas t-set-theory maintainer-merge 39/27 5 2 nobody 2024-11-19 14:40 (4 days ago)
19053 vihdzp feat(Order/InitialSeg): initial segments preserve successor limits maintainer-merge t-order 92/5 4 11 nobody 2024-11-19 21:07 (4 days ago)
18235 vihdzp feat(SetTheory/Ordinal/Basic): notation `typeLT α = type (α := α) (· < ·)` t-set-theory maintainer-merge 13/10 2 2 nobody 2024-11-19 21:58 (4 days ago)
18208 vihdzp chore(SetTheory/Ordinal/Basic): deprecate results on `WellOrder` t-set-theory maintainer-merge awaiting-author 10/13 1 4 nobody 2024-11-20 11:23 (3 days ago)
19250 pimotte feat(Combinatorics/SimpleGraph/Matching): add `IsCycles` and `IsAlternating` with basic results maintainer-merge t-combinatorics 83/0 1 15 nobody 2024-11-20 14:05 (3 days ago)
16020 adomani feat: compare PR `olean`s size with `master` maintainer-merge CI 120/0 5 49 nobody 2024-11-20 14:27 (3 days ago)
9013 winstonyin feat: uniform time lemma for the existence of global integral curves maintainer-merge t-differential-geometry -1/-1 -1 n/a nobody 2024-11-22 10:52 (1 days ago)
19373 pimotte feat(Combinatorics/SimpleGraph/Path): add `IsPath.getVert_injOn` maintainer-merge t-combinatorics 20/0 1 3 nobody 2024-11-23 13:35 (9 hours ago)
19387 PieterCuijpers feat: introduce the missing notation for `AddHom` maintainer-merge new-contributor t-algebra 6/1 1 3 nobody 2024-11-23 14:02 (8 hours ago)
19171 AntoineChambert-Loir feat: additivize equivariance of morphisms of actions maintainer-merge t-algebra 80/21 1 20 YaelDillies 2024-11-23 14:27 (8 hours ago)

PRs from a fork of mathlib

Number Author Title Labels +/- 📝 💬 Assignee(s) Updated
15617 vigoux perf: use foldl for implementation of Multiset.fold awaiting-author 9/0 1 1 nobody 2024-08-14 14:17 (3 months ago)
13941 TucanoUrbano feat: metric entropy t-measure-probability merge-conflict awaiting-author 4074/2 10 1 nobody 2024-08-23 16:48 (3 months ago)
16455 adomani test: bench action merge-conflict WIP 14409/7899 1181 0 nobody 2024-09-12 08:17 (2 months ago)
16688 vlad902 chore(scripts/install_macos): Fix 2 PATH resolution issues 4/0 1 1 nobody 2024-10-11 19:04 (1 months ago)
3610 TimothyGu feat: derive Infinite automatically for inductive types t-meta awaiting-author 517/0 3 10 kmill 2024-11-06 23:43 (16 days ago)
16216 jxjwan feat(RingTheory): isotypic components t-algebra 308/0 3 2 nobody 2024-11-14 11:08 (9 days ago)

PRs blocked on a zulip discussion

Number Author Title Labels +/- 📝 💬 Assignee(s) Updated
12331 mo271 chore: replace `refine ?_` and `refine' _` by `apply` awaiting-zulip merge-conflict 200/200 136 1 nobody 2024-07-31 08:13 (3 months ago)
16526 Parcly-Taxel chore: `Or 2` automated replacement of `cases'` awaiting-zulip tech debt merge-conflict 433/436 256 2 nobody 2024-09-09 10:14 (2 months ago)
11800 JADekker feat : Define KappaLindelöf spaces awaiting-zulip t-topology merge-conflict please-adopt 301/2 3 38 nobody 2024-09-16 04:51 (2 months ago)
16836 Parcly-Taxel chore: delete deprecated algebraic structure files awaiting-zulip tech debt easy merge-conflict 0/1890 7 5 nobody 2024-09-24 07:49 (1 months ago)
17518 grunweg feat: lint on declarations mentioning `Invertible` or `Unique` awaiting-zulip t-linter merge-conflict blocked-by-other-PR 149/7 13 3 nobody 2024-11-02 17:42 (21 days ago)
18397 YaelDillies chore: Rename `RestrictGenTopology` to `Topology.IsRestrictGen` awaiting-zulip t-topology 33/30 7 7 nobody 2024-11-12 11:36 (11 days ago)
18884 YaelDillies doc(overview): combinatorics overview awaiting-zulip documentation 52/6 2 10 nobody 2024-11-14 01:10 (9 days ago)
17458 urkud refactor(Algebra/Group): make `IsUnit` a typeclass awaiting-zulip t-algebra merge-conflict 107/114 27 11 nobody 2024-11-15 10:57 (8 days ago)
18085 fpvandoorn doc: factorial notation docstring t-data awaiting-zulip 7/1 1 2 nobody 2024-11-18 13:18 (5 days ago)
17623 FR-vdash-bot feat(Algebra/Order/GroupWithZero/Unbundled): add some lemmas awaiting-zulip t-order t-algebra merge-conflict 146/44 2 11 nobody 2024-11-20 12:17 (3 days ago)

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

Number Author Title Labels +/- 📝 💬 Assignee(s) Updated
19354 kim-em chore: split Order.Filter.Basic, creating Order.Filter.Finite longest-pole 380/302 11 6 nobody 2024-11-23 02:38 (20 hours ago)