linear_isometry): `to_linear_equiv_trans` (#11628)

Commit

3 years ago

feat(analysis/normed_space/linear_isometry): `to_linear_equiv_trans` (#11628) Add a lemma relating `trans` for `linear_isometry_equiv` and `linear_equiv`.

Author

jsm28

Parents

ed903019

mathlib dac4f405 - feat(analysis/normed_space/linear_isometry): `to_linear_equiv_trans` (#11628)

mathlib
dac4f405 - feat(analysis/normed_space/linear_isometry): `to_linear_equiv_trans` (#11628)