Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,577 Open 36,485 Closed
2,577 Open 36,485 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

chore: move test files and recapitalise file names (part 4) file-removed A Lean module was (re)moved without a `deprecated_module` annotation
#39683 opened May 22, 2026 by joneugster Contributor Loading…
1
chore: move test files and recapitalise file names (part 3) file-removed A Lean module was (re)moved without a `deprecated_module` annotation
#39682 opened May 22, 2026 by joneugster Contributor Loading…
1
chore: move test files and recapitalise file names (part 2) file-removed A Lean module was (re)moved without a `deprecated_module` annotation
#39681 opened May 22, 2026 by joneugster Contributor Loading…
1
feat(CI): validate more aspects of PR titles t-linter Linter
#39680 opened May 22, 2026 by grunweg Contributor Loading…
1
feat(RingTheory/Extension): fromH1Cotangent blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-ring-theory Ring theory
#39679 opened May 22, 2026 by BryceT233 Contributor Loading…
1 task
2
feat(RingTheory/RamificationInertia/Ramification): ramification index is invariant under a group action t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#39678 opened May 22, 2026 by tb65536 Contributor Loading…
1
feat: improve doc-strings for differential geometry elaborators blocked-by-core-release Not relevant for the current Lean release candidate, but will be needed for the next. t-differential-geometry Manifolds etc t-meta Tactics, attributes or user commands WIP Work in progress
#39677 opened May 21, 2026 by grunweg Contributor Loading…
1
chore: move test files and recapitalise filennames blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) file-removed A Lean module was (re)moved without a `deprecated_module` annotation
#39676 opened May 21, 2026 by joneugster Contributor Loading…
3 tasks
3
feat: add instances of MetricSpace, NormedAddGroup, and NormedAddCommGroup for DirectLimit awaiting-author A reviewer has asked the author a question or requested changes. new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-topology Topological spaces, uniform spaces, metric spaces, filters
#39673 opened May 21, 2026 by drocta Contributor Loading…
24
feat(RingTheory/Ideal/GoingUp): a prime ideal is minimal over the image of its preimage t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#39672 opened May 21, 2026 by tb65536 Contributor Loading…
1
feat(Data/ENat/Basic): add ENat.toNat_pos t-algebra Algebra (groups, rings, fields, etc) t-data Data (lists, quotients, numbers, etc)
#39671 opened May 21, 2026 by tb65536 Contributor Loading…
1
feat(CategoryTheory/Limits/Shapes): add WalkingArrow category new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-category-theory Category theory
#39670 opened May 21, 2026 by VictorBoscaro Loading…
2
feat(CategoryTheory): the category of κ-directed posets maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-category-theory Category theory
#39669 opened May 21, 2026 by joelriou Contributor Loading…
8
feat(ci): per-PR comment summarising cross-reference tags blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot)
#39666 opened May 21, 2026 by kim-em Contributor • Draft
1 task done
2
feat(AlgebraicGeometry/AffineSpace): affine space over an integral base is integral t-algebraic-geometry Algebraic geometry
#39665 opened May 21, 2026 by justus-springer Collaborator Loading…
1
feat(CrossRefAttribute): info-view widget for cross-reference tags blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot)
#39664 opened May 21, 2026 by kim-em Contributor • Draft
1 task done
6
feat(Topology): A spectral map between quasi-separated, prespectral sober spaces has compact fibers t-topology Topological spaces, uniform spaces, metric spaces, filters
#39663 opened May 21, 2026 by Raph-DG Collaborator Loading…
1
feat(scripts): add cross-reference tag tooling CI Modifies the continuous integration setup or other automation
#39662 opened May 21, 2026 by kim-em Contributor • Draft
1
feat(Combinatorics/Enumerative): GeneratingFunction/ part 3/13 blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) LLM-generated PRs with substantial input from LLMs - review accordingly t-combinatorics Combinatorics
#39661 opened May 21, 2026 by rwst Collaborator Loading…
1 task
2
feat(Combinatorics/Enumerative): GeneratingFunction/ part 2/13 blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) LLM-generated PRs with substantial input from LLMs - review accordingly t-combinatorics Combinatorics
#39660 opened May 21, 2026 by rwst Collaborator Loading…
1 task
2
feat(Combinatorics/Enumerative): GeneratingFunction/Defs.lean (1/13) LLM-generated PRs with substantial input from LLMs - review accordingly t-combinatorics Combinatorics
#39659 opened May 21, 2026 by rwst Collaborator Loading…
1
feat(Algebra.Module.Submodule.Ker): add one lemma about ker of domRestrict t-algebra Algebra (groups, rings, fields, etc)
#39658 opened May 21, 2026 by faenuccio Contributor Loading…
9
feat(Algebra): add abstract prod_apply and FunLike.coe_prod t-algebra Algebra (groups, rings, fields, etc)
#39657 opened May 21, 2026 by mcdoll Member Loading…
2
feat(AlgebraicGeometry/Birational/RationalMap): add RationalMap.representative maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-algebraic-geometry Algebraic geometry
#39656 opened May 21, 2026 by justus-springer Collaborator Loading…
3
feat(CategoryTheory): the κ-accessible category of κ-directed posets blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-category-theory Category theory WIP Work in progress
#39655 opened May 21, 2026 by joelriou Contributor Loading…
1 task
2
ProTip! Type g p on any issue or pull request to go back to the pull request listing page.