Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,264 Open 32,932 Closed
2,264 Open 32,932 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: update Archive, Counterexamples, docs to module format
#35791 opened Feb 26, 2026 by kim-em Loading…
4
feat(CategoryTheory/Algebra): Flasque Sheaves have vanishing cohomology 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 new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! WIP Work in progress
#35790 opened Feb 26, 2026 by Brian-Nugent Loading…
3 tasks
4
feat(RingTheory): add some easy lemmas new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-ring-theory Ring theory
#35789 opened Feb 26, 2026 by BryceT233 Loading…
4
feat(Analysis/SchwartzSpace): post composition with continuous linear map t-analysis Analysis (normed *, calculus)
#35787 opened Feb 25, 2026 by mcdoll Loading…
1
feat(Order): Add simp lemma for IsRelUpperSet and IsRelLowerSet t-order Order theory
#35786 opened Feb 25, 2026 by DavidLedvinka Loading…
1
feat(CategoryTheory/Topology): Add Flasque Sheaves 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!
#35785 opened Feb 25, 2026 by Brian-Nugent Loading…
1 task
3
feat(MeasureTheory): Add MeasurableSingletonClass version of Measure.map_dirac t-measure-probability Measure theory / Probability theory
#35784 opened Feb 25, 2026 by DavidLedvinka Loading…
1
refactor(Combinatorics): move Dart from SimpleGraph to HasAdj blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-combinatorics Combinatorics WIP Work in progress
#35783 opened Feb 25, 2026 by IvanRenison • Draft
1 task
2
feat(MeasureTheory): Add an AEMeasurable version of Measure.map_add t-measure-probability Measure theory / Probability theory
#35782 opened Feb 25, 2026 by DavidLedvinka Loading…
1
feat(Analysis/SchwartzMap): translation of arguments t-analysis Analysis (normed *, calculus)
#35781 opened Feb 25, 2026 by mcdoll Loading…
1
feat: more lemmas about Order.cof blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot)
#35779 opened Feb 25, 2026 by vihdzp • Draft
1 task
2
feat: improve the mean value property of harmonic functions
#35778 opened Feb 25, 2026 by kebekus • Draft
1
refactor(Combinatorics): move Walk from SimpleGraph to HasAdj blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) WIP Work in progress
#35777 opened Feb 25, 2026 by IvanRenison • Draft
3 tasks
2
feat(Combinatorics): define HasAdj for capturing the common structure of different kinds of (simple) graphs t-combinatorics Combinatorics WIP Work in progress
#35776 opened Feb 25, 2026 by IvanRenison • Draft
1
feat(Data/List): add theorem length_eq_two' t-data Data (lists, quotients, numbers, etc)
#35775 opened Feb 25, 2026 by IvanRenison Loading…
4
chore: use IsLUB IsGLB in ConditionallyCompleteLattice t-order Order theory
#35774 opened Feb 25, 2026 by astrainfinita Loading…
1
refactor(Algebra/Category/ModuleCat): another approach to the module structure on stalks blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-algebra Algebra (groups, rings, fields, etc) t-category-theory Category theory WIP Work in progress
#35773 opened Feb 25, 2026 by joelriou Loading…
1 task
2
chore: golf using grind
#35772 opened Feb 25, 2026 by euprunin Loading…
1
chore: golf using exact
#35771 opened Feb 25, 2026 by euprunin Loading…
1
feat(RingTheory/Localization/FractionRing): add DecidableEq instance t-ring-theory Ring theory
#35770 opened Feb 25, 2026 by mariainesdff Loading…
1
feat(Order/WellFounded): the cardinality of a set is an upper-bound for the amount of elements before the set's mex t-order Order theory
#35769 opened Feb 25, 2026 by SnirBroshi Loading…
1
feat(RingTheory/DividedPowers/Basic): add lemmas t-ring-theory Ring theory
#35768 opened Feb 25, 2026 by mariainesdff Loading…
1
feat: asymptotics of the logCounting function of Value Distribution Theory t-analysis Analysis (normed *, calculus)
#35767 opened Feb 25, 2026 by kebekus Loading…
1
feat(Probability): add Monotonicity of setBernoulli on IsUpperSet
#35766 opened Feb 25, 2026 by DavidLedvinka • Draft
15
feat(Data/Finsupp): characterise when Finsupp is Nontrivial t-data Data (lists, quotients, numbers, etc)
#35764 opened Feb 25, 2026 by YaelDillies Loading…
1
ProTip! no:milestone will show everything without a milestone.