Mathlib v3 is deprecated. Go to Mathlib v4

Def linear_isometry.to_linear_isometry_equiv

Modification history

2021-09-20 10:37
src/analysis/normed_space/finite_dimension.lean
chore(analysis/normed_space/finite_dimensional): restructure imports (#9289) …
Added linear_isometry.to_linear_isometry_equivView on Github →