Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,181 Open 32,613 Closed
2,181 Open 32,613 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: inv lemmas for uniform convergence, missing to_fun attributes t-topology Topological spaces, uniform spaces, metric spaces, filters
#35384 opened Feb 15, 2026 by sgouezel Loading…
1
feat(AlgebraicGeometry): schemes are universally open over fields t-algebraic-geometry Algebraic geometry
#35383 opened Feb 15, 2026 by erdOne Loading…
1
chore: fix markdown lists
#35382 opened Feb 15, 2026 by harahu Loading…
1
feat(CategoryTheory): constructor for abelian categories t-category-theory Category theory
#35381 opened Feb 15, 2026 by joelriou Loading…
1
chore: update Mathlib dependencies 2026-02-15 auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. dependency-bump This PR bumps the version of an upstream dependency (but not toolchain).
#35380 opened Feb 15, 2026 by mathlib-update-dependencies bot Loading…
2
feat(Algebra/Homology/SpectralObject): construction of the objects on the pages of the spectral sequence blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-algebra Algebra (groups, rings, fields, etc) t-category-theory Category theory WIP Work in progress
#35378 opened Feb 15, 2026 by joelriou Loading…
3 tasks
2
chore: golf proofs
#35377 opened Feb 15, 2026 by euprunin Loading…
1
feat(Geometry/Manifold): orientable manifolds blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-differential-geometry Manifolds etc WIP Work in progress
#35376 opened Feb 15, 2026 by michaellee94 Loading…
1 task
3
feat(Algebra/Homology/SpectralObject): first quadrant spectral objects 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
#35375 opened Feb 15, 2026 by joelriou Loading…
5 tasks
2
feat(Algebra/Homology/SpectralObject): HasSpectralSequence 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
#35374 opened Feb 15, 2026 by joelriou Loading…
4 tasks
2
feat(Order/Fin): lemmas about Fin.clamp t-order Order theory
#35373 opened Feb 15, 2026 by joelriou Loading…
1
feat(Algebra/Homology/SpectralObject): SpectralSequenceMkData blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-algebra Algebra (groups, rings, fields, etc) t-category-theory Category theory WIP Work in progress
#35372 opened Feb 15, 2026 by joelriou Loading…
1 task
2
feat(MulAction): add a SMulDistribClass instance for subgroups bench-after-CI Once the PR passes CI, comment `!bench` on the PR t-algebra Algebra (groups, rings, fields, etc)
#35371 opened Feb 15, 2026 by xroblot Loading…
1
feat(CategoryTheory/Triangulated/TStructure): the spectral object 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-category-theory Category theory WIP Work in progress
#35370 opened Feb 15, 2026 by joelriou Loading…
5 tasks
2
feat(CategoryTheory/Triangulated/TStructure): properties of truncations indexed by EInt that use the octahedron axiom 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-category-theory Category theory WIP Work in progress
#35369 opened Feb 15, 2026 by joelriou Loading…
4 tasks
2
feat(CategoryTheory/Triangulated/TStructure): extensions of truncations to the extended integers 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-category-theory Category theory WIP Work in progress
#35368 opened Feb 15, 2026 by joelriou Loading…
3 tasks
2
feat(CategoryTheory/Triangulated/TStucture): induced t-structures 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-category-theory Category theory WIP Work in progress
#35367 opened Feb 15, 2026 by joelriou Loading…
3 tasks
2
feat(LinearAlgebra/Simplex): closedInterior = interior + face.closedInterior t-algebra Algebra (groups, rings, fields, etc)
#35365 opened Feb 15, 2026 by wwylele Loading…
3
feat(CategoryTheory/Triangulated/TStructure): truncLE and truncGT 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-category-theory Category theory WIP Work in progress
#35364 opened Feb 15, 2026 by joelriou Loading…
2 tasks
2
feat(CategoryTheory/Triangulated/TStructure): properties of truncLT and truncGE which use the octahedron axiom 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-category-theory Category theory WIP Work in progress
#35363 opened Feb 15, 2026 by joelriou Loading…
1 task
2
feat(CategoryTheory/Triangulated/TStructure): more on truncLT and truncGE t-category-theory Category theory WIP Work in progress
#35362 opened Feb 15, 2026 by joelriou Loading…
1
feat(Algebra/Homology/SpectralObject): cycles as cokernels and opcycles as kernels blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-algebra Algebra (groups, rings, fields, etc) t-category-theory Category theory WIP Work in progress
#35361 opened Feb 15, 2026 by joelriou Loading…
2 tasks
2
feat(SimpleGraph): rename cycleGraph_EulerianCircuit to cycleGraph.cycle t-combinatorics Combinatorics
#35360 opened Feb 15, 2026 by vlad902 Loading…
2
feat(Algebra/Homology/SpectralObject): kernel and cokernel of differentials blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-algebra Algebra (groups, rings, fields, etc) t-category-theory Category theory WIP Work in progress
#35359 opened Feb 15, 2026 by joelriou Loading…
1 task
2
feat(Geometry/Euclidean): Simplex.closedInterior is closed t-euclidean-geometry Affine and axiomatic geometry
#35358 opened Feb 15, 2026 by wwylele Loading…
5
ProTip! Filter pull requests by the default branch with base:master.