-
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] - feat(algebra/quaternion): add quaternion.im
for the skew-adjoint part
#18456
Conversation
@[simp] lemma im_re : a.im.re = 0 := rfl | ||
@[simp] lemma im_im_i : a.im.im_i = a.im_i := rfl | ||
@[simp] lemma im_im_j : a.im.im_j = a.im_j := rfl | ||
@[simp] lemma im_im_k : a.im.im_k = a.im_k := rfl |
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.
All those names look backward to me. Is that the naming convention for quaternions?
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.
Yes, unfortunately the names in this file are all over the place WRT naming order for dot notation. I can fix the names in a follow-up PR.
bea6dce
to
9f450b8
Compare
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! Looking good.
maintainer merge
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
bors merge |
…rt (#18456) As requested by @YaelDillies, as prework for #18349 where I need to split the quaternion into real and imaginary parts. Only one marginally interesting lemma is included, `im_sq` which says `q.im^2 = -norm_sq q.im`
Pull request successfully merged into master. Build succeeded: |
quaternion.im
for the skew-adjoint partquaternion.im
for the skew-adjoint part
As requested by @YaelDillies, as prework for #18349 where I need to split the quaternion into real and imaginary parts.
Only one marginally interesting lemma is included,
im_sq
which saysq.im^2 = -norm_sq q.im