Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,310 Open 34,747 Closed
2,310 Open 34,747 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(NumberTheory/ArithmeticStatistics/Reducible): Counting reducible polynomials
#37663 opened Apr 5, 2026 by khwilson • Draft
1
feat(Algebra/Category/ModuleCat/Presheaf): the adjunction between colimitFunctor and constFunctor t-algebra Algebra (groups, rings, fields, etc) t-category-theory Category theory
#37662 opened Apr 5, 2026 by joelriou Loading…
1
feat(Algebra/Lie/Sl2): add lemma exists_primitiveVector large-import Automatically added label for PRs with a significant increase in transitive imports 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)
#37661 opened Apr 5, 2026 by pion2024 Loading…
2
feat(MvPolynomial): add Hasse derivatives new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#37660 opened Apr 5, 2026 by eliasjudin Loading…
2
feat(AlgebraicTopology): relative singular homology
#37659 opened Apr 5, 2026 by erdOne Loading…
2
chore(AlgebraicTopology): rename SingularHomology.HomotopyInvarianceTopCat 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-algebraic-topology Algebraic topology WIP Work in progress
#37658 opened Apr 5, 2026 by joelriou Loading…
1 task
3
chore(MeasureTheory/Measure/MeasureSpace): reduce privateInPublic t-measure-probability Measure theory / Probability theory tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#37657 opened Apr 5, 2026 by Komyyy Loading…
1
feat(AlgebraicTopology): simplicial homology file-removed A Lean module was (re)moved without a `deprecated_module` annotation t-algebraic-topology Algebraic topology
#37656 opened Apr 5, 2026 by joelriou Loading…
1
chore: expand docstrings to explain the meaning of C^n and C^ω delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-differential-geometry Manifolds etc
#37655 opened Apr 5, 2026 by sgouezel Loading…
7
feat(ProbabilityTheory/MeasureTheorey): Add Coupling lemma t-measure-probability Measure theory / Probability theory
#37652 opened Apr 5, 2026 by yuanyi-350 Loading…
1
feat(Data): add theorem Finset.image_eq_iff_eq_preimage t-data Data (lists, quotients, numbers, etc)
#37649 opened Apr 4, 2026 by IvanRenison Loading…
2
chore: make argument in bddAbove_of_small implicit awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-set-theory Set theory
#37648 opened Apr 4, 2026 by vihdzp Loading…
1
feat(Logic): surjective embeddings are equivs t-logic Logic (model theory, etc)
#37646 opened Apr 4, 2026 by SnirBroshi Loading…
1
feat(CategoryTheory/Limits): sigmaConst preserves colimits t-category-theory Category theory
#37645 opened Apr 4, 2026 by joelriou Loading…
@robin-carlier
1
feat(Order/Causal): add Causal ordering for stream functions new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-order Order theory
#37644 opened Apr 4, 2026 by matthunz • Draft
2
feat(CStarAlgebra): x ↦ x ^ p is operator concave for p ∈ [0, 1] t-analysis Analysis (normed *, calculus)
#37643 opened Apr 4, 2026 by dupuisf Loading…
1
chore(Combinatorics/SimpleGraph): tidy various files t-combinatorics Combinatorics
#37642 opened Apr 4, 2026 by SnirBroshi Loading…
2
feat(Order/RelIso): add lemmas about congruence with relIso t-order Order theory
#37640 opened Apr 4, 2026 by IvanRenison Loading…
1
feat(Analysis/Calculus/FDeriv): add fderiv_apply simp lemmas awaiting-author A reviewer has asked the author a question or requested changes. 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-analysis Analysis (normed *, calculus)
#37637 opened Apr 4, 2026 by IlPreteRosso Loading…
3
feat(Combinatorics/SimpleGraph/Copy): a graph is inducingly contained in another iff it's equivalent to an induced graph t-combinatorics Combinatorics
#37636 opened Apr 4, 2026 by SnirBroshi Loading…
1
chore(Analysis/Analytic): tag ofScalars_norm_eq_mul with simp easy < 20s of review time. See the lifecycle page for guidelines. t-analysis Analysis (normed *, calculus)
#37635 opened Apr 4, 2026 by vasnesterov Loading…
3
chore(CI): check all lean scripts build successfully blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) CI Modifies the continuous integration setup or other automation
#37634 opened Apr 4, 2026 by grunweg Loading…
1 task
3
feat(MvPowerSeries): add some equivs and lemmas large-import Automatically added label for PRs with a significant increase in transitive imports t-ring-theory Ring theory
#37633 opened Apr 4, 2026 by WenrongZou Loading…
1
feat: add Function.prod and Function.diag t-logic Logic (model theory, etc)
#37631 opened Apr 4, 2026 by linesthatinterlace Loading…
4
feat(AlgebraicTopology): homology in degree 0 blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-algebraic-topology Algebraic topology WIP Work in progress
#37630 opened Apr 4, 2026 by joelriou Loading…
3 tasks
2
ProTip! Mix and match filters to narrow down what you’re looking for.