Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,392 Open 35,345 Closed
2,392 Open 35,345 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(NumberTheory): add Int.divisors new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#38345 opened Apr 21, 2026 by emlis42 Loading…
2
feat(SimpleGraph/Coloring/VertexColoring): Matching is 2 colorable new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-combinatorics Combinatorics
#38344 opened Apr 21, 2026 by robo7179 Loading…
3
chore(Data/Nat/Cast/Order/Ring): Move two Nat lemmas to Data/Nat/Basic new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-data Data (lists, quotients, numbers, etc)
#38343 opened Apr 21, 2026 by mortarsanjaya Contributor Loading…
2
chore(CategoryTheory/Monoidal): rename Mod_ to Mod t-category-theory Category theory
#38342 opened Apr 21, 2026 by chrisflav Member Loading…
1
refactor(Algebra/Category/ModuleCat/Sheaf/Free): generalize SheafOfModules.mapFree t-algebra Algebra (groups, rings, fields, etc) t-algebraic-geometry Algebraic geometry
#38341 opened Apr 21, 2026 by justus-springer Collaborator Loading…
1
refactor(Data/ZMod): move coe_int_isUnit_iff_isCoprime to ZMod.Units t-data Data (lists, quotients, numbers, etc)
#38340 opened Apr 21, 2026 by xroblot Collaborator Loading…
1
feat(NumberTheory/DirichletCharacter): add conductor_changeLevel and subgroups of characters mapping to one blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#38339 opened Apr 21, 2026 by xroblot Collaborator Loading…
1 task
2
feat(Combinatorics/Graph): supremum t-combinatorics Combinatorics
#38337 opened Apr 21, 2026 by Jun2M Collaborator Loading…
1
feat(CategoryTheory/Monoidal): actions by monoid objects awaiting-author A reviewer has asked the author a question or requested changes. 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
#38336 opened Apr 21, 2026 by chrisflav Member Loading…
1 task
7
feat: add Monoid.End.ext easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields, etc)
#38335 opened Apr 21, 2026 by riccardobrasca Member Loading…
1
feat(Combinatorics/SimpleGraph/TreeDecomp): define tree decompositions blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) help-wanted The author needs attention to resolve issues new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-combinatorics Combinatorics
#38334 opened Apr 21, 2026 by 8e7 Loading…
1 task
4
feat(RepresentationTheory/Coinvariants): finiteness instance for coinvariants maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-algebra Algebra (groups, rings, fields, etc)
#38333 opened Apr 21, 2026 by tb65536 Contributor Loading…
3
feat(RingTheory/Frobenius): Frobenius elements lie in the decomposition group t-algebra Algebra (groups, rings, fields, etc) t-number-theory Number theory (also use t-algebra or t-analysis to specialize) t-ring-theory Ring theory
#38332 opened Apr 21, 2026 by tb65536 Contributor Loading…
1
feat(RingTheory/AdicCompletion): AdicCompletion of Noetherian ring is Noetherian 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-ring-theory Ring theory
#38331 opened Apr 21, 2026 by Thmoas-Guan Collaborator Loading…
1 task
2
chore: tighten down public/exposed API of AlgebraicClosure t-algebra Algebra (groups, rings, fields, etc)
#38329 opened Apr 21, 2026 by jcommelin Member Loading…
20
feat: OrderSupSet t-order Order theory
#38328 opened Apr 21, 2026 by astrainfinita Collaborator • Draft
1
chore(Topology/Connected/LocPathConnected): fix typo in LocPathConnectedSpace docstring t-topology Topological spaces, uniform spaces, metric spaces, filters
#38327 opened Apr 21, 2026 by kim-em Contributor Loading…
1
feat(Combinatorics/Graph): Degree blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot)
#38326 opened Apr 21, 2026 by Jun2M Collaborator Loading…
1 task
2
feat(Combinatorics/Graph): EndPoint function large-import Automatically added label for PRs with a significant increase in transitive imports t-combinatorics Combinatorics
#38325 opened Apr 21, 2026 by Jun2M Collaborator Loading…
2
chore(RingTheory/AdicCompletion): make AdicCompletion.map linear on linear maps t-ring-theory Ring theory
#38324 opened Apr 21, 2026 by BryceT233 Contributor Loading…
1
feat(RingTheory/MvPolynomial/MonomialOrder): remove unnecessary hypothesis t-ring-theory Ring theory
#38323 opened Apr 21, 2026 by NoahW314 Contributor Loading…
1
feat(Algebra/MvPolynomial): add monomial prod lemma t-algebra Algebra (groups, rings, fields, etc)
#38322 opened Apr 21, 2026 by NoahW314 Contributor Loading…
2
Tag absolute value lemmas with @[push] t-algebra Algebra (groups, rings, fields, etc)
#38321 opened Apr 21, 2026 by ldct Collaborator • Draft
1 of 2 tasks
1
feat(Combinatorics/SetFamily): Assouad's dual VC bound new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-combinatorics Combinatorics
#38319 opened Apr 20, 2026 by Zetetic-Dhruv Loading…
5
feat(GRewrite): new grw implementation merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)
#38318 opened Apr 20, 2026 by JovanGerb Contributor • Draft
2
ProTip! Type g i on any issue or pull request to go back to the issue listing page.