OAI/AlgebraicGeometry/Seshadri/Bertini/Derivations.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MaximalSeshadri.BertiniIntegral.aeval_injective_of_derivation line 13
  2. def OAI.MaximalSeshadri.BertiniIntegral.mvCoeffDerivation line 38
  3. theorem OAI.MaximalSeshadri.BertiniIntegral.mvCoeffDerivation_coeff line 71
  4. theorem OAI.MaximalSeshadri.BertiniIntegral.mvCoeffDerivation_C line 75
  5. theorem OAI.MaximalSeshadri.BertiniIntegral.mvCoeffDerivation_X line 81
  6. theorem OAI.MaximalSeshadri.BertiniIntegral.mvCoeffDerivation_algebraMap line 87
  7. def OAI.MaximalSeshadri.BertiniIntegral.mvParameterDerivation line 94
  8. theorem OAI.MaximalSeshadri.BertiniIntegral.hyperplane_aeval_injective line 106
  9. theorem OAI.MaximalSeshadri.BertiniIntegral.genericFiber_isDomain line 141
  10. def OAI.MaximalSeshadri.BertiniIntegral.doubledBaseChangeEquiv line 153
  11. theorem OAI.MaximalSeshadri.BertiniIntegral.doubledGenericFiber_isDomain line 160
  12. theorem OAI.MaximalSeshadri.BertiniIntegral.finiteType_rationalPoint line 179
  13. theorem OAI.MaximalSeshadri.BertiniIntegral.finiteType_point_nonvanishing line 188
  14. def OAI.MaximalSeshadri.tensorSpecialize line 212
  15. lemma OAI.MaximalSeshadri.tensorSpecialize_repr line 216
  16. theorem OAI.MaximalSeshadri.tensorProduct_isDomain line 223