Theorem Isometry.completion_extension

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) …
Modified Isometry.completion_extensionView on Github →
2023-03-12 19:12
Mathlib/Topology/MetricSpace/Completion.lean
feat: port Analysis.Normed.Group.HomCompletion (#2818)
Added Isometry.completion_extensionView on Github →