Theorem WithAbs.isometry_map

Modification history

2026-08-27 15:44
Mathlib/Analysis/Normed/Field/WithAbs.lean
feat(Analysis/Normed/Field/WithAbs): algebra structure on `AbsoluteValue.Completion` (#42542) …
Added WithAbs.isometry_mapView on Github →