Mathlib v3 is deprecated. Go to Mathlib v4

Def linear_map.to_linear_isometry

Modification history

2021-10-09 07:26
src/analysis/normed_space/linear_isometry.lean
chore(analysis/normed_space/linear_isometry): adjust `isometry` API (#9635) …
Added linear_map.to_linear_isometryView on Github →