Source indexedlemma · leanprover/lean4:v4.32.0

Complex.Hadamard.divisorZeroIndex₀_val_eq_of_mem_ball

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorUnits · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/DivisorUnits.lean:25 to 36

Mathematical statement

Exact Lean statement

lemma divisorZeroIndex₀_val_eq_of_mem_ball
    {f : ℂ → ℂ} {z₀ : ℂ} {ε : ℝ}
    (hball : Metric.ball z₀ ε ∩ (MeromorphicOn.divisor f (Set.univ : Set ℂ)).support = {z₀})
    (p : divisorZeroIndex₀ f (Set.univ : Set ℂ))
    (hp : divisorZeroIndex₀_val p ∈ Metric.ball z₀ ε) :
    divisorZeroIndex₀_val p = z₀

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma divisorZeroIndex₀_val_eq_of_mem_ball    {f : ℂ → ℂ} {z₀ : ℂ} {ε : ℝ}    (hball : Metric.ball z₀ ε ∩ (MeromorphicOn.divisor f (Set.univ : Set ℂ)).support = {z₀})    (p : divisorZeroIndex₀ f (Set.univ : Set ℂ))    (hp : divisorZeroIndex₀_val p ∈ Metric.ball z₀ ε) :    divisorZeroIndex₀_val p = z₀ := by  have hsupp : divisorZeroIndex₀_val p ∈ (MeromorphicOn.divisor f (Set.univ : Set ℂ)).support :=    divisorZeroIndex₀_val_mem_divisor_support' (p := p)  have : divisorZeroIndex₀_val p ∈      Metric.ball z₀ ε ∩ (MeromorphicOn.divisor f (Set.univ : Set ℂ)).support := ⟨hp, hsupp⟩  simp [hball] at this  simpa using this