Theorems · Definition · complex analysis

toMeromorphicNFAt

{𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} → [inst_1 : NormedAddCommGroup E] → [NormedSpace 𝕜 E] → (𝕜 → E) → 𝕜 → 𝕜 → E

If f is meromorphic at x, convert f to normal form at x by changing its value at x. Otherwise, returns the 0 function.

Defined in

Mathlib.Analysis.Meromorphic.NormalForm

Cited by

15 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpace