linear_isometry): `linear_equiv.of_eq` as a `linear_isometry_equiv` (#15471)

Commit

3 years ago

feat(analysis/normed_space/linear_isometry): `linear_equiv.of_eq` as a `linear_isometry_equiv` (#15471) We also setup `simps` on `linear_isometry` and `linear_isometry_equiv`.

Author

ADedecker

Parents

de04bafa

mathlib 34d4a9bf - feat(analysis/normed_space/linear_isometry): `linear_equiv.of_eq` as a `linear_isometry_equiv` (#15471)

mathlib
34d4a9bf - feat(analysis/normed_space/linear_isometry): `linear_equiv.of_eq` as a `linear_isometry_equiv` (#15471)