E : Type ?u.440103
inst✝ : NormedAddCommGroup E
c w : ℂ
R : ℝ
⊢ R = 0 ∨ False ∨ ¬w ∈ sphere c (Abs.abs R) ↔ R = 0 ∨ ¬w ∈ sphere c (Abs.abs R)
E : Type ?u.440103
inst✝ : NormedAddCommGroup E
c w : ℂ
R : ℝ
⊢ CircleIntegrable (fun z => (z - w)⁻¹) c R ↔ R = 0 ∨ ¬w ∈ sphere c (Abs.abs R)
simp only [← zpow_neg_one, circleIntegrable_sub_zpow_iff]
no goals
E : Type ?u.440103
inst✝ : NormedAddCommGroup E
c w : ℂ
R : ℝ
⊢ R = 0 ∨ False ∨ ¬w ∈ sphere c (Abs.abs R) ↔ R = 0 ∨ ¬w ∈ sphere c (Abs.abs R)
norm_num