Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
3,065 Open 39,869 Closed
3,065 Open 39,869 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: make a few lemmas using in RingHomClass definitions take in a concrete morphism awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#43585 opened Sep 8, 2026 by grunweg Contributor Loading…
1
chore(Order/Interval/Set/Image): use to_dual auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. t-order Order theory
#43584 opened Sep 8, 2026 by SnirBroshi Collaborator Loading…
1
chore(Algebra/QuadraticAlgebra): define natCast and intCast without C t-algebra Algebra (groups, rings, fields, etc) WIP Work in progress
#43583 opened Sep 8, 2026 by xroblot Collaborator Loading…
7
feat(AffineSpace): toAffineSubspace lemmas t-algebra Algebra (groups, rings, fields, etc)
#43582 opened Sep 8, 2026 by vlad902 Collaborator Loading…
3
refactor(Data/Nat/Factorization/Defs): redefine Nat.factorization in terms of primeFactorsList instead of padicValNat t-algebra Algebra (groups, rings, fields, etc) t-data Data (lists, quotients, numbers, etc) t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#43581 opened Sep 8, 2026 by tb65536 Contributor Loading…
5
feat: attaching additive valuations to valuations with usable targets blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot)
#43580 opened Sep 8, 2026 by WilliamCoram Collaborator Loading…
1 task
2
refactor: make several NonUnitalAlgHom definitions take a particular algebra homomorphism awaiting-author Reply -awaiting-author to remove the label on your PR once you have addressed all comments. t-algebra Algebra (groups, rings, fields, etc) tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#43579 opened Sep 8, 2026 by grunweg Contributor Loading…
7
feat: identifying WithZero (Multiplicative M) and WithTop M LLM-generated PRs with substantial input from LLMs - review accordingly
#43578 opened Sep 8, 2026 by WilliamCoram Collaborator Loading…
1
chore(Order/BooleanAlgebra): Add push tags new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-order Order theory
#43577 opened Sep 8, 2026 by javgomzar Contributor Loading…
3
chore: rename CoAlg{Hom,Equiv}Class.toCoAlg{Hom,Equiv} as CoAlg{Hom,Equiv}.ofClass 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)
#43576 opened Sep 8, 2026 by grunweg Contributor Loading…
1 task
1
feat: char two API (WIP) t-group-theory Group theory
#43575 opened Sep 8, 2026 by harahu Contributor • Draft
1
refactor(RingTheory/Multiplicity): switch multiplicity to have junk value of 0 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 tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#43573 opened Sep 8, 2026 by tb65536 Contributor Loading…
3
chore(CategoryTheory/Limits/Shapes/BinaryProducts): use to_dual t-category-theory Category theory tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip WIP Work in progress
#43571 opened Sep 8, 2026 by JovanGerb Contributor Loading…
1
refactor(AlgebraicGeometry/Modules): transport pushforward along Opens.map functoriality isos tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#43570 opened Sep 8, 2026 by kim-em Contributor Loading…
1
refactor(ModuleCat): state pushforward coherence without identifying functor bracketings tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#43569 opened Sep 8, 2026 by kim-em Contributor Loading…
1
refactor(CategoryTheory/Limits): use compEvaluation in limitIsoFlipCompLim awaiting-author Reply -awaiting-author to remove the label on your PR once you have addressed all comments. t-category-theory Category theory
#43568 opened Sep 8, 2026 by kim-em Contributor Loading…
2
refactor(CategoryTheory): insert missing Functor.op compatibility isomorphisms
#43567 opened Sep 8, 2026 by kim-em Contributor Loading…
1
refactor(CategoryTheory): insert missing functor associators and unitors tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#43566 opened Sep 8, 2026 by kim-em Contributor Loading…
3
refactor(Archive/FriendshipGraphs): golf everything tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#43565 opened Sep 8, 2026 by Parcly-Taxel Collaborator Loading…
7
chore(RepresentationTheory): remove redundant import easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields, etc)
#43564 opened Sep 8, 2026 by JX-Mo Contributor Loading…
2
feat(Tactic): add multiplication support for inclusion/dyadic_interval tactics large-import Automatically added label for PRs with a significant increase in transitive imports ready-to-merge This PR has been sent to bors.
#43563 opened Sep 8, 2026 by DavidLedvinka Collaborator Loading…
3
feat(MeasureTheory/Integral/Bochner/Set): add setIntegral_union' carleson part of the ongoing formalization of Carleson's theorem easy < 20s of review time. See the lifecycle page for guidelines. t-measure-probability Measure theory / Probability theory
#43562 opened Sep 8, 2026 by lakesare Contributor Loading…
3
wip: make RingHom.ker and friends take in a concrete morphism instead blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-ring-theory Ring theory WIP Work in progress
#43561 opened Sep 7, 2026 by grunweg Contributor Loading…
1 task
3
feat(Topology/Sets): add Compacts.singleton_le_iff easy < 20s of review time. See the lifecycle page for guidelines. t-topology Topological spaces, uniform spaces, metric spaces, filters
#43560 opened Sep 7, 2026 by gasparattila Contributor Loading…
2
feat(NumberTheory/ModularForms): mean square bound for q-expansions large-import Automatically added label for PRs with a significant increase in transitive imports LLM-generated PRs with substantial input from LLMs - review accordingly t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#43558 opened Sep 7, 2026 by loefflerd Contributor Loading…
18
ProTip! Type g p on any issue or pull request to go back to the pull request listing page.