meromorphicTrailingCoeffAt_of_ne_zero

English

If AnalyticAt f x and f x ≠ 0, then trailingCoeffAt f x = f x.

Русский

Если f аналитична в x и f(x) ≠ 0, то trailingCoeffAt f x = f x.

LaTeX

$$$\\text{meromorphicTrailingCoeffAt}_f x = f x$ при $f x \\neq 0$ и $\\text{AnalyticAt} f x$$$

Lean4

/-- If `f` is analytic and does not vanish at `x`, then the trailing coefficient of `f` at `x` is `f x`.
-/
@[simp]
theorem meromorphicTrailingCoeffAt_of_ne_zero (h₁ : AnalyticAt 𝕜 f x) (h₂ : f x ≠ 0) :
    meromorphicTrailingCoeffAt f x = f x :=
  by
  rw [h₁.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE (n := 0) h₂]
  filter_upwards
  simp

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