Def affine_isometry.to_affine_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 affine_isometry.to_affine_isometry_equivView on Github →