Theorem Isometry.nnnorm_map_of_map_one

Modification history

2024-06-20 19:07
Mathlib/Analysis/Normed/Group/Basic.lean
chore: move some lemmas to Analysis.Normed.Group.Uniform (#13945) …
Modified Isometry.nnnorm_map_of_map_oneView on Github →
2024-02-09 15:09
Mathlib/Analysis/Normed/Group/Basic.lean
feat: add `Isometry.nnnorm_map` (#10367) …
Added Isometry.nnnorm_map_of_map_oneView on Github →