A machine-checked solution to the Jacobians challenge

15.1. Keystones🔗

  • FormTraceFibre

  • FormTraceGlobal* (traced form is rational)