Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,368 Open 35,114 Closed
2,368 Open 35,114 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: fix more leaky instances delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer).
#38089 opened Apr 15, 2026 by JovanGerb Contributor Loading…
4
Batteries pr testing 1717 dependency-bump This PR bumps the version of an upstream dependency (but not toolchain). new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#38088 opened Apr 15, 2026 by MoritzBeroRoos • Draft
4
perf: add some fast_instance% t-algebra Algebra (groups, rings, fields, etc)
#38087 opened Apr 15, 2026 by kbuzzard Member Loading…
3
feat(CategoryTheory): composition of profunctors 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
#38086 opened Apr 15, 2026 by dagurtomas Contributor Loading…
1 task
2
feat(CategoryTheory): define profunctors t-category-theory Category theory
#38085 opened Apr 15, 2026 by dagurtomas Contributor Loading…
1
chore(RingTheory/Localization): rename and generalize IsLocalization.at_units t-ring-theory Ring theory
#38084 opened Apr 15, 2026 by chrisflav Member Loading…
1
feat(RingTheory/DiscreteValuationRing/Basic): compute the length of the quotient of a DVR large-import Automatically added label for PRs with a significant increase in transitive imports t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#38083 opened Apr 15, 2026 by tb65536 Contributor Loading…
1
feat(RingTheory/Ideal/Over): an ideal lying under a prime is prime t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#38082 opened Apr 15, 2026 by tb65536 Contributor Loading…
1
feat(LinearAlgebra/Dimension/StrongRankCondition): algebraMap bijective implies rank one maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#38081 opened Apr 15, 2026 by tb65536 Contributor Loading…
9
feat(Topology/Convenient): the category of X-generated spaces, as a localization blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-category-theory Category theory t-topology Topological spaces, uniform spaces, metric spaces, filters WIP Work in progress
#38080 opened Apr 15, 2026 by joelriou Contributor Loading…
1 task
2
chore: remove two unused opened namespaces easy < 20s of review time. See the lifecycle page for guidelines. t-category-theory Category theory
#38079 opened Apr 15, 2026 by bryangingechen Contributor Loading…
1
refactor: golf ValueDistribution/LogCounting/Asymptotic ConstantSpeed Analytic/Within t-analysis Analysis (normed *, calculus)
#38078 opened Apr 15, 2026 by yuanyi-350 Collaborator Loading…
2
feat(Combinatorics/Schnirelmann): prove Mann's theorem large-import Automatically added label for PRs with a significant increase in transitive imports t-combinatorics Combinatorics WIP Work in progress
#38077 opened Apr 15, 2026 by b-mehta Contributor • Draft
1
refactor: golf Analytic/IteratedFDeriv, SpecialFunctions/ t-analysis Analysis (normed *, calculus)
#38076 opened Apr 15, 2026 by yuanyi-350 Collaborator Loading…
3
refactor: golf CStarAlgebra/Unitization, Complex/Trigonometric, Asymptotics/SpecificAsymptotics t-analysis Analysis (normed *, calculus)
#38075 opened Apr 15, 2026 by yuanyi-350 Collaborator Loading…
7
refactor: PowerSeries.gaussNorm 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-ring-theory Ring theory
#38074 opened Apr 15, 2026 by WilliamCoram Collaborator Loading…
@riccardobrasca
2
chore: fix diamonds in Ideals t-ring-theory Ring theory
#38073 opened Apr 15, 2026 by sgouezel Contributor Loading…
15
feat(Convert): less aggressive congruence t-meta Tactics, attributes or user commands
#38071 opened Apr 15, 2026 by JovanGerb Contributor Loading…
1
feat: add zbmath attribute t-meta Tactics, attributes or user commands WIP Work in progress
#38070 opened Apr 15, 2026 by grunweg Contributor Loading…
2
doc(Tactic/StacksAttribute): fix outdated doc-string documentation Improvements or additions to documentation easy < 20s of review time. See the lifecycle page for guidelines. t-meta Tactics, attributes or user commands
#38069 opened Apr 15, 2026 by grunweg Contributor Loading…
1
doc(RingTheory/MvPowerSeries): fix typos in module docstrings documentation Improvements or additions to documentation easy < 20s of review time. See the lifecycle page for guidelines. t-ring-theory Ring theory
#38068 opened Apr 15, 2026 by mbkybky Collaborator Loading…
1
feat(AlgebraicTopology/SimplicialSet): the subdivision functor t-algebraic-topology Algebraic topology
#38067 opened Apr 15, 2026 by joelriou Contributor Loading…
1
chore(CategoryTheory/Comma/Arrow): restore use of inferInstanceAs t-category-theory Category theory
#38065 opened Apr 15, 2026 by JovanGerb Contributor Loading…
4
feat(CategoryTheory/CommSq): use to_dual t-category-theory Category theory
#38064 opened Apr 15, 2026 by JovanGerb Contributor Loading…
1
feat(AlgebraicTopology/SimplicialSet): the opposite of a horn blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-algebraic-topology Algebraic topology
#38063 opened Apr 15, 2026 by joelriou Contributor Loading…
1 task
2
ProTip! no:milestone will show everything without a milestone.