Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
1,689 Open 24,783 Closed
1,689 Open 24,783 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

chore: golf using grw 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
#26981 opened Jul 10, 2025 by JovanGerb Loading…
1 task
2
feat(Algebra/GroupWithZero/WithZero): add lemma map'_surjective_iff delegated t-algebra Algebra (groups, rings, fields, etc)
#26980 opened Jul 10, 2025 by faenuccio Loading…
4
feat(Topology/GDelta/Basic): add lemmas about unions of meagre sets 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-topology Topological spaces, uniform spaces, metric spaces, filters
#26979 opened Jul 10, 2025 by shalliso Loading…
6
feat: induction principle for open sets according to a basis delegated t-topology Topological spaces, uniform spaces, metric spaces, filters
#26978 opened Jul 10, 2025 by YaelDillies Loading…
6
chore: remove 3 (of 12) direct imports of Mathlib.Tactic.NormNum by using grind
#26977 opened Jul 10, 2025 by euprunin Loading…
1
refactor(Order/Concept): rename intentClosure → lowerPolar t-order Order theory
#26976 opened Jul 10, 2025 by vihdzp Loading…
9
feat: a norm_num extension for complex numbers awaiting-author A reviewer has asked the author a question or requested changes. t-meta Tactics, attributes or user commands
#26975 opened Jul 10, 2025 by Whysoserioushah Loading…
7
feat(Geometry/Diffeology): diffeologies generated from sets of plots blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-differential-geometry Manifolds etc
#26973 opened Jul 10, 2025 by peabrainiac Loading…
1 task
3
feat(CategoryTheory): localization of quotient categories t-category-theory Category theory
#26972 opened Jul 10, 2025 by joelriou Loading…
1
feat(Order/Concept): sets in a concept are codisjoint blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-order Order theory
#26968 opened Jul 10, 2025 by vihdzp Loading…
1 task
6
feat(AlgebraicTopology/ModelCategory): left homotopies 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
#26967 opened Jul 10, 2025 by joelriou Loading…
1 task
2
feat: the Dedekind-MacNeille completion t-order Order theory
#26966 opened Jul 10, 2025 by vihdzp • Draft
4
feat: add root system induction principle equivalent to connectedness of Dynkin diagram t-algebra Algebra (groups, rings, fields, etc) WIP Work in progress
#26965 opened Jul 10, 2025 by ocfnash Loading…
1
chore: a batch of whitespace fixes maintainer-merge
#26964 opened Jul 10, 2025 by adomani Loading…
@grunweg
17
chore: remove whitespace maintainer-merge
#26963 opened Jul 10, 2025 by adomani Loading…
@grunweg
11
feat(Data/Nat/Fib/Basic): some API for Nat.fib 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)
#26962 opened Jul 10, 2025 by themathqueen Loading…
7
feat(RingTheory/PowerSeries/Substitution): add API t-algebra Algebra (groups, rings, fields, etc)
#26961 opened Jul 10, 2025 by mariainesdff Loading…
1
feat(AlgebraicTopology/ModelCategory): the lemma by K. S. Brown 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
#26960 opened Jul 10, 2025 by joelriou Loading…
2 tasks
2
feat(AlgebraicTopology): path objects in model categories 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
#26958 opened Jul 10, 2025 by joelriou Loading…
1 task
2
feat(Algebra): unmixed thm of Cohen-Macaulay ring 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-algebra Algebra (groups, rings, fields, etc)
#26957 opened Jul 10, 2025 by Thmoas-Guan Loading…
1 task
2
feat(RingTheory/DividedPowers/Basic): add divided power structure on pZp
#26956 opened Jul 10, 2025 by mariainesdff Loading…
1
feat(LinearAlgebra/OnSup): extend linear maps to sums of modules awaiting-author A reviewer has asked the author a question or requested changes. t-algebra Algebra (groups, rings, fields, etc)
#26955 opened Jul 10, 2025 by mariainesdff Loading…
7
chore: use edist instead of dist in TendstoInMeasure t-measure-probability Measure theory / Probability theory
#26954 opened Jul 10, 2025 by RemyDegenne Loading…
4
feat(CategoryTheory/DayConvolution): monoid objects internal to day convolutions blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-category-theory Category theory
#26952 opened Jul 9, 2025 by robin-carlier Loading…
1 task
2
chore: remove 11 (of 37) direct imports of Mathlib.Tactic.Ring by using grind
#26951 opened Jul 9, 2025 by euprunin Loading…
6
ProTip! no:milestone will show everything without a milestone.