mathlib

832a8ba8 - feat(topology/metric_space/isometric_smul): new file (#18130)

feat(topology/metric_space/isometric_smul): new file (#18130) Define typeclasses `has_isometric_smul` and `has_isometric_vadd`. To minimize diff size, I did not fully deduplicate lemmas in this PR.