Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
1,895 Open 30,803 Closed
1,895 Open 30,803 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

doc(Combinatorics): fix file refs t-combinatorics Combinatorics
#33272 opened Dec 25, 2025 by harahu Loading…
1
feat: prove invtSubmoduleToLieIdeal_top t-algebra Algebra (groups, rings, fields, etc)
#33271 opened Dec 25, 2025 by jano-wol Loading…
1
chore(Order/Disjoint): use to_dual blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-order Order theory
#33270 opened Dec 25, 2025 by vihdzp Loading…
1 task
2
feat(MeasureTheory/Covering): generalize some lemmas to outer measures t-measure-probability Measure theory / Probability theory
#33269 opened Dec 25, 2025 by urkud • Draft
1
refactor(Order/BoundedOrder/Lattice): use to_dual t-order Order theory
#33268 opened Dec 25, 2025 by vihdzp Loading…
1
chore(Order/WithBot): use to_dual (part 4) blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-order Order theory
#33267 opened Dec 25, 2025 by vihdzp Loading…
1 task
2
chore(Order/Synonym): use to_dual t-order Order theory
#33266 opened Dec 25, 2025 by vihdzp Loading…
1
refactor(Algebra/MvPolynomial): reorganize imports of Degrees large-import Automatically added label for PRs with a significant increase in transitive imports t-algebra Algebra (groups, rings, fields, etc)
#33265 opened Dec 25, 2025 by BoltonBailey Loading…
1
doc(AlgebraicGeometry): fix file refs t-algebraic-geometry Algebraic geometry
#33264 opened Dec 24, 2025 by harahu Loading…
1
doc(Condensed): fix file refs t-condensed Condensed mathematics
#33263 opened Dec 24, 2025 by harahu Loading…
1
doc(RepresentationTheory): fix file refs t-algebra Algebra (groups, rings, fields, etc)
#33262 opened Dec 24, 2025 by harahu Loading…
1
doc(NumberTheory): fix file refs t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#33261 opened Dec 24, 2025 by harahu Loading…
1
doc(Order): fix file refs t-order Order theory
#33260 opened Dec 24, 2025 by harahu Loading…
1
feat(Trigonometric/Chebyshev/RootsExtremal): Chebyshev polynomials are extremal in terms of leading coefficient t-analysis Analysis (normed *, calculus)
#33259 opened Dec 24, 2025 by YuvalFilmus Loading…
1
doc(misc): fix file refs
#33258 opened Dec 24, 2025 by harahu Loading…
1
feat(Combinatorics/SimpleGraph/Bipartite): Odd Cycle Theorem (A Solution to TODO) awaiting-author A reviewer has asked the author a question or requested changes. new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-combinatorics Combinatorics
#33257 opened Dec 24, 2025 by NickAdfor Loading…
20
feat(CategoryTheory/Sites): characterization of (pre)stacks for a pretopology 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
#33256 opened Dec 24, 2025 by joelriou Loading…
2 tasks
2
feat(Data/Nat/Lattice): ¬BddAbove s → sSup s = 0 t-data Data (lists, quotients, numbers, etc)
#33254 opened Dec 24, 2025 by SnirBroshi Loading…
3
feat(Combinatorics/SimpleGraph/Clique): avoid Fintype/Finite assumptions where possible t-combinatorics Combinatorics
#33253 opened Dec 24, 2025 by SnirBroshi Loading…
1
feat(Combinatorics/SimpleGraph/Clique): cliques & independent sets are chains & antichains t-combinatorics Combinatorics
#33252 opened Dec 24, 2025 by SnirBroshi Loading…
1
feat(SimpleGraph): take is path if original walk is path blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-combinatorics Combinatorics
#33249 opened Dec 24, 2025 by Rida-Hamadani Loading…
1 task
2
refactor(MeasureTheory/Measure/Stieltjes): simpler definition of botSet t-measure-probability Measure theory / Probability theory
#33248 opened Dec 24, 2025 by vihdzp Loading…
1
feat(Mathlib/RingTheory/Ideal/Cotangent): dimension of cotangent spaces file-removed A Lean module was (re)moved without a `deprecated_module` annotation new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-ring-theory Ring theory
#33247 opened Dec 23, 2025 by sun123zxy Loading…
1
feat(Analysis/Complex/Trigonometric): tan⁻¹ = cot t-analysis Analysis (normed *, calculus)
#33244 opened Dec 23, 2025 by SnirBroshi Loading…
1
feat(Analysis/Fourier): L2 and TemperedDistribution Fourier transforms coincide t-analysis Analysis (normed *, calculus)
#33242 opened Dec 23, 2025 by mcdoll Loading…
2 tasks
2
ProTip! Type g p on any issue or pull request to go back to the pull request listing page.