Complex.Hadamard.divisorComplementFactor_def

lemma divisorComplementFactor_def    (m : ℕ) (f : ℂ → ℂ) (z₀ : ℂ)    (p : divisorZeroIndex₀ f (Set.univ : Set ℂ)) (z : ℂ) :    divisorComplementFactor m f z₀ p z =      if divisorZeroIndex₀_val p = z₀ then (1 : ℂ)      else weierstrassFactor m (z / divisorZeroIndex₀_val p) := by  classical  by_cases h : divisorZeroIndex₀_val p = z₀  · have hp : p ∈ divisorZeroIndex₀_fiberFinset (f := f) z₀ := by      simpa [mem_divisorZeroIndex₀_fiberFinset] using h    simp [divisorComplementFactor_eq_one_of_mem, hp, h]  · have hp : p ∉ divisorZeroIndex₀_fiberFinset (f := f) z₀ := by      intro hmem      exact h ((mem_divisorZeroIndex₀_fiberFinset f z₀ p).1 hmem)    simp [divisorComplementFactor_eq_weierstrassFactor_of_not_mem, hp, h]