Source indexedlemma · leanprover/lean4:v4.32.0

Complex.Hadamard.divisorZeroIndex₀_fiberFinset_card_eq_analyticOrderNatAt

PrimeNumberTheoremAnd.Mathlib.Analysis.Complex.DivisorFiber · PrimeNumberTheoremAnd/Mathlib/Analysis/Complex/DivisorFiber.lean:135 to 144

Mathematical statement

Exact Lean statement

lemma divisorZeroIndex₀_fiberFinset_card_eq_analyticOrderNatAt
    {f : ℂ → ℂ} (hf : Differentiable ℂ f) {z₀ : ℂ} (hz₀ : z₀ ≠ 0) :
    (divisorZeroIndex₀_fiberFinset (f := f) z₀).card = analyticOrderNatAt f z₀

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma divisorZeroIndex₀_fiberFinset_card_eq_analyticOrderNatAt    {f : ℂ → ℂ} (hf : Differentiable ℂ f) {z₀ : ℂ} (hz₀ : z₀ ≠ 0) :    (divisorZeroIndex₀_fiberFinset (f := f) z₀).card = analyticOrderNatAt f z₀ := by  have hdiv :      MeromorphicOn.divisor f (Set.univ : Set ℂ) z₀ = (analyticOrderNatAt f z₀ : ℤ) :=    divisor_univ_eq_analyticOrderNatAt_int (f := f) hf z₀  have htoNat : Int.toNat (MeromorphicOn.divisor f (Set.univ : Set ℂ) z₀) =    analyticOrderNatAt f z₀ := by    simp [hdiv]  exact (divisorZeroIndex₀_fiberFinset_card_eq_toNat_divisor (f := f) (z₀ := z₀) hz₀).trans htoNat