Mathlib v3 is deprecated. Go to Mathlib v4

Theorem algebra_map_isometry

Modification history

2022-04-22 01:34
src/analysis/normed_space/basic.lean
fix(analysis/normed_space/basic): allow the zero ring to be a normed algebra (#13544) …
Modified algebra_map_isometryView on Github →
2021-06-19 23:38
src/analysis/normed_space/basic.lean
refactor(topology/metric_space/isometry): move material about isometries of normed spaces (#8003) …
Modified algebra_map_isometryView on Github →
2021-04-02 21:56
src/topology/metric_space/isometry.lean
refactor(topology/metric_space/isometry): generalize to pseudo_metric (#6910) …
Modified algebra_map_isometryView on Github →
2019-11-26 12:10
src/topology/metric_space/isometry.lean
feat(analysis/complex/basic): restriction of scalars, real differentiability of complex functions (#1716) …
Added algebra_map_isometryView on Github →