Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
1,921 Open 30,819 Closed
1,921 Open 30,819 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(Trigonometric/Chebyshev/Basic): calculate iterated derivatives of T and U at 1
#33314 opened Dec 26, 2025 by YuvalFilmus Loading…
1 task
1
feat(Combinatorics/SimpleGraph/EdgeColoring): create a basic edge-coloring API 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
#33313 opened Dec 26, 2025 by SnirBroshi Loading…
1 task
2
feat(Polynomial/Chebyshev): formulas for iterated derivatives of T and U at 1 blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot)
#33312 opened Dec 26, 2025 by YuvalFilmus Loading…
2 tasks
2
feat(Polynomial/Chebyshev): calculate values of T and U at zero t-ring-theory Ring theory
#33311 opened Dec 26, 2025 by YuvalFilmus Loading…
1
feat(RingTheory/WittVector): isomorphism of Witt vectors mod p with base ring 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-ring-theory Ring theory
#33310 opened Dec 26, 2025 by sglasman Loading…
4
feat(Topology.GDelta.Basic): add helpers for IsMeagre 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-topology Topological spaces, uniform spaces, metric spaces, filters
#33308 opened Dec 26, 2025 by LTolDe Loading…
1
Orientable manifolds updated t-differential-geometry Manifolds etc WIP Work in progress
#33307 opened Dec 26, 2025 by grunweg Loading…
2
feat(Polynomial/Derivative): formulas for iterated derivatives of P * X^m t-algebra Algebra (groups, rings, fields, etc)
#33306 opened Dec 26, 2025 by YuvalFilmus Loading…
1
doc(GroupTheory): fix file refs t-group-theory Group theory
#33305 opened Dec 26, 2025 by harahu Loading…
1
doc(CategoryTheory): fix file refs t-category-theory Category theory
#33304 opened Dec 26, 2025 by harahu • Draft
1
feat(CategoryTheory): The monads and comonads of locally cartesian closed categories t-category-theory Category theory WIP Work in progress
#33303 opened Dec 26, 2025 by sinhp Loading…
1
chore(Algebra/Central/End): generalize Algebra.IsCentral.instEnd t-algebra Algebra (groups, rings, fields, etc)
#33301 opened Dec 26, 2025 by themathqueen Loading…
2
feat: a finite space is Baire. large-import Automatically added label for PRs with a significant increase in transitive imports t-topology Topological spaces, uniform spaces, metric spaces, filters
#33300 opened Dec 26, 2025 by CoolRmal Loading…
1
feat: Add decidable membership for Interval new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-order Order theory
#33299 opened Dec 26, 2025 by kingiler Loading…
3
chore: mark Ordinal.enumOrd with no_expose easy < 20s of review time. See the lifecycle page for guidelines. t-set-theory Set theory
#33298 opened Dec 26, 2025 by vihdzp Loading…
1
feat(Algebra/Polynomial/Roots): add card_rootSet_le large-import Automatically added label for PRs with a significant increase in transitive imports t-algebra Algebra (groups, rings, fields, etc)
#33297 opened Dec 26, 2025 by tb65536 Loading…
1
feat(Algebra/Central/End): center of endomorphisms of a free module t-algebra Algebra (groups, rings, fields, etc)
#33295 opened Dec 26, 2025 by AntoineChambert-Loir Loading…
1
refactor: deprecate Ordinal.IsNormal for Order.IsNormal delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-order Order theory t-set-theory Set theory
#33294 opened Dec 26, 2025 by vihdzp Loading…
8
feat(Combinatorics/SimpleGraphs/LineGraph): lift copies/isomorphisms to line-graph large-import Automatically added label for PRs with a significant increase in transitive imports t-combinatorics Combinatorics
#33292 opened Dec 25, 2025 by SnirBroshi Loading…
1
refactor(Computability): File for state transition systems t-computability Computability theory (TMs, DFAs, languages, grammars, etc)
#33291 opened Dec 25, 2025 by BoltonBailey Loading…
1
chore: golf using grind and simp
#33290 opened Dec 25, 2025 by euprunin Loading…
3
feat(Analysis/SpecialFunctions/Integrals): add ∫ x : ℝ in a..b, (c ^ 2 + x ^ 2)⁻¹ new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#33289 opened Dec 25, 2025 by michelsol Loading…
1
chore(Combinatorics/SimpleGraph/Paths): review API t-combinatorics Combinatorics
#33288 opened Dec 25, 2025 by vihdzp Loading…
1
feat(CategoryTheory/Sites): more API for IsSheafFor maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-category-theory Category theory
#33287 opened Dec 25, 2025 by joelriou Loading…
5
chore: golf using grind
#33286 opened Dec 25, 2025 by euprunin Loading…
1
ProTip! no:milestone will show everything without a milestone.