meromorphicTrailingCoeffAt_pow — Mathlib

English

The trailing coefficient of f^n equals the nth power of the trailing coefficient for natural n.

Русский

Хвостовой коэффициент f^n равен n-й степени хвостового коэффициента f при натуральном n.

LaTeX

$$$$ \mathrm{meromorphicTrailingCoeffAt}(f^n, x) = (\mathrm{meromorphicTrailingCoeffAt}(f, x))^{n}. $$$$

Lean4

/-- The trailing coefficient of the power of a function is the power of the trailing coefficient.
-/
theorem meromorphicTrailingCoeffAt_pow {n : ℕ} {f : 𝕜 → 𝕜} (h₁ : MeromorphicAt f x) :
    meromorphicTrailingCoeffAt (f ^ n) x = (meromorphicTrailingCoeffAt f x) ^ n := by
  convert h₁.meromorphicTrailingCoeffAt_zpow (n := n) <;> simp

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