Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,340 Open 34,845 Closed
2,340 Open 34,845 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/MvPolynomial/Variables): add some lemmas about vars 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)
#37791 opened Apr 8, 2026 by SnkXyx Loading…
2
chore: remove duplicate variable declaration easy < 20s of review time. See the lifecycle page for guidelines. maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-order Order theory
#37790 opened Apr 8, 2026 by Parcly-Taxel Loading…
3
feat(NumberTheory/ModularForms): level one dimension formula t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#37789 opened Apr 8, 2026 by CBirkbeck • Draft
23
refactor: golf proofs in AdicCompletion/LocalRing t-ring-theory Ring theory
#37788 opened Apr 8, 2026 by yuanyi-350 Loading…
6
feat(Topology/UniformSpace): IndiscreteTopology on a UniformSpace t-topology Topological spaces, uniform spaces, metric spaces, filters
#37787 opened Apr 8, 2026 by NoahW314 Loading…
2
feat: add ContinuousMul instance on Icc 0 1 t-topology Topological spaces, uniform spaces, metric spaces, filters
#37786 opened Apr 8, 2026 by NoahW314 Loading…
@eric-wieser
1
chore: Golf proofs in FDeriv/Symmetric and DominatedConvergence easy < 20s of review time. See the lifecycle page for guidelines.
#37785 opened Apr 8, 2026 by yuanyi-350 Loading…
2
feat(Order/ConditionallyCompleteLattice/Basic): ConditionallyCompleteLinearOrderBot (WithBot α) t-order Order theory
#37784 opened Apr 8, 2026 by SnirBroshi Loading…
1
bench: batteries#1754 dependency-bump This PR bumps the version of an upstream dependency (but not toolchain).
#37782 opened Apr 8, 2026 by thorimur • Draft
3
chore(Topology/Order/SuccPred): use to_dual blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot)
#37781 opened Apr 8, 2026 by vihdzp Loading…
1 task
2
chore(Topology/Order/Basic): use to_dual blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot)
#37780 opened Apr 8, 2026 by vihdzp Loading…
1 task
2
feat(Data/FunLike): introduce typeclasses for algebraic properties of FunLike t-data Data (lists, quotients, numbers, etc)
#37779 opened Apr 8, 2026 by mcdoll Loading…
1
chore: remove unneeded to_dual existing maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-order Order theory
#37778 opened Apr 7, 2026 by vihdzp Loading…
4
doc(1000.yaml): update authors for Sprague-Grundy documentation Improvements or additions to documentation
#37777 opened Apr 7, 2026 by vihdzp Loading…
1
feat(CategoryTheory/Sites): Over.post F preserves covers if F does t-category-theory Category theory
#37775 opened Apr 7, 2026 by chrisflav Loading…
1
fix: change variables in bicompl to Sort* and add missing theorem mentioned in bicompl docs new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-logic Logic (model theory, etc)
#37774 opened Apr 7, 2026 by weisbrja Loading…
5
chore(Algebra/Category): add ModuleCat.restrictScalarsIsoOfEquiv t-algebra Algebra (groups, rings, fields, etc)
#37773 opened Apr 7, 2026 by chrisflav Loading…
1
chore(Order/OrdContinuous): dualize maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#37772 opened Apr 7, 2026 by SabrinaJewson Loading…
1 task done
10
feat(AlgebraicGeometry/EllipticCurve/LFunction): define the L-Function of an elliptic curve t-algebra Algebra (groups, rings, fields, etc) t-algebraic-geometry Algebraic geometry t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#37771 opened Apr 7, 2026 by tb65536 Loading…
1
feat(NumberTheory/ArithmeticFunction/LFunction): an euler product of power series is the limit of the euler products t-algebra Algebra (groups, rings, fields, etc) t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#37770 opened Apr 7, 2026 by tb65536 Loading…
1
Test a modification of #36613
#37769 opened Apr 7, 2026 by JovanGerb Loading…
2
doc(1000.yml): Church–Rosser theorem
#37768 opened Apr 7, 2026 by chenson2018 Loading…
3
feat(NumberTheory/ArithmeticFunction/LFunction): ofPowerSeries produces multiplicative power series t-algebra Algebra (groups, rings, fields, etc) t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#37767 opened Apr 7, 2026 by tb65536 Loading…
1
feat(AlgebraicGeometry): restriction of quasi-coherent sheaf is quasi-coherent 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
#37766 opened Apr 7, 2026 by chrisflav Loading…
2 tasks
2
chore(Tactic): rewrite qify and zify tactic docstrings documentation Improvements or additions to documentation t-meta Tactics, attributes or user commands
#37765 opened Apr 7, 2026 by Vierkantor Loading…
@dwrensha
1
ProTip! What’s not been updated in a month: updated:<2026-03-08.