Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
1,901 Open 30,804 Closed
1,901 Open 30,804 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(LinearAlgebra): fix file refs t-algebra Algebra (groups, rings, fields, etc)
#33279 opened Dec 25, 2025 by harahu Loading…
1
doc(MeasureTheory): fix file refs t-measure-probability Measure theory / Probability theory
#33278 opened Dec 25, 2025 by harahu Loading…
1
doc(Logic): fix file refs t-logic Logic (model theory, etc)
#33277 opened Dec 25, 2025 by harahu Loading…
1
feat: Renaming List.reverse_perm to List.reverse_perm_self new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#33276 opened Dec 25, 2025 by NicolaBernini Loading…
1
feat(Trigonometric/Chebyshev/Extremal): Chebyshev polynomials maximize iterated derivatives blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot)
#33275 opened Dec 25, 2025 by YuvalFilmus Loading…
2 tasks
2
feat(LinearAlgebra/Lagrange): Formula for iterated derivative of a polynomial using Lagrange interpolation blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot)
#33274 opened Dec 25, 2025 by YuvalFilmus Loading…
3 tasks
2
doc(Tactics): fix file refs t-meta Tactics, attributes or user commands
#33273 opened Dec 25, 2025 by harahu Loading…
1
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 maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-order Order theory
#33266 opened Dec 25, 2025 by vihdzp Loading…
4
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(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…
22
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
ProTip! Follow long discussions with comments:>50.