linear_isometry): add an upgrade from linear isometries between finite dimensional spaces of eq finrank to linear isometry equivs (#8406)

Commit

4 years ago

feat(analysis/normed_space/linear_isometry): add an upgrade from linear isometries between finite dimensional spaces of eq finrank to linear isometry equivs (#8406)

Author

justadzr

Parents

8062521e

mathlib3 dfa95abf - feat(analysis/normed_space/linear_isometry): add an upgrade from linear isometries between finite dimensional spaces of eq finrank to linear isometry equivs (#8406)

mathlib3
dfa95abf - feat(analysis/normed_space/linear_isometry): add an upgrade from linear isometries between finite dimensional spaces of eq finrank to linear isometry equivs (#8406)