-
Notifications
You must be signed in to change notification settings - Fork 299
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] - chore(algebra/quaternion): generalize the algebra instance #18382
Conversation
ecaf4ba
to
e7a90ef
Compare
e7a90ef
to
fadbbb6
Compare
…ion-algebra-generalize
…' into eric-wieser/quaternion-algebra-generalize
…' into eric-wieser/quaternion-algebra-generalize
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.
Clean overall!
This PR/issue depends on:
|
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.
I am now happy with it. Thanks!
maintainer merge
maintainer merge (since it didn't seem to post in the Zulip thread) |
🚀 Pull request has been placed on the maintainer queue by eric-wieser. |
bors merge |
To prevent this generalization forming diamonds, we have to now populate the `nsmul`, `zsmul`, and `qsmul` fields. I use this in another PR to talk about the `R` algebra structure of `quaternion (dual_number R)`. Even without that motivation, this change means that the existing `smul` lemmas now apply to `nsmul`, `zsmul`, and `rat_smul` where previously they did not.
Pull request successfully merged into master. Build succeeded: |
To prevent this generalization forming diamonds, we have to now populate the
nsmul
,zsmul
, andqsmul
fields.I use this in another PR to talk about the
R
algebra structure ofquaternion (dual_number R)
.Even without that motivation, this change means that the existing
smul
lemmas now apply tonsmul
,zsmul
, andrat_smul
where previously they did not.