[Merged by Bors] - feat(analysis/inner_product_space/pi_L2): map_isometry_euclidean_of_orthonormal
#11907
Conversation
…orthonormal` Add a lemma giving the result of `isometry_euclidean_of_orthonormal` when applied to an orthonormal basis obtained from another orthonormal basis with `basis.map`.
| @@ -176,6 +177,12 @@ rfl | |||
| ((v.isometry_euclidean_of_orthonormal hv).symm : euclidean_space 𝕜 ι → E) = v.equiv_fun.symm := | |||
| rfl | |||
|
|
|||
| @[simp] lemma basis.map_isometry_euclidean_of_orthonormal (v : basis ι 𝕜 E) (hv : orthonormal 𝕜 v) | |||
There was a problem hiding this comment.
Is this actually useful as a simp lemma? Wouldn't you just want to call it explicitly?
There was a problem hiding this comment.
Well, I think the RHS is simpler than the LHS, and I've used it as a simp lemma (to prove the corresponding simp lemma for the composition of complex.isometry_euclidean and isometry_euclidean_of_orthonormal, which in turn is used in defining and proving properties of oriented angles). If these aren't simp lemmas they can of course be named directly in the relevant simp calls.
There was a problem hiding this comment.
I agree this should be simp lemma. It may not fire very often but the fact that f appears only once on the RHS convinces me it is the simpler form.
|
✌️ jsm28 can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-bot-assistant
added
delegated
Co-authored-by: Oliver Nash <github@olivernash.org>
|
bors r+ |
…orthonormal` (#11907) Add a lemma giving the result of `isometry_euclidean_of_orthonormal` when applied to an orthonormal basis obtained from another orthonormal basis with `basis.map`.
|
This PR was included in a batch that was canceled, it will be automatically retried |
…orthonormal` (#11907) Add a lemma giving the result of `isometry_euclidean_of_orthonormal` when applied to an orthonormal basis obtained from another orthonormal basis with `basis.map`.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
map_isometry_euclidean_of_orthonormalmap_isometry_euclidean_of_orthonormal
Add a lemma giving the result of
isometry_euclidean_of_orthonormalwhen applied to an orthonormal basis obtained from another orthonormal
basis with
basis.map.