𝓕 : Type ?u.1226823
𝕜 : Type ?u.1226826
α : Type ?u.1226829
ι : Type ?u.1226832
κ : Type ?u.1226835
E : Type u_1
F : Type ?u.1226841
G : Type ?u.1226844
inst✝¹ : NormedGroup E
inst✝ : NormedGroup F
a b : E
⊢ ‖a / b‖ ≠ 0 ↔ a ≠ b
𝓕 : Type ?u.1226823
𝕜 : Type ?u.1226826
α : Type ?u.1226829
ι : Type ?u.1226832
κ : Type ?u.1226835
E : Type u_1
F : Type ?u.1226841
G : Type ?u.1226844
inst✝¹ : NormedGroup E
inst✝ : NormedGroup F
a b : E
⊢ 0 < ‖a / b‖ ↔ a ≠ b
rw [(norm_nonneg' _).lt_iff_ne, ne_comm]
no goals
𝓕 : Type ?u.1226823
𝕜 : Type ?u.1226826
α : Type ?u.1226829
ι : Type ?u.1226832
κ : Type ?u.1226835
E : Type u_1
F : Type ?u.1226841
G : Type ?u.1226844
inst✝¹ : NormedGroup E
inst✝ : NormedGroup F
a b : E
⊢ ‖a / b‖ ≠ 0 ↔ a ≠ b
exact norm_div_eq_zero_iff.not