'ProofExplorer.Jacobian.MarkusEight.characteristic_determinant' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'ProofExplorer.Jacobian.MarkusEight.actual_jacobian' depends on axioms: [propext, Classical.choice, Quot.sound]
'ProofExplorer.Jacobian.MarkusEight.three_zeros' depends on axioms: [propext, Classical.choice, Quot.sound]
'ProofExplorer.Jacobian.MarkusEight.weak_markus_yamabe_false_in_eight' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
