meromorphicAt — Mathlib

English

Equivalence of divisor with the factorized rational function on the set U in normal form.

Русский

Эквивалентность дивизора и факторизованной рациональной функции на U в нормальной форме.

LaTeX

$$$\text{MeromorphicOn.divisor}(\prod^{\mathrm{fin}}_{u} (\cdot - u)^{D(u)} \; U) = D$$$

Lean4

/-- If a function is meromorphic in normal form at `x`, then it is meromorphic at `x`. -/
theorem meromorphicAt (hf : MeromorphicNFAt f x) : MeromorphicAt f x :=
  by
  rw [meromorphicNFAt_iff_analyticAt_or] at hf
  rcases hf with h | h
  · exact h.meromorphicAt
  · obtain ⟨hf, _⟩ := h
    exact hf

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