English
Conversion to normal form does not alter divisors on U; i.e., divisor (toMeromorphicNFOn f U) U = divisor f U.
Русский
Преобразование к нормальной форме не изменяет дивизор на U; дивизор nfOn совпадает с дивизором f.
LaTeX
$$$\operatorname{divisor}(toMeromorphicNFOn\ f\ U, U) = \operatorname{divisor}(f, U)$$$
Lean4
/-- The order of a meromorphic function `f` at `z₀` is finite iff `f` can locally be
written as `f z = (z - z₀) ^ order • g z`, where `g` is analytic and does not
vanish at `z₀`.
-/
theorem meromorphicOrderAt_ne_top_iff {f : 𝕜 → E} {z₀ : 𝕜} (hf : MeromorphicAt f z₀) :
meromorphicOrderAt f z₀ ≠ ⊤ ↔
∃ (g : 𝕜 → E),
AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ f =ᶠ[𝓝[≠] z₀] fun z ↦ (z - z₀) ^ ((meromorphicOrderAt f z₀).untop₀) • g z :=
⟨fun h ↦ (meromorphicOrderAt_eq_int_iff hf).1 (WithTop.coe_untop₀_of_ne_top h).symm, fun h ↦
Option.ne_none_iff_exists'.2 ⟨(meromorphicOrderAt f z₀).untopD 0, (meromorphicOrderAt_eq_int_iff hf).2 h⟩⟩
