Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
Clear current search query, filters, and sorts
1,185 Open 18,990 Closed
1,185 Open 18,990 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
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

feat: run library_search when the cursor is at a sorry merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-meta Tactics, attributes or user commands
#4109 opened May 19, 2023 by kim-em • Draft
refactor: create HasAdj class, define Digraph, and generalize some SimpleGraph API awaiting-author A reviewer has asked the author a question or requested changes merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-combinatorics Combinatorics
#4127 opened May 20, 2023 by kmill Loading…
feat: Backtrack minimize merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-meta Tactics, attributes or user commands
#4771 opened Jun 7, 2023 by thorimur • Draft
feat: SubExpr utilities merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-meta Tactics, attributes or user commands WIP Work in progress
#4775 opened Jun 7, 2023 by thorimur • Draft
feat: AppBuilder utils t-meta Tactics, attributes or user commands
#4786 opened Jun 7, 2023 by thorimur • Draft
chore: use open scoped awaiting-CI merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)
#4960 opened Jun 10, 2023 by eric-wieser Loading…
feat: IntermediateField adjoin syntax for sets of elements merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-algebra Algebra (groups, rings, fields, etc) WIP Work in progress
#5133 opened Jun 16, 2023 by kmill Loading…
feat(Analysis.Distribution.ContDiffMapSupportedIn): space of smooth maps with support in a fixed compact merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-analysis Analysis (normed *, calculus) WIP Work in progress
#5912 opened Jul 14, 2023 by ADedecker Loading…
feat: port Data.Rat.MetaDefs help-wanted The author needs attention to resolve issues mathlib-port This is a port of a theory file from mathlib. merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-meta Tactics, attributes or user commands
#5934 opened Jul 15, 2023 by eric-wieser Loading…
4
feat: add APIs about Quotient.choice awaiting-author A reviewer has asked the author a question or requested changes merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) RFC Request for comment t-data Data (lists, quotients, numbers, etc)
#5995 opened Jul 19, 2023 by FR-vdash-bot Loading…
@eric-wieser
4
fix: deduplicate variables awaiting-CI merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)
#6079 opened Jul 23, 2023 by eric-wieser Loading…
1
refactor(Data/Finsupp/Defs): make Finsupp.single defeq to Pi.single merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) WIP Work in progress
#6317 opened Aug 2, 2023 by eric-wieser Loading…
chore(Mathlib/Algebra/Hom/GroupAction): add SMulHomClass.comp_smul merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-algebra Algebra (groups, rings, fields, etc)
#6491 opened Aug 10, 2023 by eric-wieser Loading…
feat: discrete Fourier transform of a finite sequence awaiting-author A reviewer has asked the author a question or requested changes merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-algebra Algebra (groups, rings, fields, etc)
#6517 opened Aug 11, 2023 by MohanadAhmed Loading…
27
WIP: feat(GroupTheory/GroupAction/Basic): add pointwise and setwise stabilizers merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-algebra Algebra (groups, rings, fields, etc) WIP Work in progress
#6533 opened Aug 11, 2023 by wupr • Draft
chore: move_add-driven replacements awaiting-author A reviewer has asked the author a question or requested changes merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)
#6580 opened Aug 14, 2023 by adomani Loading…
feat(Algebra/MonoidAlgebra/NoZeroDivisors): NoZeroDivisors instance on AddMonoidAlgebras awaiting-author A reviewer has asked the author a question or requested changes merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-algebra Algebra (groups, rings, fields, etc)
#6627 opened Aug 17, 2023 by adomani Loading…
14
feat: Reduced Spectral Theorem merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-algebra Algebra (groups, rings, fields, etc) WIP Work in progress
#6630 opened Aug 17, 2023 by MohanadAhmed Loading…
refactor: Use flat structures for morphisms awaiting-author A reviewer has asked the author a question or requested changes awaiting-CI help-wanted The author needs attention to resolve issues merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)
#6791 opened Aug 25, 2023 by eric-wieser Loading…
TryLean4Bundle: Windows Bundle Creator CI Modifies the continuous integration / deployment setup help-wanted The author needs attention to resolve issues WIP Work in progress
#6859 opened Aug 29, 2023 by MohanadAhmed Loading…
feat: resynth_instances tactic for resynthesizing instances in the goal or local context merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-meta Tactics, attributes or user commands WIP Work in progress
#6930 opened Sep 3, 2023 by kmill Loading…
refactor(Analysis/Normed*): use RingHomIsometric for *.norm_cast help-wanted The author needs attention to resolve issues merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-analysis Analysis (normed *, calculus)
#6931 opened Sep 3, 2023 by urkud Loading…
some random stuff merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)
#7225 opened Sep 17, 2023 by jjaassoonn • Draft
6
feat: synthetic geometry awaiting-author A reviewer has asked the author a question or requested changes help-wanted The author needs attention to resolve issues t-euclidean-geometry Affine and axiomatic geometry
#7300 opened Sep 21, 2023 by ah1112 Loading…
71
chore: use preimageIso instead of defeq abuse for InducedCategory awaiting-CI merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-category-theory Category theory
#7325 opened Sep 22, 2023 by eric-wieser Loading…
ProTip! Add no:assignee to see everything that’s not assigned.