meromorphicTrailingCoeffAt_ne_zero

English

If f is meromorphic at x with finite order, then the trailing coefficient at x is nonzero.

Русский

Если f мероморфна в точке x и порядок конечен, то хвостовой коэффициент в x не нулевой.

LaTeX

$$$$\mathrm{meromorphicTrailingCoeffAt}(f,x) \neq 0.$$$$

Lean4

/-- If `f` is meromorphic of finite order at `x`, then the trailing coefficient is not zero.
-/
theorem meromorphicTrailingCoeffAt_ne_zero (h₁ : MeromorphicAt f x) (h₂ : meromorphicOrderAt f x ≠ ⊤) :
    meromorphicTrailingCoeffAt f x ≠ 0 :=
  by
  obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_ne_top_iff h₁).1 h₂
  simpa [h₁g.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE h₂g h₃g] using h₂g

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