Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,643 Open 36,726 Closed
2,643 Open 36,726 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

feat(Topology/CategoryTheory): TopologicalSpace.Opens.map preserves colimits and finite limits blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) large-import Automatically added label for PRs with a significant increase in transitive imports t-category-theory Category theory t-topology Topological spaces, uniform spaces, metric spaces, filters
#39993 opened May 28, 2026 by Brian-Nugent Collaborator Loading…
2 tasks
2
feat(CategoryTheory/Order): Lattice Homs preserve limits and colimits t-category-theory Category theory t-order Order theory
#39992 opened May 28, 2026 by Brian-Nugent Collaborator Loading…
1
chore(Topology): refactor TopologicalSpace.Opens.map to use OrderHom.toFunctor t-topology Topological spaces, uniform spaces, metric spaces, filters
#39991 opened May 28, 2026 by Brian-Nugent Collaborator Loading…
1
chore: move Data/Nat/Lattice to Order file-removed A Lean module was (re)moved without a `deprecated_module` annotation tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#39990 opened May 28, 2026 by grunweg Contributor Loading…
1
feat(AlgebraicGeometry/Sheaves/Sites): The pullback of a quasicoherent sheaf is quasicoherent
#39989 opened May 28, 2026 by Brian-Nugent Collaborator • Draft
1
refactor(Tactic/Translate): document name translation a bit more t-meta Tactics, attributes or user commands
#39988 opened May 28, 2026 by grunweg Contributor Loading…
4
chore: golf Ordinal.cof_univ easy < 20s of review time. See the lifecycle page for guidelines. t-set-theory Set theory
#39987 opened May 28, 2026 by vihdzp Collaborator Loading…
1
feat: add HasKernels instance for Pointed awaiting-author A reviewer has asked the author a question or requested changes. large-import Automatically added label for PRs with a significant increase in transitive imports new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-category-theory Category theory
#39986 opened May 28, 2026 by CRudrum Loading…
5
fix(GroupTheory/Nilpotent): add back deprecations deleted in #39844 maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-group-theory Group theory
#39985 opened May 28, 2026 by SnirBroshi Collaborator Loading…
3
chore(Data): move some files to better locations 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 tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#39984 opened May 28, 2026 by grunweg Contributor Loading…
1 task
3
chore: remove Dynamics dependency from Data 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 tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip WIP Work in progress
#39983 opened May 28, 2026 by grunweg Contributor Loading…
1 task
2
feat: add Ideal.IsPrincipal.of_isPrincipal_pow_of_coprime t-ring-theory Ring theory
#39982 opened May 28, 2026 by riccardobrasca Member Loading…
1
feat(Analysis/Convex): prove Shapley-Folkman lemma 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-analysis Analysis (normed *, calculus)
#39981 opened May 28, 2026 by MarAndrey77 Loading…
6
chore: bump toolchain to v4.31.0-rc1 large-import Automatically added label for PRs with a significant increase in transitive imports
#39980 opened May 28, 2026 by Garmelon Contributor Loading…
4
feat(Analysis/Oscillation): oscillation along a filter large-import Automatically added label for PRs with a significant increase in transitive imports t-analysis Analysis (normed *, calculus)
#39979 opened May 28, 2026 by lua-vr Contributor • Draft
1
refactor(CategoryTheory): redefine MorphismProperty.IsLocalAtTarget in terms of presieves maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-category-theory Category theory
#39978 opened May 28, 2026 by chrisflav Member Loading…
4
feat(RingTheory/RamificationInertia/Ramification): positivity of ramification index t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#39977 opened May 28, 2026 by tb65536 Contributor Loading…
1
chore: move Data.Rat.NatSqrt.Real to Analysis 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 tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#39976 opened May 28, 2026 by grunweg Contributor Loading…
1 task
2
chore: tag (Continuous)LinearEquiv.prodCongr_symm with @[simp]
#39975 opened May 28, 2026 by gasparattila Contributor Loading…
1
chore: move Data/Real/StarOrdered to Algebra/Order/Star/Real 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
#39974 opened May 28, 2026 by grunweg Contributor Loading…
1 task
2
chore(Topology/Algebra/Category/ProfiniteGrp/*): to_additivize some declarations t-algebra Algebra (groups, rings, fields, etc) t-group-theory Group theory t-topology Topological spaces, uniform spaces, metric spaces, filters
#39973 opened May 28, 2026 by tb65536 Contributor Loading…
2
feat(GroupTheory/Torsion): the free rank of an abelian group t-algebra Algebra (groups, rings, fields, etc) t-group-theory Group theory
#39972 opened May 28, 2026 by tb65536 Contributor Loading…
4
chore: move Data.Real.{Archimedian,Hom} to Algebra.Order.Archimedian.Real.{Basic,Hom} 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
#39971 opened May 28, 2026 by grunweg Contributor Loading…
1 task
2
perf(AlgebraicGeometry): specialize index type in AffineSpace to Type u t-algebraic-geometry Algebraic geometry
#39970 opened May 28, 2026 by chrisflav Member Loading…
3
feat(Analysis): pre/postcomposition by an isometry preserves the operator norm t-analysis Analysis (normed *, calculus)
#39969 opened May 28, 2026 by YaelDillies Contributor Loading…
1
ProTip! Updated in the last three days: updated:>2026-05-25.