Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,169 Open 32,658 Closed
2,169 Open 32,658 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

refactor(Cache): use module name for file hash instead of non-resolved file path blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) CI Modifies the continuous integration setup or other automation t-meta Tactics, attributes or user commands
#35417 opened Feb 16, 2026 by joneugster Loading…
2 tasks
2
feat(Data/Set/Basic): add some missing lemmas t-data Data (lists, quotients, numbers, etc)
#35416 opened Feb 16, 2026 by joneugster Loading…
2
feat(Cache): enable partial cache in downstream projects CI Modifies the continuous integration setup or other automation t-meta Tactics, attributes or user commands
#35415 opened Feb 16, 2026 by joneugster Loading…
1
feat(Cache): Allow arguments of the form Mathlib.Data.+ which correspond to a folder but not a file CI Modifies the continuous integration setup or other automation t-meta Tactics, attributes or user commands
#35414 opened Feb 16, 2026 by joneugster Loading…
@eric-wieser
2
fix(Util/CountHeartbeats): move elaboration in #count_heartbeats inside a namespace t-meta Tactics, attributes or user commands
#35413 opened Feb 16, 2026 by joneugster Loading…
@adomani
3
feat(Tactic/Linter): add unicode linter for unicode variant-selectors t-linter Linter
#35412 opened Feb 16, 2026 by joneugster Loading…
@grunweg
3
feat(CategoryTheory/Enriched/Limits): define cotensors in an enriched category blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) infinity-cosmos This PR is associated with Infinity Cosmos project t-category-theory Category theory WIP Work in progress
#35411 opened Feb 16, 2026 by daniel-carranza Loading…
1 task
3
chore(Translate): don't preemptively evaluate equation theorems t-meta Tactics, attributes or user commands
#35410 opened Feb 16, 2026 by JovanGerb Loading…
1
chore(Translate): use Term.applyAttributes t-meta Tactics, attributes or user commands
#35409 opened Feb 16, 2026 by JovanGerb Loading…
1
feat(NumberTheory/Height/Basic): add {mul|log}Height_comp_le, {mul|log}Height_fun_mul_eq t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#35408 opened Feb 16, 2026 by MichaelStollBayreuth Loading…
1
feat(RamificationInertia): add ramificationIdx_le_ramificationIdx and inertiaDeg_le_inertiaDeg t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#35405 opened Feb 16, 2026 by xroblot Loading…
1
feat(Topology/Algebra/Group/Basic): group is totally disconnected iff connectedComponent 1 = {1} t-algebra Algebra (groups, rings, fields, etc) t-topology Topological spaces, uniform spaces, metric spaces, filters
#35404 opened Feb 16, 2026 by tb65536 Loading…
5
feat(Topology/Algebra/Ring/Ideal): the connected component of zero is an ideal t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory t-topology Topological spaces, uniform spaces, metric spaces, filters
#35403 opened Feb 16, 2026 by tb65536 Loading…
1
feat(Dynamics/BirkhoffSum): birkhoffAverage const new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-dynamics Dynamical Systems
#35402 opened Feb 16, 2026 by samueloettl Loading…
2
feat(CategoryTheory/Sites): the equivalence between DescentData' and DescentData 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
#35401 opened Feb 16, 2026 by joelriou Loading…
2 tasks
2
feat(SimpleGraph): IsEdgeReachable lemmas t-combinatorics Combinatorics
#35400 opened Feb 16, 2026 by vlad902 Loading…
4
feat: Poisson Integral Formula for ℂ-differentiable functions t-analysis Analysis (normed *, calculus)
#35399 opened Feb 16, 2026 by kebekus Loading…
1
feat(SimpleGraph): bypass lemmas t-combinatorics Combinatorics
#35398 opened Feb 16, 2026 by vlad902 Loading…
1
feat(AlgebraicGeometry): infinitesimal lifting criterion for formally unramified morphisms t-algebraic-geometry Algebraic geometry
#35397 opened Feb 16, 2026 by erdOne Loading…
1
feat(CategoryTheory/Sites): descent data when we have pullbacks 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
#35396 opened Feb 16, 2026 by joelriou Loading…
1 task
2
chore(CategoryTheory/Subobject): correct inf_eq_map_pullback t-category-theory Category theory
#35395 opened Feb 16, 2026 by FernandoChu Loading…
1
feat(Tactic/Positivity): make positivity work for types that are not partial orders new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-meta Tactics, attributes or user commands
#35394 opened Feb 16, 2026 by HugLycan Loading…
3
feat(CategoryTheory/Limits): chosen pullbacks t-category-theory Category theory
#35393 opened Feb 16, 2026 by joelriou Loading…
1
feat(CategoryTheory/Triangulated): the heart of a t-structure t-category-theory Category theory
#35392 opened Feb 16, 2026 by joelriou Loading…
1
feat(Geometry/Manifold): API for extended coordinate changes t-differential-geometry Manifolds etc
#35391 opened Feb 16, 2026 by peabrainiac Loading…
1
ProTip! Filter pull requests by the default branch with base:master.