α : Type u_1
β : Type ?u.270994
γ : Type ?u.270997
ι : Type ?u.271000
inst✝ : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
⊢ ↑(nndist z⁻¹ w⁻¹) = ↑(nndist z w / (‖z‖₊ * ‖w‖₊))
α : Type u_1
β : Type ?u.270994
γ : Type ?u.270997
ι : Type ?u.271000
inst✝ : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
⊢ nndist z⁻¹ w⁻¹ = nndist z w / (‖z‖₊ * ‖w‖₊)
rw [← NNReal.coe_eq]
no goals
α : Type u_1
β : Type ?u.270994
γ : Type ?u.270997
ι : Type ?u.271000
inst✝ : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
⊢ ↑(nndist z⁻¹ w⁻¹) = ↑(nndist z w / (‖z‖₊ * ‖w‖₊))
simp [-NNReal.coe_eq, dist_inv_inv₀ hz hw]