Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,420 Open 35,296 Closed
2,420 Open 35,296 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(RingTheory/AdicCompletion): make AdicCompletion.map linear on linear maps t-ring-theory Ring theory
#38324 opened Apr 21, 2026 by BryceT233 Contributor Loading…
1
feat(RingTheory/MvPolynomial/MonomialOrder): remove unnecessary hypothesis t-ring-theory Ring theory
#38323 opened Apr 21, 2026 by NoahW314 Contributor Loading…
1
feat(Algebra/MvPolynomial): add monomial prod lemma t-algebra Algebra (groups, rings, fields, etc)
#38322 opened Apr 21, 2026 by NoahW314 Contributor Loading…
2
Tag absolute value lemmas with @[push] t-algebra Algebra (groups, rings, fields, etc)
#38321 opened Apr 21, 2026 by ldct Collaborator • Draft
1 of 2 tasks
1
chore: Tag floor lemmas t-algebra Algebra (groups, rings, fields, etc)
#38320 opened Apr 21, 2026 by ldct Collaborator Loading…
1
feat(Combinatorics/SetFamily): Assouad's dual VC bound new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-combinatorics Combinatorics
#38319 opened Apr 20, 2026 by Zetetic-Dhruv Loading…
5
feat(GRewrite): new grw implementation
#38318 opened Apr 20, 2026 by JovanGerb Contributor • Draft
2
feat(Date/Choose): add some lemmas about choose of prime pow t-data Data (lists, quotients, numbers, etc)
#38317 opened Apr 20, 2026 by WenrongZou Contributor Loading…
1
feat(Order/OmegaCompletePartialOrder): least fixed point and Scott induction new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#38316 opened Apr 20, 2026 by tannerduve Collaborator Loading…
2
try t-algebra Algebra (groups, rings, fields, etc)
#38315 opened Apr 20, 2026 by sgouezel Contributor • Draft
3
feat(CategoryTheory/Monoidal): tensorμ_braid_swap and tensor-product IsCommComonObj new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-category-theory Category theory
#38314 opened Apr 20, 2026 by pedroscortes Loading…
2
feat: warn on deprecated declarations in scripts/check-yaml CI Modifies the continuous integration setup or other automation
#38313 opened Apr 20, 2026 by thorimur Contributor Loading…
1 task done
2
feat(FinitelyPresentedGroup): Additivise definitions and add ℤ instance merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-group-theory Group theory
#38311 opened Apr 20, 2026 by homeowmorphism Contributor • Draft
1
feat(Combinatorics/Quiver/Schreier): word evaluation and reachability 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-combinatorics Combinatorics
#38310 opened Apr 20, 2026 by ZRTMRH Contributor Loading…
2
feat(Algebra/NonAssoc): dendriform algebras 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)
#38309 opened Apr 20, 2026 by ntapiam Contributor Loading…
3
feat(Algebra/Colimit/DirectLimit): add star structures (Star, StarRing, etc.) on DirectLimit 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)
#38308 opened Apr 20, 2026 by drocta Loading…
10
chore(LinearAlgebra/Matrix): deprecate Matrix.star_mul easy < 20s of review time. See the lifecycle page for guidelines. merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc) tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#38307 opened Apr 20, 2026 by Vierkantor Contributor Loading…
8
chore: remove a redundant instance on trees in set theory t-set-theory Set theory
#38302 opened Apr 20, 2026 by sgouezel Contributor Loading…
1
feat(Algebra/Group/Commutator): tag addCommutatorElement as a scoped instance maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-algebra Algebra (groups, rings, fields, etc)
#38301 opened Apr 20, 2026 by SnirBroshi Collaborator Loading…
6
chore(CategoryTheory): remove unnecessary conditions in Mathlib/CategoryTheory/Limits/Shapes/Opposites/Equalizers t-category-theory Category theory
#38298 opened Apr 20, 2026 by yuanyi-350 Collaborator Loading…
1
chore: fix double conflicting instances of OmegaCompletePartialOrder on CompleteLattice t-order Order theory
#38297 opened Apr 20, 2026 by sgouezel Contributor Loading…
1
feat(MeasureTheory/LpSpace): Isometric embedding L∞ → (L¹)* new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-measure-probability Measure theory / Probability theory
#38296 opened Apr 20, 2026 by mike1729 Contributor Loading…
@kex-y
4
feat(MeasureTheory/LpSpace): isometric equivalence L∞ → (L¹)* new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#38295 opened Apr 20, 2026 by mike1729 Contributor • Draft
2
chore(Tactic): rewrite subsingleton tactic docstring documentation Improvements or additions to documentation t-meta Tactics, attributes or user commands
#38294 opened Apr 20, 2026 by Vierkantor Contributor Loading…
@JovanGerb
1
chore(Tactic): rewrite split_ifs tactic docstring documentation Improvements or additions to documentation t-meta Tactics, attributes or user commands
#38293 opened Apr 20, 2026 by Vierkantor Contributor Loading…
@JovanGerb
1
ProTip! Adding no:label will show everything without a label.