11.6. Meromorphic.MeromorphicInverse🔗

Jacobians.Meromorphic.MeromorphicInverse — source

_root_.Jacobians.IsMeromorphic.inv

The pointwise reciprocal of a meromorphic function is meromorphic (Mathlib MeromorphicAt.inv, applied in each chart — composition with the chart inverse commutes with pointwise ⁻¹).

theorem _root_.Jacobians.IsMeromorphic.inv {f : X → ℂ} (hf : IsMeromorphic X f) :
    IsMeromorphic X f⁻¹

inv_toFun

@[simp] theorem inv_toFun (f : MeromorphicFunction X) : (f⁻¹).toFun = f.toFun⁻¹

orderW_inv

The germ-order of a reciprocal is the negation: (f⁻¹).orderW x = −(f.orderW x) (Mathlib meromorphicOrderAt_inv, read in the chart at x). A pole of order n of f becomes a zero of order n of f⁻¹ and vice versa.

theorem orderW_inv (f : MeromorphicFunction X) (x : X) :
    (f⁻¹).orderW x = -(f.orderW x)