Theorem Isometry.norm_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.norm_map_of_map_one View on Github →

2023-03-09 06:58

Mathlib/Analysis/Normed/Group/Basic.lean

feat: port Analysis.Normed.Group.Basic (#2736)

Added Isometry.norm_map_of_map_one View on Github →