Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,321 Open 34,725 Closed
2,321 Open 34,725 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(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…
1
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
#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: 0 < a → 0 < a + b t-order Order theory
#37641 opened Apr 4, 2026 by vihdzp Loading…
1
feat(Order/RelIso): add lemmas about congruence with relIso t-order Order theory
#37640 opened Apr 4, 2026 by IvanRenison Loading…
1
chore(Analysis/Normed): tag norm_id with simp easy < 20s of review time. See the lifecycle page for guidelines. t-analysis Analysis (normed *, calculus)
#37638 opened Apr 4, 2026 by vasnesterov Loading…
1
feat(Analysis/Calculus/FDeriv): add fderiv_apply simp lemmas 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…
2
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…
1
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…
3
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…
2 tasks
2
chore: use fast_instance% in classes of continuous maps ready-to-merge This PR has been sent to bors. t-topology Topological spaces, uniform spaces, metric spaces, filters
#37629 opened Apr 4, 2026 by sgouezel Loading…
2
chore: Rename Xor' to Xor new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#37628 opened Apr 4, 2026 by JadAbouHawili Loading…
19
refactor(RingTheory/Ideal/Height): torwards private Ideal.primeHeight 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
#37627 opened Apr 4, 2026 by Thmoas-Guan Loading…
1 task
2
feat(Algebra/Algebra/Operations): add Submodule.mul_eq_bot 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)
#37626 opened Apr 4, 2026 by NoahW314 Loading…
3
feat(LinearAlgebra/Matrix/Charpoly): general coefficient formula as sum of principal minors 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)
#37625 opened Apr 3, 2026 by slavanaprienko Loading…
5
feat(Combinatorics/SimpleGraph/Maps): add theorems about composition t-combinatorics Combinatorics
#37624 opened Apr 3, 2026 by IvanRenison Loading…
1
feat(Order/RelIso): add theorems about RelHom.comp and RelEmbedding.trans t-order Order theory
#37623 opened Apr 3, 2026 by IvanRenison Loading…
4
ProTip! Type g p on any issue or pull request to go back to the pull request listing page.