-
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(analysis/quaternion): add complete_space
, module.free
, and module.finite
instances
#18347
Conversation
… its coefficients
complete_space
, module.free
, and module.finite
instances
src/algebra/quaternion.lean
Outdated
def linear_equiv_tuple : ℍ[R,c₁,c₂] ≃ₗ[R] (fin 4 → R) := | ||
linear_equiv.symm | ||
{ to_fun := (equiv_tuple c₁ c₂).symm, | ||
inv_fun := (equiv_tuple c₁ c₂), | ||
map_add' := λ v₁ v₂, rfl, | ||
map_smul' := λ v₁ v₂, rfl, | ||
.. (equiv_tuple c₁ c₂).symm } |
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.
Sorry if I'm missing something obvious, but why do you need to symm
everything?
def linear_equiv_tuple : ℍ[R,c₁,c₂] ≃ₗ[R] (fin 4 → R) := | |
linear_equiv.symm | |
{ to_fun := (equiv_tuple c₁ c₂).symm, | |
inv_fun := (equiv_tuple c₁ c₂), | |
map_add' := λ v₁ v₂, rfl, | |
map_smul' := λ v₁ v₂, rfl, | |
.. (equiv_tuple c₁ c₂).symm } | |
def linear_equiv_tuple : ℍ[R,c₁,c₂] ≃ₗ[R] (fin 4 → R) := | |
{ map_add' := λ v₁ v₂, rfl, | |
map_smul' := λ v₁ v₂, rfl, | |
..equiv_tuple c₁ c₂ } |
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 seem to remember that that didn't work as the proofs weren't rfl in that direction; but I can't test right now because the cache seems to be a corrupt tarball...
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.
Yep, I can confirm that rfl
doesn't work in your code. I added a comment explaining the symm
.
You could of course spend some effort proving the harder statements, but I don't see any reason to do so.
LGTM bors merge |
…module.finite` instances (#18347) The main trick here is showing that the quaternions are in isometric equivalence with 4D euclidean space.
Pull request successfully merged into master. Build succeeded: |
complete_space
, module.free
, and module.finite
instancescomplete_space
, module.free
, and module.finite
instances
The main trick here is showing that the quaternions are in isometric equivalence with 4D euclidean space.