English
For analytic f at z0, the order of f^n at z0 is n times the order of f at z0 for every natural n.
Русский
Для аналитической функции f в z0 порядок f^n в z0 равен n-кратно порядку f в z0 для каждого натурального n.
LaTeX
$$$analyticOrderAt\,(f^{n})\, z_0 = n \cdot analyticOrderAt\, f\, z_0\quad(\text{для каждого } n\in\mathbb{N})$$$
Lean4
/-- The order multiplies by `n` when taking an analytic function to its `n`th power. -/
theorem analyticOrderAt_pow (hf : AnalyticAt 𝕜 f z₀) : ∀ n, analyticOrderAt (f ^ n) z₀ = n • analyticOrderAt f z₀
| 0 => by simp [analyticOrderAt_eq_zero]
| n + 1 => by simp [add_mul, pow_add, analyticOrderAt_mul (hf.pow n), analyticOrderAt_pow, hf]
