MeromorphicNFAt — Mathlib

English

Variant statement asserting equality of divisor under certain manipulations of divisor and factorized product.

Русский

Вариант утверждения о равенстве дивизора при определенных преобразованиях делителя и произведения.

LaTeX

$$$\text{MeromorphicOn.divisor}(\text{finprod } (\cdot - u)^{D(u)}, U) = D$$$

Lean4

/-- A function is 'meromorphic in normal form' at `x` if it vanishes around `x`
or if it can locally be written as `fun z ↦ (z - x) ^ n • g` where `g` is
analytic and does not vanish at `x`. -/
def MeromorphicNFAt :=
  f =ᶠ[𝓝 x] 0 ∨ ∃ (n : ℤ) (g : 𝕜 → E), AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ f =ᶠ[𝓝 x] (· - x) ^ n • g

Похожие утверждения