Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,083 Open 28,080 Closed
2,083 Open 28,080 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

chore(Analysis/SpecialFunctions/Log/PosLog): golf a proof using grw easy < 20s of review time. See the lifecycle page for guidelines. maintainer-merge t-analysis Analysis (normed *, calculus)
#30704 opened Oct 19, 2025 by eric-wieser Loading…
3
feat(Geometry/Euclidean/Projection): projection onto sup blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-euclidean-geometry Affine and axiomatic geometry
#30703 opened Oct 19, 2025 by jsm28 Loading…
2 tasks
2
feat(LinearAlgebra/AffineSpace/Independent): inf_affineSpan_eq_affineSpan_inter t-algebra Algebra (groups, rings, fields, etc)
#30702 opened Oct 19, 2025 by jsm28 Loading…
3
feat: Set.prod_image_left t-data Data (lists, quotients, numbers, etc)
#30701 opened Oct 19, 2025 by vihdzp Loading…
1
feat(LinearAlgebra/AffineSpace/AffineSubspace/Defs): nonempty sup awaiting-bench easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields, etc)
#30699 opened Oct 19, 2025 by jsm28 Loading…
4
feat(Geometry/Euclidean/Projection): characteristic property t-euclidean-geometry Affine and axiomatic geometry
#30698 opened Oct 19, 2025 by jsm28 Loading…
12
chore(Algebra/Star/Unitary): fix lemma names easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields, etc)
#30697 opened Oct 19, 2025 by themathqueen Loading…
1
feat(Order/Category): PardOrdEmb has filtering colimits blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-order Order theory WIP Work in progress
#30696 opened Oct 19, 2025 by joelriou Loading…
1 task
2
chore(Analysis/InnerProductSpace/MulOpposite): NormedAddCommGroup -> SeminormedAddCommGroup delegated easy < 20s of review time. See the lifecycle page for guidelines. t-analysis Analysis (normed *, calculus)
#30695 opened Oct 19, 2025 by themathqueen Loading…
8
chore(Analysis/CStarAlgebra/CFC/Order): relate section to strict positivity t-analysis Analysis (normed *, calculus)
#30694 opened Oct 19, 2025 by themathqueen Loading…
1
feat(Order/Category): partial orders with order embeddings as morphisms t-order Order theory
#30693 opened Oct 19, 2025 by joelriou Loading…
2
chore(Algebra/Order/Star/Basic): rename **conjugate** to **conjugate**' t-algebra Algebra (groups, rings, fields, etc)
#30692 opened Oct 19, 2025 by themathqueen Loading…
3
style(misc): fix whitespace
#30691 opened Oct 19, 2025 by grunweg Loading…
1
style(Order): fix whitespace t-order Order theory
#30690 opened Oct 19, 2025 by grunweg Loading…
1
style(Algebra): fix whitespace t-algebra Algebra (groups, rings, fields, etc)
#30688 opened Oct 19, 2025 by grunweg Loading…
1
style(Analysis): fix whitespace maintainer-merge t-analysis Analysis (normed *, calculus)
#30687 opened Oct 19, 2025 by grunweg Loading…
3
tracking: #30658 split into pieces 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
#30686 opened Oct 19, 2025 by grunweg Loading…
1 of 6 tasks
2
style(RingTheory): fix whitespace maintainer-merge t-ring-theory Ring theory
#30685 opened Oct 19, 2025 by grunweg Loading…
4
chore: deprecate monoidalOfHasFiniteProducts awaiting-author A reviewer has asked the author a question or requested changes. large-import Automatically added label for PRs with a significant increase in transitive imports t-category-theory Category theory
#30684 opened Oct 19, 2025 by YaelDillies Loading…
2
chore: use IsAddTorsionFree M instead of NoZeroSMulDivisors ℕ M/NoZeroSMulDivisors ℤ M 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)
#30683 opened Oct 19, 2025 by YaelDillies Loading…
1 task
2
feat(NumberField/Cyclotomic): splitting of the prime p in the p^k-th cyclotomic field t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#30682 opened Oct 19, 2025 by xroblot Loading…
@riccardobrasca
1
feat(Analysis/SpecialFunctions/Log): log_prod for Multiset
#30681 opened Oct 19, 2025 by fbarroero Loading…
4
feat(Algebra/Group/Torsion): characterise when a ^ n = 1 t-algebra Algebra (groups, rings, fields, etc)
#30680 opened Oct 19, 2025 by YaelDillies Loading…
1
feat(LinearAlgebra/TensorProduct/Matrix): equivalence between ⊗ₜ and ⊗ₖ t-algebra Algebra (groups, rings, fields, etc)
#30679 opened Oct 19, 2025 by themathqueen Loading…
1
refactor(Algebra/Quaternion): intermediate Module instance awaiting-author A reviewer has asked the author a question or requested changes. t-algebra Algebra (groups, rings, fields, etc)
#30678 opened Oct 19, 2025 by YaelDillies Loading…
7
ProTip! Add no:assignee to see everything that’s not assigned.