meromorphicTrailingCoeffAt_const — Mathlib

English

The trailing coefficient of a constant function is the constant itself.

Русский

Хвостовой коэффициент константной функции равен самой константе.

LaTeX

$$$$\mathrm{meromorphicTrailingCoeffAt}(\lambda z. e, x) = e.$$$$

Lean4

/-- The trailing coefficient of a constant function is the constant.
-/
@[simp]
theorem meromorphicTrailingCoeffAt_const {x : 𝕜} {e : 𝕜} : meromorphicTrailingCoeffAt (fun _ ↦ e) x = e :=
  by
  by_cases he : e = 0
  · rw [he]
    apply MeromorphicAt.meromorphicTrailingCoeffAt_of_order_eq_top
    rw [meromorphicOrderAt_eq_top_iff]
    simp
  · exact analyticAt_const.meromorphicTrailingCoeffAt_of_ne_zero he

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