A machine-checked solution to the Jacobians challenge

10.1. Keystones🔗

  • ProjectiveLine instances + genus ℙ¹ facts