A machine-checked solution to the Jacobians challenge

11.1. Keystones🔗

MeromorphicFunction — source · report an issue

structure MeromorphicFunction [TopologicalSpace X] [ChartedSpace ℂ X] : Type _ where

Divisor — source · report an issue

abbrev Divisor : Type _

lDim / linearSystem — source · report an issue

noncomputable def lDim (D : Divisor X) : ℕ