OAI/AlgebraicGeometry/Seshadri/Bertini/LinearFamilies.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MaximalSeshadri.LinearBertini.parameters_dependent line 14
  2. theorem OAI.MaximalSeshadri.LinearBertini.parameters_polynomial line 32
  3. lemma OAI.MaximalSeshadri.LinearBertini.parameters_polynomial_image line 46
  4. theorem OAI.MaximalSeshadri.LinearBertini.incidence_polynomial line 61
  5. def OAI.MaximalSeshadri.LinearBertini.universalSection line 107
  6. def OAI.MaximalSeshadri.LinearBertini.universalGradient line 110
  7. def OAI.MaximalSeshadri.LinearBertini.criticalIdeal line 114
  8. theorem OAI.MaximalSeshadri.LinearBertini.universal_critical_polynomial line 118
  9. def OAI.MaximalSeshadri.LinearBertini.specializedSection line 156
  10. def OAI.MaximalSeshadri.LinearBertini.specializedGradient line 159
  11. theorem OAI.MaximalSeshadri.LinearBertini.critical_specialization_eq_top line 165
  12. lemma OAI.MaximalSeshadri.LinearBertini.specializedGradient_eq line 222
  13. theorem OAI.MaximalSeshadri.LinearBertini.affine_bertini_smooth line 229
  14. theorem OAI.MaximalSeshadri.LinearBertini.affine_bertini line 253
  15. theorem OAI.MaximalSeshadri.LinearBertini.simultaneous_affine_bertini line 262
  16. theorem OAI.MaximalSeshadri.SchemeBertini.smooth_subscheme_of_affine_quotients line 291
  17. theorem OAI.MaximalSeshadri.SchemeBertini.smooth_linear_family line 329