A machine-checked solution to the Jacobians challenge

11.1. Keystones🔗

MeromorphicFunctionsource · report an issue

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

Divisorsource · report an issue

abbrev Divisor : Type _

lDim / linearSystemsource · report an issue

noncomputable def lDim (D : Divisor X) : ℕ