OAI/AlgebraicGeometry/Seshadri/Bertini/DifferentialFrames.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MaximalSeshadri.FrameBertini.DifferentialFrame line 12
  2. theorem OAI.MaximalSeshadri.FrameBertini.exists_differentialFrame line 18
  3. lemma OAI.MaximalSeshadri.FrameBertini.differential_expansion line 36
  4. lemma OAI.MaximalSeshadri.FrameBertini.critical_of_coordinates line 44
  5. def OAI.MaximalSeshadri.FrameBertini.universalSection line 59
  6. def OAI.MaximalSeshadri.FrameBertini.universalGradient line 62
  7. def OAI.MaximalSeshadri.FrameBertini.criticalIdeal line 66
  8. theorem OAI.MaximalSeshadri.FrameBertini.universal_critical_polynomial line 70
  9. def OAI.MaximalSeshadri.FrameBertini.specializedSection line 104
  10. def OAI.MaximalSeshadri.FrameBertini.specializedGradient line 107
  11. theorem OAI.MaximalSeshadri.FrameBertini.critical_specialization_eq_top line 113
  12. theorem OAI.MaximalSeshadri.FrameBertini.formallySmooth_principal_of_gradient line 167
  13. theorem OAI.MaximalSeshadri.FrameBertini.formallySmooth_quotient_of_gradient line 184
  14. lemma OAI.MaximalSeshadri.FrameBertini.specializedGradient_eq line 213
  15. theorem OAI.MaximalSeshadri.FrameBertini.affine_bertini_smooth line 220
  16. theorem OAI.MaximalSeshadri.FrameBertini.affine_bertini line 242