no goals
𝓕 : Type ?u.1226326
𝕜 : Type ?u.1226329
α : Type ?u.1226332
ι : Type ?u.1226335
κ : Type ?u.1226338
E : Type u_1
F : Type ?u.1226344
G : Type ?u.1226347
inst✝¹ : NormedGroup E
inst✝ : NormedGroup F
a b : E
⊢ ‖a / b‖ = 0 ↔ a = b
rw [norm_eq_zero'', div_eq_one]