Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,439 Open 36,019 Closed
2,439 Open 36,019 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(RingTheory/RamificationInertia/Ramification): relate ramificationIdx' to Algebra.IsUnramifiedAt awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. large-import Automatically added label for PRs with a significant increase in transitive imports t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#39074 opened May 8, 2026 by tb65536 Contributor Loading…
1
feat(RingTheory/RamificationInertia/Inertia): add inertiaDeg'_pos awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#39073 opened May 8, 2026 by tb65536 Contributor Loading…
1
feat(RingTheory/Unramified/Locus): add iff lemma relating Unramified to IsUnramifiedAt awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#39072 opened May 8, 2026 by tb65536 Contributor Loading…
1
feat(Topology): add PartialHomeomorph as generalization of OpenPartialHomeomorph
#39071 opened May 8, 2026 by scholzhannah Collaborator • Draft
1
chore(RingTheory/Ideal/GoingUp): weaken IsIntegralClosure to Algebra.IsIntegral awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#39070 opened May 8, 2026 by tb65536 Contributor Loading…
1
Review 37924 instance whnf t-meta Tactics, attributes or user commands
#39069 opened May 8, 2026 by joneugster Contributor • Draft
5
feat(Algebra/Module): define modules admitting finite free resolutions t-algebra Algebra (groups, rings, fields, etc)
#39067 opened May 8, 2026 by mbkybky Collaborator Loading…
1
feat(Analysis): LinearMap.id is unitary t-analysis Analysis (normed *, calculus)
#39066 opened May 8, 2026 by YaelDillies Contributor Loading…
4
feat(Analysis): the trivial inner product space t-analysis Analysis (normed *, calculus)
#39065 opened May 8, 2026 by YaelDillies Contributor Loading…
2
feat: make showLinter detect tactics that assign metavariables t-linter Linter
#39064 opened May 8, 2026 by kim-em Contributor Loading…
1
feat(Topology/Algebra/Module/LocallyConvex): a very nice basis of locally convex spaces t-topology Topological spaces, uniform spaces, metric spaces, filters
#39063 opened May 8, 2026 by khwilson Contributor Loading…
2
feat(Algebra/Order/SuccPred): generalize CanonicallyOrderedAdd to IsBotZeroClass
#39062 opened May 8, 2026 by vihdzp Collaborator Loading…
2
feat(Combinatorics/SimpleGraph/Walk/Paths): a trail which isn't a path has a cycle subwalk t-combinatorics Combinatorics
#39061 opened May 8, 2026 by SnirBroshi Collaborator Loading…
1
feat: generalize Finsupp theorems from CanonicallyOrderedAdd to IsBotZeroClass 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) t-order Order theory
#39060 opened May 8, 2026 by vihdzp Collaborator Loading…
1 task
2
feat: IsBotOneClass (Associates M) t-algebra Algebra (groups, rings, fields, etc)
#39059 opened May 7, 2026 by vihdzp Collaborator Loading…
1
chore: deprecate Fin.bot_eq_zero large-import Automatically added label for PRs with a significant increase in transitive imports t-order Order theory
#39058 opened May 7, 2026 by vihdzp Collaborator Loading…
1
feat: min and max theorems for IsBotZeroClass large-import Automatically added label for PRs with a significant increase in transitive imports t-order Order theory
#39057 opened May 7, 2026 by vihdzp Collaborator Loading…
1
feat: IsBotOneClass ℕ+ t-data Data (lists, quotients, numbers, etc)
#39056 opened May 7, 2026 by vihdzp Collaborator Loading…
1
chore: deprecate not_lt_zero' and bot_eq_zero'' t-order Order theory
#39055 opened May 7, 2026 by vihdzp Collaborator Loading…
1
feat(Combinatorics/GraphLike): SimpleGraph is GraphLike blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-combinatorics Combinatorics
#39054 opened May 7, 2026 by Jun2M Collaborator Loading…
3 tasks
2
feat(Combinatorics/GraphLike): Graph is GraphLike blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-combinatorics Combinatorics
#39053 opened May 7, 2026 by Jun2M Collaborator Loading…
3 tasks
2
feat(Combinatorics/GraphLike): Digraph is GraphLike blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-combinatorics Combinatorics
#39050 opened May 7, 2026 by Jun2M Collaborator Loading…
2 tasks
2
bench: review
#39049 opened May 7, 2026 by thorimur Contributor • Draft
5
feat(Algebra/Group/Defs): add positive natural exponentiation for semigroups 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-algebra Algebra (groups, rings, fields, etc)
#39048 opened May 7, 2026 by AydenLamp Loading…
8
feat(Combinatorics/GraphLike): GraphLike with no multi edges blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-combinatorics Combinatorics
#39047 opened May 7, 2026 by Jun2M Collaborator Loading…
1 task
2
ProTip! What’s not been updated in a month: updated:<2026-04-08.