Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,018 Open 31,320 Closed
2,018 Open 31,320 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(LinearAlgebra/SpecialLinearGroup/Simple): simplicity of the projective special linear group. blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) file-removed A Lean module was (re)moved without a `deprecated_module` annotation large-import Automatically added label for PRs with a significant increase in transitive imports
#33916 opened Jan 13, 2026 by AntoineChambert-Loir Loading…
11 tasks
2
feat: irreducible components of schemes awaiting-author A reviewer has asked the author a question or requested changes. large-import Automatically added label for PRs with a significant increase in transitive imports t-algebra Algebra (groups, rings, fields, etc) t-algebraic-geometry Algebraic geometry t-ring-theory Ring theory WIP Work in progress
#33915 opened Jan 13, 2026 by tb65536 Loading…
1
fix(Tactic/Linter): support Verso docstrings in header style linter delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-linter Linter
#33914 opened Jan 13, 2026 by Vierkantor Loading…
8
feat(Data/Set/Pairwise): the {f i} are pairwise disjoint iff f is injective delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-data Data (lists, quotients, numbers, etc)
#33913 opened Jan 13, 2026 by YaelDillies Loading…
7
chore: golf using grind, reduce compilation time and imports ready-to-merge This PR has been sent to bors.
#33912 opened Jan 13, 2026 by euprunin Loading…
4
feat(Data/Set/Finite): make simp more powerful t-data Data (lists, quotients, numbers, etc)
#33911 opened Jan 13, 2026 by YaelDillies Loading…
1
feat(Data/List): a :: l ~r l.concat a awaiting-author A reviewer has asked the author a question or requested changes. easy < 20s of review time. See the lifecycle page for guidelines. t-data Data (lists, quotients, numbers, etc)
#33910 opened Jan 13, 2026 by YaelDillies Loading…
2
feat(SetTheory/Cardinal): more lemmas about ENat
#33909 opened Jan 13, 2026 by YaelDillies Loading…
1
perf: set IsScalarTower.right to high priority t-algebra Algebra (groups, rings, fields, etc)
#33908 opened Jan 13, 2026 by erdOne • Draft
4
feat(Asymptotics): Show that f =O[atTop] g from a recurrence relation t-analysis Analysis (normed *, calculus)
#33907 opened Jan 13, 2026 by dupuisf Loading…
@ADedecker
1
feat(RingTheory/SimpleModule): Jacobson density theorem delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-ring-theory Ring theory
#33906 opened Jan 13, 2026 by alreadydone Loading…
6
chore(Order/RelClasses): name arguments of recursors t-order Order theory
#33905 opened Jan 13, 2026 by plp127 Loading…
1
refactor(Algebra): weaken NormalizationMonoid 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-ring-theory Ring theory WIP Work in progress
#33904 opened Jan 12, 2026 by alreadydone Loading…
1 task
2
feat(RingTheory): local structure of monogenic unramified algebras large-import Automatically added label for PRs with a significant increase in transitive imports t-ring-theory Ring theory
#33903 opened Jan 12, 2026 by erdOne Loading…
1
chore: golf Real.exists_floor easy < 20s of review time. See the lifecycle page for guidelines. FLT part of the ongoing formalization of Fermat's Last Theorem ready-to-merge This PR has been sent to bors. t-data Data (lists, quotients, numbers, etc)
#33902 opened Jan 12, 2026 by Ruben-VandeVelde Loading…
3
feat(LinearAlgebra/Span): add inter/union/sInf/sSup lemmas for Submodule.span new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-algebra Algebra (groups, rings, fields, etc)
#33901 opened Jan 12, 2026 by martinwintermath Loading…
3
fix: generalize TransvectionStruct.det_toMatrix_prod to CommRing easy < 20s of review time. See the lifecycle page for guidelines. FLT part of the ongoing formalization of Fermat's Last Theorem ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)
#33900 opened Jan 12, 2026 by Ruben-VandeVelde Loading…
3
style: fix whitespace delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors.
#33899 opened Jan 12, 2026 by grunweg Loading…
11
feat(AlgebraicGeometry): relative gluing t-algebraic-geometry Algebraic geometry
#33898 opened Jan 12, 2026 by chrisflav Loading…
1
feat(HereditarilyLindelof): review and expand API t-topology Topological spaces, uniform spaces, metric spaces, filters
#33897 opened Jan 12, 2026 by ADedecker Loading…
1
refactor(Geometry/Manifold): split long file ChartedSpace.lean t-differential-geometry Manifolds etc tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#33896 opened Jan 12, 2026 by loefflerd Loading…
@grunweg
1
feat(Computability/Primrec): add list_take, list_drop, list_modify, and list_set new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-computability Computability theory (TMs, DFAs, languages, grammars, etc)
#33895 opened Jan 12, 2026 by jessealama Loading…
1
chore: move Archimedean to a new Defs file t-algebra Algebra (groups, rings, fields, etc)
#33894 opened Jan 12, 2026 by vihdzp Loading…
1
feat(NumberTheory/Height): heights of tuples and finsupps t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#33893 opened Jan 12, 2026 by MichaelStollBayreuth Loading…
1
feat(Algebra/Module/Submodule/Pointwise): add smul_iSup' delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#33892 opened Jan 12, 2026 by tb65536 Loading…
4
ProTip! Updated in the last three days: updated:>2026-01-10.