Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,426 Open 35,975 Closed
2,426 Open 35,975 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(Algebra/Colimit/DirectLimit): nonunital algebra instances t-algebra Algebra (groups, rings, fields, etc)
#39017 opened May 7, 2026 by eric-wieser Member Loading…
1
chore: deprecate WithZero.zero_le t-algebra Algebra (groups, rings, fields, etc)
#39016 opened May 6, 2026 by vihdzp Collaborator Loading…
1
chore(Order/SuccPred/LinearLocallyFinite): no expose t-order Order theory
#39015 opened May 6, 2026 by vihdzp Collaborator Loading…
1
feat(Order/SuccPred/LinearLocallyFinite): StrictMono toZ t-order Order theory
#39014 opened May 6, 2026 by vihdzp Collaborator Loading…
1
chore(*): small fixes for backward.inferInstanceAs tech debt tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#39012 opened May 6, 2026 by Vierkantor Contributor Loading…
1
chore(Algebra/Polynomial/Module): workaround for backward.inferInstanceAs t-algebra Algebra (groups, rings, fields, etc) tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#39011 opened May 6, 2026 by Vierkantor Contributor Loading…
1
feat: set dsimp := false in @[to_app]
#39009 opened May 6, 2026 by JovanGerb Contributor Loading…
1
feat(NumberTheory/NumberField/Completion/FinitePlace): add multiplicity lemmas blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#39008 opened May 6, 2026 by MichaelStollBayreuth Contributor Loading…
1 task
2
feat(Algebra/Field/Subfield/Basic): add definition of finitely generated fields t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#39006 opened May 6, 2026 by tb65536 Contributor Loading…
1
fix(Topology/Category): make TopCat.Hom constructor private t-category-theory Category theory t-topology Topological spaces, uniform spaces, metric spaces, filters
#39005 opened May 6, 2026 by dagurtomas Contributor Loading…
1
chore(ModelTheory): fix hypo of realize_liftAt t-logic Logic (model theory, etc)
#39004 opened May 6, 2026 by zhuyizheng Contributor Loading…
3
chore: avoid declaring duplicate instances LE String and LT String t-data Data (lists, quotients, numbers, etc)
#39003 opened May 6, 2026 by TwoFX Member Loading…
2
RFC: don't expose definitions of immersions t-differential-geometry Manifolds etc
#39002 opened May 6, 2026 by grunweg Contributor Loading…
@ocfnash
3
feat(NumberTheory/ModularForms): Sturm bound for finite-index subgroups (WIP) blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) file-removed A Lean module was (re)moved without a `deprecated_module` annotation t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#39000 opened May 6, 2026 by CBirkbeck Collaborator • Draft
1 task
2
feat(Algebra/Homology): homology sequence and acyclic complexes t-algebra Algebra (groups, rings, fields, etc) t-category-theory Category theory
#38999 opened May 6, 2026 by joelriou Contributor Loading…
1
feat(AlgebraicTopology/ModelCategory): precylinders in full subcategories t-algebraic-topology Algebraic topology
#38998 opened May 6, 2026 by joelriou Contributor Loading…
1
feat(Algebra/Homology): the homotopy fiber and the path object blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-category-theory Category theory
#38997 opened May 6, 2026 by joelriou Contributor Loading…
1 task
2
feat(CategoryTheory/Limits): biprod.opIso t-category-theory Category theory
#38996 opened May 6, 2026 by joelriou Contributor Loading…
1
feat(to_additive): support (attr := reassoc)
#38994 opened May 6, 2026 by JovanGerb Contributor Loading…
3
feat(NumberTheory/ModularForms): Sturm bound for level-1 modular forms blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) file-removed A Lean module was (re)moved without a `deprecated_module` annotation LLM-generated PRs with substantial input from LLMs - review accordingly t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#38993 opened May 6, 2026 by CBirkbeck Collaborator • Draft
1 task
6
feat(Order/WellFounded): the minimum of f '' s is f applied to the minimum of s t-order Order theory
#38992 opened May 6, 2026 by SnirBroshi Collaborator Loading…
4
chore(NumberTheory/ModularForms): deprecation shims for moved level-one files blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#38991 opened May 6, 2026 by CBirkbeck Collaborator • Draft
1 task
2
chore(Algebra/DirectSum): workaround for backward.inferInstanceAs t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#38990 opened May 6, 2026 by Vierkantor Contributor Loading…
1
chore: remove (d)simp only []
#38989 opened May 6, 2026 by grunweg Contributor Loading…
4
feat(CategoryTheory/Triangulated): definition of localising subcategories t-category-theory Category theory
#38987 opened May 6, 2026 by joelriou Contributor Loading…
1
ProTip! Mix and match filters to narrow down what you’re looking for.