Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
1,638 Open 24,479 Closed
1,638 Open 24,479 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

fix: make CompleteLattice extend BoundedOrder t-order Order theory
#26626 opened Jul 2, 2025 by PierreQuinton Loading…
1
chore: update Mathlib dependencies 2025-07-02 auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. dependency-bump This PR bumps the version of an upstream dependency (but not toolchain). ready-to-merge This PR has been sent to bors.
#26625 opened Jul 2, 2025 by mathlib4-update-dependencies-bot Loading…
3
feat(RingTheory/Valuation/Discrete/Basic): relate DVRs and discrete valuations 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-algebra Algebra (groups, rings, fields, etc)
#26623 opened Jul 2, 2025 by mariainesdff Loading…
1 task
2
chore: golf using subsingleton bench-after-CI Once the PR passes CI, comment `!bench` on the PR
#26621 opened Jul 2, 2025 by euprunin Loading…
6
chore: deprecate Scott in favour of WithScott t-topology Topological spaces, uniform spaces, metric spaces, filters
#26619 opened Jul 2, 2025 by YaelDillies Loading…
1
1
feat: simple lemmas on circle integrability t-analysis Analysis (normed *, calculus) t-measure-probability Measure theory / Probability theory
#26618 opened Jul 2, 2025 by kebekus Loading…
12
feat(Data/Sum/Order): toLex as a RelIso t-data Data (lists, quotients, numbers, etc) t-order Order theory
#26617 opened Jul 2, 2025 by vihdzp Loading…
1
feat(Data/Sum/Order): Equiv.sumCongr as an order isomorphism auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. delegated t-data Data (lists, quotients, numbers, etc) t-order Order theory
#26616 opened Jul 2, 2025 by vihdzp Loading…
11
feat(SimpleGraph): add more API for take/drop t-combinatorics Combinatorics
#26614 opened Jul 2, 2025 by Rida-Hamadani Loading…
1
feat: linear order is isomorphic to lexicographic sum of two intervals blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) delegated t-order Order theory
#26613 opened Jul 2, 2025 by vihdzp Loading…
1 task
5
refactor(SetTheory/Ordinal/Arithmetic): rework Ordinal.pred API maintainer-merge t-set-theory Set theory
#26612 opened Jul 2, 2025 by vihdzp Loading…
3
chore: fix minor docstring mistake LHS → RHS easy < 20s of review time. See the lifecycle page for guidelines. t-order Order theory
#26610 opened Jul 2, 2025 by vihdzp Loading…
1
chore(Aesop): remove aesop apply 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-meta Tactics, attributes or user commands
#26609 opened Jul 2, 2025 by artie2000 Loading…
1 task
2
feat(SetTheory/Cardinal/Aleph): o.card ≤ ℵ_ o and variants t-set-theory Set theory
#26608 opened Jul 2, 2025 by vihdzp Loading…
1
feat(SetTheory/Cardinal/Aleph): characterization of initial successor ordinals t-set-theory Set theory
#26607 opened Jul 2, 2025 by vihdzp Loading…
2
refactor(SetTheory/Cardinal/Regular): review IsInaccessible API t-set-theory Set theory
#26606 opened Jul 2, 2025 by vihdzp Loading…
1
chore: GRewrite typo easy < 20s of review time. See the lifecycle page for guidelines. maintainer-merge t-meta Tactics, attributes or user commands
#26604 opened Jul 2, 2025 by DavidLedvinka Loading…
3
refactor(SetTheory/Ordinal/FixedPoint): redefine Ordinal.deriv t-set-theory Set theory
#26603 opened Jul 1, 2025 by vihdzp Loading…
1
feat: some IsUnit results for Matrix t-algebra Algebra (groups, rings, fields, etc)
#26602 opened Jul 1, 2025 by eric-wieser Loading…
1
feat(CategoryTheory): make Functor.comp irreducible t-category-theory Category theory WIP Work in progress
#26601 opened Jul 1, 2025 by yuma-mizuno • Draft
1
test t-algebraic-geometry Algebraic geometry
#26598 opened Jul 1, 2025 by mattrobball • Draft
1
Update Orthogonal.lean 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)
#26597 opened Jul 1, 2025 by sahanwijetunga Loading…
1
refactor(Probability/ProbabilityMassFunction): Make constructions use NNReal t-measure-probability Measure theory / Probability theory
#26596 opened Jul 1, 2025 by BoltonBailey Loading…
1
feat(Algebra/Polynomial/ZMod): Add Polynomial.equiv_of_nat_of_polynomial_zmod 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)
#26594 opened Jul 1, 2025 by metakunt Loading…
1
feat: add lemma 3.5 from [Geck](https://dx.doi.org/10.1090/proc/13600) t-algebra Algebra (groups, rings, fields, etc) WIP Work in progress
#26592 opened Jul 1, 2025 by ocfnash Loading…
1
ProTip! Mix and match filters to narrow down what you’re looking for.