New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(Algebra/Module/LinearMap/Basic): module structures of (semi)-linear maps over DomMulAct
of a ring
#10766
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks!
maintainer merge
🚀 Pull request has been placed on the maintainer queue by alreadydone. |
!bench |
Here are the benchmark results for commit b899b04. Benchmark Metric Change
===============================================================
- ~Mathlib.Algebra.Module.LinearMap.Basic instructions 27.4% |
bors d+ Thanks! |
✌️ jjaassoonn can now approve this pull request. To approve and merge a pull request, simply reply with |
Ones the CI passes, can you take another look before merging please @alreadydone |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks! LGTM
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
bors merge |
…ear maps over `DomMulAct` of a ring (#10766) splitted from #8559 These are written by @alreadydone Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Pull request successfully merged into master. Build succeeded: |
DomMulAct
of a ringDomMulAct
of a ring
…ear maps over `DomMulAct` of a ring (#10766) splitted from #8559 These are written by @alreadydone Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…ear maps over `DomMulAct` of a ring (#10766) splitted from #8559 These are written by @alreadydone Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…ear maps over `DomMulAct` of a ring (#10766) splitted from #8559 These are written by @alreadydone Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
…ear maps over `DomMulAct` of a ring (#10766) splitted from #8559 These are written by @alreadydone Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
splitted from #8559
These are written by @alreadydone