Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,041 Open 31,500 Closed
2,041 Open 31,500 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: GroupWithZero versions of le lemmas WIP Work in progress
#34120 opened Jan 19, 2026 by winstonyin Loading…
1
feat(Analysis): classical adjacency matrices are quantum adjacency matrices blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-analysis Analysis (normed *, calculus)
#34119 opened Jan 19, 2026 by themathqueen • Draft
1 task
2
refactor(RingTheory/Ideal/AssociatedPrime/Basic): switch definition over to colon t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#34118 opened Jan 18, 2026 by tb65536 Loading…
1
feat(CategoryTheory/Elements): initially small if functor is (co)representable t-category-theory Category theory
#34117 opened Jan 18, 2026 by chrisflav Loading…
1
feat(AlgebraicGeometry): geometric points induce points on the étale site 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-algebraic-geometry Algebraic geometry WIP Work in progress
#34116 opened Jan 18, 2026 by chrisflav Loading…
2 tasks
2
chore: deprecate removed modules
#34115 opened Jan 18, 2026 by Ruben-VandeVelde Loading…
1
feat(Algebra/Algebra/Subalgebra): generalize iSupLift to T ≤ iSup K 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)
#34114 opened Jan 18, 2026 by bilichboris Loading…
1
chore: golf using grind and add grind annotations
#34112 opened Jan 18, 2026 by euprunin Loading…
1
feat(Algebra/Star/LinearMap): the convolutive intrinsic star ring on linear maps t-algebra Algebra (groups, rings, fields, etc)
#34111 opened Jan 18, 2026 by themathqueen Loading…
1
feat(LinearAlgebra/BilinearForm): Harmonize definitions of "Nondegenerate"
#34110 opened Jan 18, 2026 by loefflerd Loading…
1
feat(NumberTheory/FactorizationProperties): Infinite abundant numbers, then golf t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#34109 opened Jan 18, 2026 by metakunt Loading…
6
feat(InformationTheory/Coding): Kraft-McMillan inequality for uniquely decodable codes new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-measure-probability Measure theory / Probability theory
#34108 opened Jan 18, 2026 by elazarg Loading…
19
feat: map a seminorm along a surjective linear map blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot)
#34106 opened Jan 18, 2026 by ADedecker • Draft
2 tasks
2
feat: IsLUB version of [c]sSup_add blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot)
#34105 opened Jan 18, 2026 by ADedecker Loading…
1 task
2
feat: IsLUB versions of [c]sSup_image2_eq_[c]sSup_[c]sSup t-order Order theory
#34104 opened Jan 18, 2026 by ADedecker Loading…
1
chore(Analysis/InnerProductSpace/Orthogonal): add simp attrib, rename t-analysis Analysis (normed *, calculus)
#34103 opened Jan 18, 2026 by yoh-tanimoto Loading…
6
feat(Complex/UnitDisc): add CanLift t-analysis Analysis (normed *, calculus)
#34102 opened Jan 18, 2026 by urkud Loading…
1
feat(AlgebraicGeometry): morphisms of finite type induce essentially of finite type stalk maps t-algebraic-geometry Algebraic geometry
#34101 opened Jan 18, 2026 by chrisflav Loading…
2
feat(Analysis/Distribution): more smulLeftCLM lemmas for tempered distributions t-analysis Analysis (normed *, calculus)
#34100 opened Jan 18, 2026 by mcdoll Loading…
1
feat(Analysis/Distribution): Fourier multiplier 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) WIP Work in progress
#34099 opened Jan 18, 2026 by mcdoll Loading…
1 task
3
chore(MeasureTheory): golf some proofs blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-measure-probability Measure theory / Probability theory
#34098 opened Jan 18, 2026 by CoolRmal Loading…
1 task
2
chore(MeasureTheory): make some arguments implicit easy < 20s of review time. See the lifecycle page for guidelines. t-measure-probability Measure theory / Probability theory
#34097 opened Jan 18, 2026 by CoolRmal Loading…
2
chore(EMetric/*): rename theorems
#34096 opened Jan 18, 2026 by urkud • Draft
1
feat(Data/Finsupp/Single): generalize single_eq_set_indicator easy < 20s of review time. See the lifecycle page for guidelines. 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)
#34095 opened Jan 18, 2026 by IlPreteRosso Loading…
1
feat(Topology/Sheaves): use abbrev for Presheaf, IsSheaf, and 'Sheaf' 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
#34094 opened Jan 18, 2026 by Brian-Nugent Loading…
3
ProTip! no:milestone will show everything without a milestone.