OAI/AlgebraicGeometry/Seshadri/Jets/QuadraticJets.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MaximalSeshadri.QuadraticJets.quarticValue line 18
  2. def OAI.MaximalSeshadri.QuadraticJets.quarticCombination line 21
  3. def OAI.MaximalSeshadri.QuadraticJets.exponent20 line 24
  4. def OAI.MaximalSeshadri.QuadraticJets.exponent11 line 25
  5. def OAI.MaximalSeshadri.QuadraticJets.exponent02 line 26
  6. lemma OAI.MaximalSeshadri.QuadraticJets.degree20 line 28
  7. lemma OAI.MaximalSeshadri.QuadraticJets.degree11 line 29
  8. lemma OAI.MaximalSeshadri.QuadraticJets.degree02 line 30
  9. def OAI.MaximalSeshadri.QuadraticJets.jet20 line 32
  10. def OAI.MaximalSeshadri.QuadraticJets.jet11 line 34
  11. def OAI.MaximalSeshadri.QuadraticJets.jet02 line 36
  12. def OAI.MaximalSeshadri.QuadraticJets.discriminant line 39
  13. def OAI.MaximalSeshadri.QuadraticJets.coefficientForm line 42
  14. def OAI.MaximalSeshadri.QuadraticJets.discriminantPolynomial line 46
  15. lemma OAI.MaximalSeshadri.QuadraticJets.coefficientForm_eval line 50
  16. lemma OAI.MaximalSeshadri.QuadraticJets.discriminantPolynomial_eval line 55
  17. lemma OAI.MaximalSeshadri.QuadraticJets.quarticCombination_add line 61
  18. lemma OAI.MaximalSeshadri.QuadraticJets.quarticCombination_single line 65
  19. lemma OAI.MaximalSeshadri.QuadraticJets.discriminant_squares line 70
  20. lemma OAI.MaximalSeshadri.QuadraticJets.discriminantPolynomial_ne_zero line 92
  21. lemma OAI.MaximalSeshadri.QuadraticJets.quarticCombination_mem_square line 111
  22. theorem OAI.MaximalSeshadri.QuadraticJets.exists_quadratic_jet_of_etale line 124