OAI/AlgebraicGeometry/NumericalDimension/RationalDegrees.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Rational Degrees.

  1. lemma OAI.NumericalDimensionOne.CartierMultiple.isQCartier line 16
  2. lemma OAI.NumericalDimensionOne.CartierMultiple.degreeOn_eq line 20
  3. theorem OAI.NumericalDimensionOne.qCartierCurveDegree_eq_multiple line 35
  4. def OAI.NumericalDimensionOne.CartierMultiple.add line 42
  5. def OAI.NumericalDimensionOne.CartierMultiple.smul line 60
  6. lemma OAI.NumericalDimensionOne.CartierMultiple.degreeOn_add line 82
  7. lemma OAI.NumericalDimensionOne.CartierMultiple.degreeOn_smul line 92
  8. lemma OAI.NumericalDimensionOne.qCartierCurveDegree_add line 104
  9. lemma OAI.NumericalDimensionOne.qCartierCurveDegree_smul line 114
  10. theorem OAI.NumericalDimensionOne.qCartierCurveDegree_add_smul line 123
  11. theorem OAI.NumericalDimensionOne.curve_nonnegative_of_generated_approximations line 133
  12. def OAI.NumericalDimensionOne.CurveOn.comp line 172
  13. lemma OAI.NumericalDimensionOne.cartierCurveDegree_cartierPullback line 175
  14. lemma OAI.NumericalDimensionOne.qCartierCurveDegree_pullback line 184
  15. lemma OAI.NumericalDimensionOne.cartierCurveDegree_pullback_contracted line 195
  16. lemma OAI.NumericalDimensionOne.qCartierCurveDegree_pullback_contracted line 205
  17. lemma OAI.NumericalDimensionOne.cartierCurveDegree_nonneg_of_ample line 213
  18. lemma OAI.NumericalDimensionOne.qCartierCurveDegree_nonneg_of_ample line 222
  19. lemma OAI.NumericalDimensionOne.IsRelativelyAmpleQ.curveDegree_nonneg line 230
  20. lemma OAI.NumericalDimensionOne.qCartierCurveDegree_neg line 255
  21. lemma OAI.NumericalDimensionOne.qCartierCurveDegree_sub line 260
  22. lemma OAI.NumericalDimensionOne.canonical_difference_antinef_of_commuting line 271
  23. lemma OAI.NumericalDimensionOne.common_model_commutes_over_base line 312
  24. lemma OAI.NumericalDimensionOne.canonical_comparison_boundary line 344
  25. lemma OAI.NumericalDimensionOne.IsCanonicalMMPStep.antinef_on_common_model line 410
  26. lemma OAI.NumericalDimensionOne.IsCanonicalMMPStep.comparison_boundary_on_common_model line 456