Commit 2026-03-06 17:10 d07ceaec

View on Github →

feat: Isometry.mapRingHom (#36257)

Estimated changes

Modified Mathlib/Topology/MetricSpace/Completion.lean

modified def Isometry.extensionHom

modified theorem Isometry.extensionHom_coe

added theorem Isometry.isometry_mapRingHom

added def Isometry.mapRingHom

added theorem Isometry.mapRingHom_coe