Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
3,142 Open 38,940 Closed
3,142 Open 38,940 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

feat(Order/GaloisConnection): add variant of l_sSup and l_sInf t-order Order theory
#42729 opened Aug 13, 2026 by martinwintermath Contributor Loading…
1
chore(Dynamics): remove backward.isDefEq.respectTransparency options easy < 20s of review time. See the lifecycle page for guidelines. t-dynamics Dynamical Systems tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#42728 opened Aug 13, 2026 by FrankieNC Collaborator Loading…
1
chore: mark Monotone.functor as implicit_reducible t-category-theory Category theory tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#42726 opened Aug 13, 2026 by JovanGerb Contributor Loading…
1
feat(Combinatorics): the dominance order on partitions 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 t-combinatorics Combinatorics
#42725 opened Aug 13, 2026 by kim-em Contributor • Draft
1 task
2
feat(RingTheory/Polynomial/Hermite): derivatives and the generating function t-ring-theory Ring theory
#42724 opened Aug 13, 2026 by kim-em Contributor • Draft
1
feat(GroupTheory/Perm): cycle type of a power of a cycle t-group-theory Group theory
#42723 opened Aug 13, 2026 by kim-em Contributor • Draft
1
chore: mark WidePushoutShape.wideSpan as implicit_reducible tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#42722 opened Aug 13, 2026 by JovanGerb Contributor Loading…
1
chore: mark CategoryTheory.Limits.pair as implicit_reducible t-category-theory Category theory tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#42721 opened Aug 13, 2026 by JovanGerb Contributor Loading…
1
feat(Order/KrullDimension): level sets of height are antichains new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-order Order theory
#42720 opened Aug 13, 2026 by justinhalford Loading…
2
feat(LinearAlgebra/BilinearForm): totally isotropic subspaces have dimension at most half new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-algebra Algebra (groups, rings, fields, etc)
#42719 opened Aug 13, 2026 by justinhalford Loading…
2
feat(Combinatorics/SetFamily): the linear algebra method and the Oddtown theorem new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-combinatorics Combinatorics
#42718 opened Aug 13, 2026 by justinhalford Loading…
3
chore(RingTheory/MvPolynomial/Symmetric/Eval): automated extraction from #28013 auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. t-ring-theory Ring theory
#42717 opened Aug 13, 2026 by mathlib-splicebot Bot Loading…
1
feat(CategoryTheory): module structure on ext groups t-algebra Algebra (groups, rings, fields, etc)
#42716 opened Aug 13, 2026 by Raph-DG Collaborator Loading…
2
chore(Data/Finsupp/Quotient): automated extraction from #28013 auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. t-data Data (lists, quotients, numbers, etc)
#42715 opened Aug 13, 2026 by mathlib-splicebot Bot Loading…
1
feat(Logic/Function): define predicate for constant function t-logic Logic (model theory, etc)
#42713 opened Aug 13, 2026 by martinwintermath Contributor Loading…
1
feat(Algebra/QuadraticAlgebra): quadratic orders over ℤ and their fraction ring t-ring-theory Ring theory
#42711 opened Aug 13, 2026 by xroblot Collaborator Loading…
1 task
2
chore(GroupTheory/GroupAction): cleanup imports blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot)
#42710 opened Aug 13, 2026 by qawbecrdtey Collaborator Loading…
1 task
4
chore(Analysis): deprecate Seminorm.lean t-analysis Analysis (normed *, calculus)
#42709 opened Aug 13, 2026 by mcdoll Member Loading…
1
feat(Algebra/QuadraticAlgebra): classify quadratic algebras by their discriminant t-algebra Algebra (groups, rings, fields, etc)
#42708 opened Aug 13, 2026 by xroblot Collaborator Loading…
1 task
2
feat(Topology): generalise Lipschitz to WeakPseudoEMetricSpace blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-topology Topological spaces, uniform spaces, metric spaces, filters
#42706 opened Aug 12, 2026 by felixpernegger Contributor Loading…
1 task
4
refactor(Data/SetLike): make second parameter of *.ofSetLike implicit t-data Data (lists, quotients, numbers, etc)
#42705 opened Aug 12, 2026 by artie2000 Collaborator Loading…
1
refactor(Data/FunLike): make the arguments of Is*Apply implicit
#42704 opened Aug 12, 2026 by gasparattila Contributor Loading…
1
refactor(Data/SetLike): make second parameter of IsConcreteLE implicit t-data Data (lists, quotients, numbers, etc)
#42703 opened Aug 12, 2026 by artie2000 Collaborator Loading…
2
chore(Data/SetLike): rename IsConcreteLE and its API blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-data Data (lists, quotients, numbers, etc)
#42702 opened Aug 12, 2026 by artie2000 Collaborator Loading…
1 task
3
feat(Valuation/ValuationSubring): add ofSubring_toSubring easy < 20s of review time. See the lifecycle page for guidelines. t-ring-theory Ring theory
#42701 opened Aug 12, 2026 by xgenereux Collaborator Loading…
1
ProTip! Add no:assignee to see everything that’s not assigned.