-
Notifications
You must be signed in to change notification settings - Fork 626
Pull requests: leanprover-community/mathlib4
Author
Label
Projects
Milestones
Reviews
Assignee
Sort
Pull requests list
chore: golf using 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
grw
blocked-by-other-PR
#26981
opened Jul 10, 2025 by
JovanGerb
Loading…
1 task
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…
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…
chore: remove 3 (of 12) direct imports of
Mathlib.Tactic.NormNum by using grind
#26977
opened Jul 10, 2025 by
euprunin
Loading…
refactor(Order/Concept): rename Order theory
intentClosure → lowerPolar
t-order
#26976
opened Jul 10, 2025 by
vihdzp
Loading…
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…
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
feat(CategoryTheory): localization of quotient categories
t-category-theory
Category theory
#26972
opened Jul 10, 2025 by
joelriou
Loading…
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
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
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…
feat(Data/Nat/Fib/Basic): some API for This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
t-data
Data (lists, quotients, numbers, etc)
Nat.fib
new-contributor
#26962
opened Jul 10, 2025 by
themathqueen
Loading…
feat(RingTheory/PowerSeries/Substitution): add API
t-algebra
Algebra (groups, rings, fields, etc)
#26961
opened Jul 10, 2025 by
mariainesdff
Loading…
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
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
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
feat(RingTheory/DividedPowers/Basic): add divided power structure on pZp
#26956
opened Jul 10, 2025 by
mariainesdff
Loading…
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…
chore: use Measure theory / Probability theory
edist instead of dist in TendstoInMeasure
t-measure-probability
#26954
opened Jul 10, 2025 by
RemyDegenne
Loading…
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
chore: remove 11 (of 37) direct imports of
Mathlib.Tactic.Ring by using grind
#26951
opened Jul 9, 2025 by
euprunin
Loading…
Primitives of holomorphic functions and path integral
blocked-by-other-PR
This PR depends on another PR (this label is automatically managed by a bot)
merge-conflict
The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)
t-analysis
Analysis (normed *, calculus)
t-topology
Topological spaces, uniform spaces, metric spaces, filters
WIP
Work in progress
#26950
opened Jul 9, 2025 by
alreadydone
•
Draft
3 tasks
Previous Next
ProTip!
Type g p on any issue or pull request to go back to the pull request listing page.