Source indexedlemma · leanprover/lean4:v4.32.0

Complex.Hadamard.divisor_univ_eq_analyticOrderNatAt_int

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorFiber · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/DivisorFiber.lean:36 to 48

Mathematical statement

Exact Lean statement

lemma divisor_univ_eq_analyticOrderNatAt_int {f : ℂ → ℂ} (hf : Differentiable ℂ f) (z : ℂ) :
    MeromorphicOn.divisor f (Set.univ : Set ℂ) z = (analyticOrderNatAt f z : ℤ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma divisor_univ_eq_analyticOrderNatAt_int {f : ℂ → ℂ} (hf : Differentiable ℂ f) (z : ℂ) :    MeromorphicOn.divisor f (Set.univ : Set ℂ) z = (analyticOrderNatAt f z : ℤ) := by  have hmero : MeromorphicOn f (Set.univ : Set ℂ) := by    intro w hw    exact (Differentiable.analyticAt (f := f) hf w).meromorphicAt  simp only    [MeromorphicOn.divisor_apply hmero (by simp : z ∈ (Set.univ : Set ℂ)), analyticOrderNatAt]  have han : AnalyticAt ℂ f z := Differentiable.analyticAt (f := f) hf z  cases h : analyticOrderAt f z with  | top =>      simp [han.meromorphicOrderAt_eq, h]  | coe n =>      simp [han.meromorphicOrderAt_eq, h]