Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
3,067 Open 39,828 Closed
3,067 Open 39,828 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/Finsupp): add simp on Finsupp.ofSupportFinite_coe easy < 20s of review time. See the lifecycle page for guidelines. t-data Data (lists, quotients, numbers, etc)
#43546 opened Sep 7, 2026 by JX-Mo Contributor Loading…
2
refactor(Algebra/Order/Ring/Idempotent): introduce bundled types t-ring-theory Ring theory
#43545 opened Sep 7, 2026 by gasparattila Contributor Loading…
1
feat(Analysis/SpecialFunctions/Trigonometric): add |π| = π
#43544 opened Sep 7, 2026 by emlis42 Contributor Loading…
1
fix(LinearAlgebra): correct name and type of Affine.Simplex.span_eq_top easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields, etc)
#43543 opened Sep 7, 2026 by wwylele Collaborator Loading…
2
chore(CategoryTheory/Limits/Shapes/Products): use to_dual t-category-theory Category theory tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#43542 opened Sep 7, 2026 by JovanGerb Contributor Loading…
1
feat(Algebra/Group/Pointwise): sdiv lemmas bors-staging This PR is currently being built by bors on the staging branch. delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors.
#43541 opened Sep 7, 2026 by YaelDillies Contributor Loading…
5
feat(Topology/Order/LowerUpperTopology): the order topology in a linear order is the infimum of the lower & upper topologies t-topology Topological spaces, uniform spaces, metric spaces, filters
#43540 opened Sep 7, 2026 by SnirBroshi Collaborator Loading…
1
feat(CategoryTheory/Monoidal/Mon): add addition structure for Mon Homs 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
#43539 opened Sep 7, 2026 by abhijitaj1997 Loading…
3
feat(CategoryTheory/Abelian/Injective): the connecting homomorphism for Ext via a horseshoe diagram t-category-theory Category theory WIP Work in progress
#43538 opened Sep 7, 2026 by joelriou Contributor Loading…
1
feat: add a typeclass for the continuum hypothesis merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)
#43537 opened Sep 7, 2026 by eric-wieser Member • Draft
feat(Order): SupClosed/DirSupClosed/DirectedOn/etc for set intervals t-topology Topological spaces, uniform spaces, metric spaces, filters
#43536 opened Sep 7, 2026 by SnirBroshi Collaborator Loading…
1
feat(Analysis/SpecialFunctions/Trigonometric/Bounds): bounds for arctan against the identity new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#43535 opened Sep 7, 2026 by b1de0 Loading…
2
feat(RingTheory/Polynomial/Hermite): the Hermite polynomials have n simple real roots blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#43534 opened Sep 7, 2026 by charlesJTD Loading…
1 task
3
feat(Topology/Order/Rolle): versions of Rolle's theorem for unbounded intervals 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
#43533 opened Sep 7, 2026 by charlesJTD Loading…
3
feat(GroupTheory/Finiteness): add general IsMulFG awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-algebra Algebra (groups, rings, fields, etc) t-group-theory Group theory
#43532 opened Sep 7, 2026 by tb65536 Contributor Loading…
1
chore: put IsCadlag et al in the Function namespace t-topology Topological spaces, uniform spaces, metric spaces, filters
#43531 opened Sep 7, 2026 by EtienneC30 Member • Draft
1
feat(Order): characterise compact elements in atomistic lattices maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-order Order theory
#43530 opened Sep 7, 2026 by YaelDillies Contributor Loading…
4
feat(RepresentationTheory/Homological/ContCohomology/Sha): define Sha t-algebra Algebra (groups, rings, fields, etc)
#43529 opened Sep 7, 2026 by Whysoserioushah Collaborator Loading…
7
feat(Geometry/Convex): the simplicial set of affine simplices of a convex space blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-convex-geometry Affine geometry, cones, simplices
#43528 opened Sep 7, 2026 by joelriou Contributor Loading…
1 task
2
chore(Topology/CantorBendixson): cleanup + more basic API t-topology Topological spaces, uniform spaces, metric spaces, filters
#43526 opened Sep 7, 2026 by vihdzp Collaborator Loading…
1
feat: tag Function.leftLim with to_dual t-meta Tactics, attributes or user commands
#43525 opened Sep 7, 2026 by EtienneC30 Member • Draft
1
feat(Geometry/Convex): the cone of an affine map from the standard simplex t-convex-geometry Affine geometry, cones, simplices
#43524 opened Sep 7, 2026 by joelriou Contributor Loading…
1
feat: indepence lemma t-measure-probability Measure theory / Probability theory
#43523 opened Sep 7, 2026 by EtienneC30 Member • Draft
1
style: omit <| before fun
#43522 opened Sep 7, 2026 by JovanGerb Contributor Loading…
4
chore: make mfderiv(Within)_eq_fderiv(Within) more type-correct blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-differential-geometry Manifolds etc
#43521 opened Sep 7, 2026 by grunweg Contributor Loading…
1 task
2
ProTip! What’s not been updated in a month: updated:<2026-08-07.