OAI/AlgebraicGeometry/Seshadri/Bertini/CriticalLocus.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MaximalSeshadri.Bertini.mapBaseChange_injective_formallySmooth line 12
  2. theorem OAI.MaximalSeshadri.Bertini.algebraicIndependent_differentials line 26
  3. theorem OAI.MaximalSeshadri.Bertini.universal_hyperplane_parameters_dependent line 57
  4. theorem OAI.MaximalSeshadri.Bertini.critical_parameters_polynomial line 73
  5. lemma OAI.MaximalSeshadri.Bertini.critical_parameters_polynomial_image line 87
  6. theorem OAI.MaximalSeshadri.Bertini.critical_incidence_polynomial line 108
  7. lemma OAI.MaximalSeshadri.Bertini.differential_expansion line 154
  8. lemma OAI.MaximalSeshadri.Bertini.critical_of_coordinates line 162
  9. def OAI.MaximalSeshadri.Bertini.universalSection line 176
  10. def OAI.MaximalSeshadri.Bertini.universalGradient line 179
  11. def OAI.MaximalSeshadri.Bertini.criticalIdeal line 183
  12. theorem OAI.MaximalSeshadri.Bertini.universal_critical_polynomial line 187
  13. def OAI.MaximalSeshadri.Bertini.specializedSection line 219
  14. def OAI.MaximalSeshadri.Bertini.specializedGradient line 222
  15. theorem OAI.MaximalSeshadri.Bertini.critical_specialization_eq_top line 228
  16. theorem OAI.MaximalSeshadri.Bertini.formallySmooth_principal_of_derivation line 281
  17. theorem OAI.MaximalSeshadri.Bertini.formallySmooth_principal_of_gradient line 300
  18. theorem OAI.MaximalSeshadri.Bertini.formallySmooth_quotient_of_gradient line 317
  19. lemma OAI.MaximalSeshadri.Bertini.specializedGradient_eq line 345
  20. theorem OAI.MaximalSeshadri.Bertini.affine_bertini_smooth line 352