A machine-checked solution to the Jacobians challenge

30.1. Keystones🔗

abelJacobi_twoPoint_ne_zerosource · report an issue

theorem abelJacobi_twoPoint_ne_zero
    (h : 0 < genus X) {P Q : X} (hPQ : P ≠ Q) :
    abelJacobi ⟨twoPointDivisor X P Q, twoPointDivisor_mem_degZero X P Q⟩ ≠ 0