Theorems · Theorem · complex analysis

meromorphicOrderAt_deriv_eq_sub_one

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CompleteSpace E] {f : 𝕜 → E} {x : 𝕜} {n : ℤ},
  ↑n ≠ 0 → meromorphicOrderAt f x = ↑n → meromorphicOrderAt (deriv f) x = ↑(n - 1)

The meromorphic order of the derivative is one less than the order of the original function. This however is not true if the characteristic of the domain field divides the original order, where the order of the derivative can rise to a larger integer.

Defined in

Mathlib.Analysis.Meromorphic.Order

Cited by

2 results in Mathlib

Foundations

Depth 199 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceCompleteSpace