[Merged by Bors] - feat(analysis/normed_space/linear_isometry): linear_equiv.of_eq as a linear_isometry_equiv
#15471
Conversation
ADedecker
added
easy
|
|
||
| variables {p q} | ||
|
|
||
| @[simp] lemma coe_of_eq_apply (h : p = q) (x : p) : (of_eq p q h x : E) = x := rfl |
There was a problem hiding this comment.
Could you please setup simps to work with linear isometries, if that is not already done? Then these lemmas can be auto-generated.
There was a problem hiding this comment.
I don't think simps is easy to configure to generate the right name here (with coe as a prefix)
There was a problem hiding this comment.
Yes, if we want to autogenerate these we can't do anything about the names. I'm struggling a bit to understand how to setup these properly, but I'll ask people in Providence tomorrow
There was a problem hiding this comment.
I did the simps setup and removed the coe_of_eq_apply, here and for linear_equiv, since simps generate it as of_eq_apply, which is more homogeneous with the rest of the library. Does that sound fine ?
eric-wieser
added
awaiting-author
ADedecker
removed
the
easy
ADedecker
added
awaiting-review
| variables {R E E₂ E₃} {R' : Type*} [ring R'] [module R' E] (p q : submodule R' E) | ||
|
|
||
| /-- `linear_equiv.of_eq` as a `linear_isometry_equiv`. -/ | ||
| @[simps apply symm_apply] def of_eq (hpq : p = q) : |
There was a problem hiding this comment.
What lemmas does this generate now then?
There was a problem hiding this comment.
Okay I should have checked more carefully, because this doesn't give what we want here. The generated lemmas basically says that linear_isometry_equiv.of_eq p q h x = linear_equiv.of_eq p q h x, which itself simplifies back to equiv.set_of_eq...
So I'll switch back to the manually generated ones
|
✌️ ADedecker can now approve this pull request. To approve and merge a pull request, simply reply with |
ADedecker
added
delegated
|
bors r+ |
…a `linear_isometry_equiv` (#15471) We also setup `simps` on `linear_isometry` and `linear_isometry_equiv`.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
linear_equiv.of_eq as a linear_isometry_equivlinear_equiv.of_eq as a linear_isometry_equiv
…a `linear_isometry_equiv` (#15471) We also setup `simps` on `linear_isometry` and `linear_isometry_equiv`.
We also setup
simpsonlinear_isometryandlinear_isometry_equiv.