linear_isometry): add lemmas to `linear_isometry_equiv` (#12218)

Commit

3 years ago

feat(analysis/normed_space/linear_isometry): add lemmas to `linear_isometry_equiv` (#12218) Added two API lemmas to `linear_isometry_equiv` that I need elsewhere.

Author

Daniel-Packer

Parents

f44ed74a

mathlib dc9b8bea - feat(analysis/normed_space/linear_isometry): add lemmas to `linear_isometry_equiv` (#12218)

mathlib
dc9b8bea - feat(analysis/normed_space/linear_isometry): add lemmas to `linear_isometry_equiv` (#12218)