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(Analysis/Asymptotics/Asymptotics): generalize smul lemmas to normed rings #9811
Conversation
Should we allow |
Possibly; though arguably with that change it should be renamed to |
Thanks! 🎉 |
…med rings (#9811) Using `BoundedSMul` instead of `NormedSpace` makes these true more generally. The old proofs do not generalize, so are replaced with copies of the `mul` proofs. The `const_smul_self` lemmas match the existing `const_mul_self` ones.
Build failed (retrying...): |
…med rings (#9811) Using `BoundedSMul` instead of `NormedSpace` makes these true more generally. The old proofs do not generalize, so are replaced with copies of the `mul` proofs. The `const_smul_self` lemmas match the existing `const_mul_self` ones.
Build failed (retrying...): |
…med rings (#9811) Using `BoundedSMul` instead of `NormedSpace` makes these true more generally. The old proofs do not generalize, so are replaced with copies of the `mul` proofs. The `const_smul_self` lemmas match the existing `const_mul_self` ones.
Build failed (retrying...): |
This might be causing bors failure... bors r- bors d+ |
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
Canceled. |
bors merge |
It has a merge conflict now. Please merge |
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
Canceled. |
bors merge |
…med rings (#9811) Using `BoundedSMul` instead of `NormedSpace` makes these true more generally. The old proofs do not generalize, so are replaced with copies of the `mul` proofs. The `const_smul_self` lemmas match the existing `const_mul_self` ones. `shake` then reports that the imports can be reduced.
Pull request successfully merged into master. Build succeeded: |
…med rings (#9811) Using `BoundedSMul` instead of `NormedSpace` makes these true more generally. The old proofs do not generalize, so are replaced with copies of the `mul` proofs. The `const_smul_self` lemmas match the existing `const_mul_self` ones. `shake` then reports that the imports can be reduced.
…med rings (#9811) Using `BoundedSMul` instead of `NormedSpace` makes these true more generally. The old proofs do not generalize, so are replaced with copies of the `mul` proofs. The `const_smul_self` lemmas match the existing `const_mul_self` ones. `shake` then reports that the imports can be reduced.
Using
BoundedSMul
instead ofNormedSpace
makes these true more generally. The old proofs do not generalize, so are replaced with copies of themul
proofs.The
const_smul_self
lemmas match the existingconst_mul_self
ones.shake
then reports that the imports can be reduced.