Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,828 Open 38,157 Closed
2,828 Open 38,157 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(SimpleGraph/Trails): a walk is Eulerian iff it is a trail of length G.edgeSet.encard large-import Automatically added label for PRs with a significant increase in transitive imports t-combinatorics Combinatorics
#41623 opened Jul 11, 2026 by SnirBroshi Collaborator Loading…
1
feat(Order): add subset_Icc_iff and Set.OrdConnected.eq_Icc new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-order Order theory
#41622 opened Jul 11, 2026 by benjub Loading…
2
draft(AlgebraicGeometry): Conditional Riemann-Roch merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)
#41621 opened Jul 11, 2026 by Raph-DG Collaborator • Draft
fix(GRewrite): preserve binder names in a forall t-meta Tactics, attributes or user commands
#41620 opened Jul 11, 2026 by JovanGerb Contributor Loading…
1
fix(Order/Notation): unify at correct transparency in sup/inf delaborators t-order Order theory
#41619 opened Jul 11, 2026 by JovanGerb Contributor Loading…
1
chore(Order/Relseries): cleaning up a proof t-order Order theory
#41618 opened Jul 11, 2026 by joelriou Contributor Loading…
3
feat(Order/Fin): conditions for Fin.insertNth to be monotone or strictly monotone t-order Order theory
#41617 opened Jul 11, 2026 by joelriou Contributor Loading…
1
feat(RepresentationTheory): add instance Abelian (Rep k G) in Rep.Basic 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)
#41616 opened Jul 11, 2026 by JX-Mo Loading…
2
chore: replace haveI/letI with have/let in tactic proofs of propositions
#41615 opened Jul 11, 2026 by kbuzzard Member Loading…
8
feat(RingTheory/Algebraic): tower law for Module.finrank over domains t-ring-theory Ring theory
#41614 opened Jul 11, 2026 by xroblot Collaborator Loading…
@riccardobrasca
4
feat(ModularForm): add eisensteinSeries G_k^v large-import Automatically added label for PRs with a significant increase in transitive imports
#41613 opened Jul 11, 2026 by WenrongZou Collaborator • Draft
2
feat: Commute and IsCoprime are Std.Symm t-ring-theory Ring theory
#41612 opened Jul 11, 2026 by SnirBroshi Collaborator Loading…
1
chore(Data/Seq/Computation): golf using grind awaiting-author A reviewer has asked the author a question or requested changes. t-data Data (lists, quotients, numbers, etc)
#41611 opened Jul 11, 2026 by SnirBroshi Collaborator Loading…
3
chore(Logic/Relation): golf using grind awaiting-author A reviewer has asked the author a question or requested changes. t-logic Logic (model theory, etc)
#41610 opened Jul 11, 2026 by SnirBroshi Collaborator Loading…
6
feat(Data/List/Dedup): dedup and Nodup lemmas t-data Data (lists, quotients, numbers, etc)
#41609 opened Jul 11, 2026 by SnirBroshi Collaborator Loading…
1
chore(RingTheory/Polynomial/Basic): remove unused haveI and defeq abuse easy < 20s of review time. See the lifecycle page for guidelines. maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-ring-theory Ring theory tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#41608 opened Jul 11, 2026 by mbkybky Collaborator Loading…
3
chore(RingTheory/DedekindDomain): update definitions t-ring-theory Ring theory
#41607 opened Jul 11, 2026 by mbkybky Collaborator Loading…
1
feat(NumberTheory/Height/NumberField): comparison of heights across extensions of number fields awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-algebra Algebra (groups, rings, fields, etc) t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#41606 opened Jul 10, 2026 by tb65536 Contributor Loading…
3 tasks
2
feat(NumberTheory/Height/NumberField): the absolute height of an algebraic number t-algebra Algebra (groups, rings, fields, etc) t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#41605 opened Jul 10, 2026 by tb65536 Contributor Loading…
1
feat(NumberTheory/NumberField/Completion/FinitePlace): compatibility of finite places across an algebra map t-algebra Algebra (groups, rings, fields, etc) t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#41604 opened Jul 10, 2026 by tb65536 Contributor Loading…
1
WIP: feat(AlgebraicTopology): Fundamental groupoid functor is a cosheaf (Seifert–van Kampen) LLM-generated PRs with substantial input from LLMs - review accordingly t-algebraic-topology Algebraic topology WIP Work in progress
#41603 opened Jul 10, 2026 by hanwenzhu Collaborator • Draft
1
feat: constructions of Fredholm operators blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) WIP Work in progress
#41602 opened Jul 10, 2026 by ADedecker Member Loading…
1 task
2
feat: composition of Fredholm operators blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot)
#41601 opened Jul 10, 2026 by ADedecker Member Loading…
1 task
2
feat(NumberTheory/NumberField/Completion/Ramification): add InfinitePlace.mult_mul_finrank t-algebra Algebra (groups, rings, fields, etc) t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#41600 opened Jul 10, 2026 by tb65536 Contributor Loading…
1
WIP: inline noncomputable sections merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) WIP Work in progress
#41599 opened Jul 10, 2026 by felixpernegger Contributor • Draft
13
ProTip! Adding no:label will show everything without a label.