Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
1,907 Open 30,846 Closed
1,907 Open 30,846 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(Topology/Defs/Filter): mention "Kolmogorov quotient" in docstring documentation Improvements or additions to documentation easy < 20s of review time. See the lifecycle page for guidelines. t-topology Topological spaces, uniform spaces, metric spaces, filters
#33327 opened Dec 27, 2025 by vihdzp Loading…
1
feat(RingTheory/DedekindDomain/GaussLemma): Gauss's Lemma for Dedekind Domains blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-ring-theory Ring theory
#33326 opened Dec 26, 2025 by fbarroero Loading…
1 task
7
chore(Order/Defs/Unbundled): deprecate IsSymm in favor of core's Std.Symm t-order Order theory
#33325 opened Dec 26, 2025 by SnirBroshi Loading…
1
feat(RingTheory/DedekindDomain/AdicValuation): introduce intAdicAbv t-ring-theory Ring theory
#33324 opened Dec 26, 2025 by fbarroero Loading…
4
doc(Algebra): fix file refs t-algebra Algebra (groups, rings, fields, etc)
#33323 opened Dec 26, 2025 by harahu • Draft
1
fix: fix #lint by marking tacticDocs as public ready-to-merge This PR has been sent to bors. t-linter Linter
#33322 opened Dec 26, 2025 by thorimur Loading…
2
feat: linear independence of indecomposable roots of a root system large-import Automatically added label for PRs with a significant increase in transitive imports t-algebra Algebra (groups, rings, fields, etc)
#33321 opened Dec 26, 2025 by ocfnash Loading…
1
chore(Algebra/Order/SuccPred): add simp tags awaiting-CI This PR doesn't pass CI yet. This label is automatically removed once it does. t-algebra Algebra (groups, rings, fields, etc) t-order Order theory
#33320 opened Dec 26, 2025 by vihdzp Loading…
1
refactor(SetTheory/Ordinal/Arithmetic): deprecate boundedLimitRecOn t-set-theory Set theory
#33319 opened Dec 26, 2025 by vihdzp Loading…
1
doc(Analysis): fix file refs t-analysis Analysis (normed *, calculus)
#33318 opened Dec 26, 2025 by harahu • Draft
1
doc(Order/IsNormal): remove outdated todo documentation Improvements or additions to documentation easy < 20s of review time. See the lifecycle page for guidelines. t-order Order theory
#33317 opened Dec 26, 2025 by vihdzp Loading…
1
chore: deprecate duplicate declaration for the scalar product as a sesquilinear form t-analysis Analysis (normed *, calculus)
#33316 opened Dec 26, 2025 by sgouezel Loading…
3
doc(Data): fix file refs ready-to-merge This PR has been sent to bors. t-data Data (lists, quotients, numbers, etc)
#33315 opened Dec 26, 2025 by harahu Loading…
2
feat(Trigonometric/Chebyshev/Basic): calculate 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)
#33314 opened Dec 26, 2025 by YuvalFilmus Loading…
1 task
2
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…
6
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 delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-group-theory Group theory
#33305 opened Dec 26, 2025 by harahu Loading…
5
doc(CategoryTheory): fix file refs ready-to-merge This PR has been sent to bors. t-category-theory Category theory
#33304 opened Dec 26, 2025 by harahu Loading…
5
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
ProTip! Follow long discussions with comments:>50.