Theorems · Definition · complex analysis

toMeromorphicNFOn

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

If f is meromorphic on U, convert f to normal form on U by changing its values along a discrete subset within U. Otherwise, returns the 0 function.

Defined in

Mathlib.Analysis.Meromorphic.NormalForm

Cited by

13 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpace