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: Generalizing some results from CommRing to CommSemiring #9512
Conversation
Modify some local instances to solve a problem after the proposed changes in TensorProduct
Is this still a draft? |
No, it's not, sorry. |
!bench |
Hopefully this does not slow |
Here are the benchmark results for commit f9a53a5. Benchmark Metric Change
===============================================================
+ ~Mathlib.Algebra.Module.LocalizedModule instructions -4.4%
+ ~Mathlib.RingTheory.IsTensorProduct instructions -11.6% |
That's surprising! I guess that's a good sign |
🚀 Pull request has been placed on the maintainer queue by erdOne. |
+3% wall clock isn’t great. Might be an artifact. |
Here are the benchmark results for commit f9a53a5. Benchmark Metric Change
===============================================================
+ ~Mathlib.Algebra.Module.LocalizedModule instructions -4.4%
+ ~Mathlib.RingTheory.IsTensorProduct instructions -11.6% |
How one does this checking? |
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 🎉
bors merge
Canceled. |
bors merge (The diff was showing changes from #9125 too) |
Most of the changes are minor. Co-authored-by: Xavier Xarles <56635243+XavierXarles@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Pull request successfully merged into master. Build succeeded: |
Most of the changes are minor.