Theorem Isometry.extensionHom_coe

Modification history

2026-03-06 17:10
Mathlib/Topology/MetricSpace/Completion.lean
feat: `Isometry.mapRingHom` (#36257)
Modified Isometry.extensionHom_coeView on Github →
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 →