K : Type u_1
E : Type ?u.6921453
inst✝ : IsROrC K
z : K
⊢ abs (↑im z) / ‖z‖ ≤ 1
K : Type u_1
E : Type ?u.6921453
inst✝ : IsROrC K
z : K
⊢ abs (↑im z / ‖z‖) ≤ 1
rw [abs_div, abs_norm]
no goals
K : Type u_1
E : Type ?u.6921453
inst✝ : IsROrC K
z : K
⊢ abs (↑im z) / ‖z‖ ≤ 1
exact div_le_one_of_le (abs_im_le_norm _) (norm_nonneg _)