OAI/AlgebraicGeometry/NumericalDimension/AmpleGeneration.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Ample Generation.

  1. lemma OAI.NumericalDimensionOne.divisorSupport_add_of_nonneg line 17
  2. lemma OAI.NumericalDimensionOne.sectionNonvanishing_mul line 37
  3. lemma OAI.NumericalDimensionOne.IsGeneratedAt.add line 52
  4. lemma OAI.NumericalDimensionOne.isGeneratedAt_zero line 66
  5. lemma OAI.NumericalDimensionOne.IsGeneratedAt.nsmul line 74
  6. lemma OAI.NumericalDimensionOne.isOpen_isGeneratedAt line 80
  7. lemma OAI.NumericalDimensionOne.ample_has_generated_power line 91
  8. lemma OAI.NumericalDimensionOne.ample_add_generated line 110
  9. lemma OAI.NumericalDimensionOne.open_le_divisorComplement_of_coeff_zero line 140
  10. lemma OAI.NumericalDimensionOne.exists_effective_multiple_absorbing line 149
  11. lemma OAI.NumericalDimensionOne.exists_generated_twist_at line 176
  12. lemma OAI.NumericalDimensionOne.eventually_generated_twist_of_generated line 214
  13. lemma OAI.NumericalDimensionOne.eventually_generated_cartier_twist line 233
  14. theorem OAI.NumericalDimensionOne.ample_eventual_cartier_twist line 256