Structure linear_isometry
Modification history
2022-07-24 16:34
src/analysis/normed_space/linear_isometry.lean
chore(*): Rename `normed_group` to `normed_add_comm_group` (#15619) …
Modified linear_isometryView on Github →2021-10-08 00:30
src/analysis/normed_space/linear_isometry.lean
refactor(analysis/normed_space/linear_isometry): semilinear isometries (#9551) …
Modified linear_isometryView on Github →