Def Isometry.extensionHom

Modification history

2025-11-28 16:39
Mathlib/Topology/MetricSpace/Completion.lean
refactor: use isometry extensions for completions at infinite places of number fields (#29969) …
Added Isometry.extensionHomView on Github →