Mathlib v3 is deprecated. Go to Mathlib v4

Theorem isometric.isometry_vadd_vsub_of_isometry

Modification history

2020-08-15 12:06
src/analysis/normed_space/add_torsor.lean
refactor(algebra/add_torsor): use `out_param` (#3727)
Deleted isometric.isometry_vadd_vsub_of_isometryView on Github →
2020-08-03 17:57
src/analysis/normed_space/add_torsor.lean
feat(analysis/normed_space/add_torsor): isometries of normed_add_torsors (#3666) …
Added isometric.isometry_vadd_vsub_of_isometryView on Github →