English
If f is meromorphic at x, then for any natural n, meromorphicOrderAt(f^n) = n · meromorphicOrderAt(f).
Русский
Если f мероморфна в x, то для любого натурального n имеет место meromorphicOrderAt(f^n) = n · meromorphicOrderAt(f).
LaTeX
$$$\\operatorname{meromorphicOrderAt} (f^n) x = n \\cdot \\operatorname{meromorphicOrderAt} f x$$$
Lean4
/-- The order multiplies by `n` when taking a meromorphic function to its `n`th power. -/
theorem meromorphicOrderAt_pow {f : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) {n : ℕ} :
meromorphicOrderAt (f ^ n) x = n * meromorphicOrderAt f x :=
by
induction n
case zero =>
simp only [pow_zero, CharP.cast_eq_zero, zero_mul]
rw [← WithTop.coe_zero, meromorphicOrderAt_eq_int_iff]
· exact ⟨1, analyticAt_const, by simp⟩
· apply MeromorphicAt.const
case succ n
hn =>
simp only [pow_add, pow_one, meromorphicOrderAt_mul (hf.pow n) hf, hn, Nat.cast_add, Nat.cast_one]
cases meromorphicOrderAt f x
· aesop
· norm_cast
simp only [Nat.cast_add, Nat.cast_one]
ring
