OAI/AlgebraicGeometry/Seshadri/Bertini/GenericHyperplanes.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MaximalSeshadri.BertiniIntegral.universalHyperplane_geometricGeneric_domain line 24
  2. lemma OAI.MaximalSeshadri.BertiniIntegral.mvC_nonZeroDivisor line 49
  3. lemma OAI.MaximalSeshadri.BertiniIntegral.homogeneousLinearForm_regular_of_coefficient line 58
  4. lemma OAI.MaximalSeshadri.BertiniIntegral.quotient_regular_of_dvd line 73
  5. lemma OAI.MaximalSeshadri.BertiniIntegral.linearForm_coefficient_saturated line 85
  6. theorem OAI.MaximalSeshadri.BertiniIntegral.homogeneousLinearForm_isPrime_of_regularPair line 107
  7. def OAI.MaximalSeshadri.BertiniIntegral.mvPolynomialMapOver line 140
  8. lemma OAI.MaximalSeshadri.BertiniIntegral.mvPolynomialMapOver_C line 151
  9. lemma OAI.MaximalSeshadri.BertiniIntegral.mvPolynomialMapOver_X line 153
  10. def OAI.MaximalSeshadri.BertiniIntegral.mvPolynomialTensorTo line 156
  11. abbrev OAI.MaximalSeshadri.BertiniIntegral.mvPolynomialTensorCoeff line 160
  12. def OAI.MaximalSeshadri.BertiniIntegral.mvPolynomialTensorFrom line 166
  13. lemma OAI.MaximalSeshadri.BertiniIntegral.mvPolynomialTensorTo_left line 176
  14. lemma OAI.MaximalSeshadri.BertiniIntegral.mvPolynomialTensorTo_right line 181
  15. lemma OAI.MaximalSeshadri.BertiniIntegral.mvPolynomialTensorFrom_C_tmul line 186
  16. lemma OAI.MaximalSeshadri.BertiniIntegral.mvPolynomialTensorFrom_X line 190
  17. lemma OAI.MaximalSeshadri.BertiniIntegral.mvPolynomialTensorTo_tmul line 195
  18. lemma OAI.MaximalSeshadri.BertiniIntegral.mvPolynomialTensorFrom_left line 201
  19. lemma OAI.MaximalSeshadri.BertiniIntegral.mvPolynomialTensorFrom_right line 219
  20. lemma OAI.MaximalSeshadri.BertiniIntegral.mvPolynomialTensorFrom_to line 241
  21. lemma OAI.MaximalSeshadri.BertiniIntegral.mvPolynomialTensorTo_from line 260
  22. def OAI.MaximalSeshadri.BertiniIntegral.mvPolynomialTensorEquiv line 280
  23. lemma OAI.MaximalSeshadri.BertiniIntegral.mvPolynomialTensorEquiv_left line 284
  24. lemma OAI.MaximalSeshadri.BertiniIntegral.mvPolynomialTensorEquiv_right line 289
  25. theorem OAI.MaximalSeshadri.BertiniIntegral.tensor_polynomial_relation line 302
  26. theorem OAI.MaximalSeshadri.BertiniIntegral.hyperplaneFamily_double_isDomain line 384