Theorems · Theorem · complex analysis

AnalyticAt.unique_eventuallyEq_zpow_smul_nonzero

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} {m n : ℤ},
  (∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in nhdsWithin z₀ {z₀}ᶜ, f z = (z - z₀) ^ m • g z) →
    (∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in nhdsWithin z₀ {z₀}ᶜ, f z = (z - z₀) ^ n • g z) → m = n

For a function f on 𝕜, and z₀ ∈ 𝕜, there exists at most one n such that on a punctured neighbourhood of z₀ we have f z = (z - z₀) ^ n • g z, with g analytic and nonvanishing at z₀. We formulate this with n : ℤ, and deduce the case n : ℕ later, for applications to meromorphic functions.

Defined in

Mathlib.Analysis.Analytic.IsolatedZeros

Cited by

2 results in Mathlib

Foundations

Depth 192 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpace