Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
Clear current search query, filters, and sorts
6 Open 33 Closed
6 Open 33 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(LinearAlgebra/QuadraticForm/Basis): basis expansion of a quadratic map t-algebra Algebra (groups, rings, fields, etc)
#18578 opened Nov 3, 2024 by mans0954 Loading…
@eric-wieser
17
feat(GroupTheory/GroupAction): instance MulAction (β ⧸ H) α 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-algebra Algebra (groups, rings, fields, etc)
#11212 opened Mar 7, 2024 by shuxuezhuyi Loading…
@eric-wieser
6
feat(LinearAlgebra/{ExteriorPower,LinearIndependent,TensorPower}): define the exterior powers of a module and prove some of their basic properties blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) large-import Automatically added label for PRs with a significant increase in transitive imports merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) please-adopt Inactive PR (would be valuable to adopt) t-algebra Algebra (groups, rings, fields, etc)
#10654 opened Feb 17, 2024 by smorel394 Loading…
2 of 3 tasks
@eric-wieser
46
feat : Tensor-Hom adjunction in the category of modules awaiting-author A reviewer has asked the author a question or requested changes t-algebra Algebra (groups, rings, fields, etc) WIP Work in progress
#8495 opened Nov 18, 2023 by jjaassoonn • Draft
@eric-wieser
88
feat: Equivs for AddMonoidAlgebras awaiting-author A reviewer has asked the author a question or requested changes t-algebra Algebra (groups, rings, fields, etc)
#7219 opened Sep 17, 2023 by Ruben-VandeVelde Loading…
@eric-wieser
12
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
ProTip! Adding no:label will show everything without a label.