Theorem Isometry.extensionHom_coe

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.extensionHom_coeView on Github →