α : Type ?u.578231
β : Type ?u.578234
γ : Type ?u.578237
ι : Type ?u.578240
𝕜 : Type u_2
𝕜' : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
x y : 𝕜
⊢ dist (↑(algebraMap 𝕜 𝕜') x) (↑(algebraMap 𝕜 𝕜') y) = dist x y
α : Type ?u.578231
β : Type ?u.578234
γ : Type ?u.578237
ι : Type ?u.578240
𝕜 : Type u_2
𝕜' : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
⊢ Isometry ↑(algebraMap 𝕜 𝕜')
refine' Isometry.of_dist_eq fun x y => _
no goals
α : Type ?u.578231
β : Type ?u.578234
γ : Type ?u.578237
ι : Type ?u.578240
𝕜 : Type u_2
𝕜' : Type u_1
inst✝³ : NormedField 𝕜
inst✝² : SeminormedRing 𝕜'
inst✝¹ : NormedAlgebra 𝕜 𝕜'
inst✝ : NormOneClass 𝕜'
x y : 𝕜
⊢ dist (↑(algebraMap 𝕜 𝕜') x) (↑(algebraMap 𝕜 𝕜') y) = dist x y
rw [dist_eq_norm, dist_eq_norm, ← RingHom.map_sub, norm_algebraMap']