OAI/AlgebraicGeometry/NumericalDimension/FixedDivisors.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Fixed Divisors.

  1. lemma OAI.NumericalDimensionOne.surfaceCartierPrimeDegree_principal line 19
  2. lemma OAI.NumericalDimensionOne.surfaceIntersection_principal_right line 36
  3. lemma OAI.NumericalDimensionOne.surfaceIntersection_principal_left line 41
  4. def OAI.NumericalDimensionOne.sectionOrderSet line 57
  5. lemma OAI.NumericalDimensionOne.sectionOrderSet_nonempty line 60
  6. lemma OAI.NumericalDimensionOne.sectionOrderSet_nonnegative line 65
  7. def OAI.NumericalDimensionOne.fixedCoefficient line 71
  8. lemma OAI.NumericalDimensionOne.fixedCoefficient_nonnegative line 74
  9. lemma OAI.NumericalDimensionOne.fixedCoefficient_le line 80
  10. lemma OAI.NumericalDimensionOne.exists_fixedCoefficient_eq line 86
  11. lemma OAI.NumericalDimensionOne.fixedCoefficient_support_finite line 93
  12. def OAI.NumericalDimensionOne.fixedPart line 108
  13. lemma OAI.NumericalDimensionOne.fixedPart_nonnegative line 112
  14. lemma OAI.NumericalDimensionOne.fixedPart_le_zeroDivisor line 119
  15. lemma OAI.NumericalDimensionOne.fixedPart_residual_no_fixed_prime line 127
  16. lemma OAI.NumericalDimensionOne.le_fixedPart_iff line 137
  17. lemma OAI.NumericalDimensionOne.divisorSupport_mono_nonnegative line 163
  18. theorem OAI.NumericalDimensionOne.fixedPart_support_subset line 178
  19. theorem OAI.NumericalDimensionOne.fixedPart_prime_image_constant line 190
  20. lemma OAI.NumericalDimensionOne.linearSystem_avoid_finite line 221
  21. lemma OAI.NumericalDimensionOne.surfaceIntersection_effective_disjoint line 278
  22. lemma OAI.NumericalDimensionOne.surfaceIntersection_movable_nonneg line 294
  23. lemma OAI.NumericalDimensionOne.surfaceIntersection_residual_nonneg line 317
  24. lemma OAI.NumericalDimensionOne.isPulledCartierRepresentative_zero_of_equation line 352
  25. lemma OAI.NumericalDimensionOne.IsCartierPullback.zero_representative_of_constant line 366
  26. lemma OAI.NumericalDimensionOne.surfaceCartierPrimeDegree_contracted line 381
  27. lemma OAI.NumericalDimensionOne.surfaceIntersection_contracted line 405
  28. lemma OAI.NumericalDimensionOne.surfacePrimePrime_nonneg line 426
  29. lemma OAI.NumericalDimensionOne.surfacePrimePrime_zero_of_disjoint line 438
  30. def OAI.NumericalDimensionOne.surfacePrimePair line 482
  31. lemma OAI.NumericalDimensionOne.surfacePrimePair_comm line 484
  32. lemma OAI.NumericalDimensionOne.surfaceDegree_eq_pair_sum line 488
  33. lemma OAI.NumericalDimensionOne.surfacePrimePair_nonneg line 496
  34. lemma OAI.NumericalDimensionOne.surfacePrimePair_zero_of_disjoint line 499
  35. lemma OAI.NumericalDimensionOne.surface_prime_contracted_of_not_prime line 514