Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,741 Open 37,930 Closed
2,741 Open 37,930 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(Data/Set/Lattice): Sort* polymorphism t-order Order theory
#41304 opened Jul 2, 2026 by plp127 Contributor Loading…
1 task
2
feat: Invariance of meromorphicity under scaling t-analysis Analysis (normed *, calculus)
#41303 opened Jul 2, 2026 by kebekus Collaborator • Draft
1
chore(Topology/Algebra/Valued/WithVal): clean up instances t-topology Topological spaces, uniform spaces, metric spaces, filters
#41302 opened Jul 2, 2026 by JovanGerb Contributor Loading…
1
feat(CategoryTheory): (co)kernels in functor categories/homological complexes t-category-theory Category theory
#41301 opened Jul 2, 2026 by joelriou Contributor Loading…
1
feat(EllipticCurve): the universal elliptic curve t-algebra Algebra (groups, rings, fields, etc) t-algebraic-geometry Algebraic geometry
#41300 opened Jul 2, 2026 by alreadydone Contributor Loading…
3
chore(DomAct): clean up DomMulAct/DomAddAct instances large-import Automatically added label for PRs with a significant increase in transitive imports t-group-theory Group theory
#41299 opened Jul 2, 2026 by JovanGerb Contributor Loading…
1
chore: fix Additive/Multiplicative order instances t-algebra Algebra (groups, rings, fields, etc)
#41298 opened Jul 2, 2026 by JovanGerb Contributor Loading…
1
feat: cardinality of Ultrafilter t-order Order theory
#41297 opened Jul 2, 2026 by plp127 Contributor Loading…
1
chore(CategoryTheory/Adjunction/Basic): to_dual for Adjunction.comp bors-staging This PR is currently being built by bors on the staging branch. ready-to-merge This PR has been sent to bors. t-category-theory Category theory
#41296 opened Jul 2, 2026 by JovanGerb Contributor Loading…
2
feat(CategoryTheory/Preadditive/FreydCategory/RightFreyd): the right Freyd category has cokernels blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-category-theory Category theory
#41295 opened Jul 2, 2026 by smorel394 Collaborator Loading…
2 tasks
5
feat(CategoryTheory/Preadditive/FreydCategory/RightFreyd): right Freyd category of a preadditive category blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-category-theory Category theory
#41294 opened Jul 2, 2026 by smorel394 Collaborator Loading…
1 task
2
feat: add WeierstrassCurve.exists_variableChange_lift t-algebraic-geometry Algebraic geometry
#41293 opened Jul 2, 2026 by riccardobrasca Member Loading…
1
feat(Category/Preadditive/FreydCategory/Homotopy): homotopies on the category of arrows ready-to-merge This PR has been sent to bors. t-category-theory Category theory
#41292 opened Jul 2, 2026 by smorel394 Collaborator Loading…
5
refactor(RingTheory/IntegralClosure/IsIntegral/Basic): use FaithfulSMul in isIntegral_algebraMap_iff t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#41291 opened Jul 2, 2026 by tb65536 Contributor Loading…
1
feat: implement LMFDB attribute t-meta Tactics, attributes or user commands
#41290 opened Jul 2, 2026 by Paul-Lez Collaborator Loading…
1
feat(Dynamics): recurrents set and refactoring of conservative maps t-dynamics Dynamical Systems
#41289 opened Jul 2, 2026 by D-Thomine Collaborator • Draft
1
feat(EReal): add_eq_top_iff_eq_top_* t-data Data (lists, quotients, numbers, etc)
#41288 opened Jul 2, 2026 by lua-vr Contributor Loading…
1
feat(EReal): addition of real as an orderIso t-topology Topological spaces, uniform spaces, metric spaces, filters
#41286 opened Jul 2, 2026 by lua-vr Contributor Loading…
1
feat(AlgebraicTopology/SimplicialSet): relative homology blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-algebraic-topology Algebraic topology WIP Work in progress
#41285 opened Jul 2, 2026 by joelriou Contributor Loading…
2 tasks
2
feat(Tactic/ComputablePolynomial): computable multivariate polynomials and mv_decide t-meta Tactics, attributes or user commands
#41283 opened Jul 2, 2026 by mkaratarakis Contributor • Draft
1
feat(Tactic/ComputablePolynomial): computable univariate polynomials and poly_decide t-meta Tactics, attributes or user commands
#41282 opened Jul 2, 2026 by mkaratarakis Contributor • Draft
1
doc(NumberTheory/ModularForms): remove a TODO which is done easy < 20s of review time. See the lifecycle page for guidelines. t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#41281 opened Jul 2, 2026 by loefflerd Contributor Loading…
2
feat(Geometry/Manifold): C^n smoothness of the inverse of a bundle trivialization t-differential-geometry Manifolds etc
#41280 opened Jul 2, 2026 by Deicyde Contributor Loading…
2
feat(NumberTheory): the identity of the abstract Hecke ring blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#41279 opened Jul 2, 2026 by CBirkbeck Collaborator • Draft
1 task
2
feat(NumberTheory): the convolution product on abstract Hecke rings blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-group-theory Group theory
#41277 opened Jul 2, 2026 by CBirkbeck Collaborator • Draft
1 task
2
ProTip! Adding no:label will show everything without a label.