OAI/NumberTheory/PiExponent/Ampleness/ExceptionalCurveDegree.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.ExceptionalCurveDegree.inverseSection line 24
  2. theorem OAI.PiExponent.ExceptionalCurveDegree.inverseSection_zeroIdeal line 28
  3. theorem OAI.PiExponent.ExceptionalCurveDegree.inverseSection_zeroIdeal_eq_comap line 58
  4. theorem OAI.PiExponent.ExceptionalCurveDegree.zeroIdeal_pullback line 66
  5. theorem OAI.PiExponent.ExceptionalCurveDegree.zeroIdeal_zero line 99
  6. theorem OAI.PiExponent.ExceptionalCurveDegree.pullback_inverseSection_zeroIdeal line 111
  7. theorem OAI.PiExponent.ExceptionalCurveDegree.pullback_inverseSection_ne_zero line 121
  8. theorem OAI.PiExponent.ExceptionalCurveDegree.zeroIdeal_spec_top line 132
  9. def OAI.PiExponent.ExceptionalCurveDegree.localIdeal line 147
  10. theorem OAI.PiExponent.ExceptionalCurveDegree.localIdeal_specIdeal line 152
  11. theorem OAI.PiExponent.ExceptionalCurveDegree.localIdeal_compactIdeal line 165
  12. theorem OAI.PiExponent.ExceptionalCurveDegree.localIdeal_eq_top_of_not_mem line 177
  13. theorem OAI.PiExponent.ExceptionalCurveDegree.map_powerIdeal_eq_top_of_transcendental line 195
  14. theorem OAI.PiExponent.ExceptionalCurveDegree.compactIdeal_comap_ne_bot_of_generic line 231
  15. theorem OAI.PiExponent.ExceptionalCurveDegree.centerMorphism_eq_centeredLift line 259
  16. theorem OAI.PiExponent.ExceptionalCurveDegree.localIdeal_length_eq_logContact line 277
  17. theorem OAI.PiExponent.ExceptionalCurveDegree.divisor_eq_localIdeal_length line 315
  18. def OAI.PiExponent.ExceptionalCurveDegree.idealDivisor line 345
  19. theorem OAI.PiExponent.ExceptionalCurveDegree.idealDivisor_apply line 350
  20. theorem OAI.PiExponent.ExceptionalCurveDegree.degree_eq_neg_idealDivisor_sum line 363
  21. theorem OAI.PiExponent.ExceptionalCurveDegree.compactIdeal_degree_eq_neg_contact_sum line 381
  22. theorem OAI.PiExponent.ExceptionalCurveDegree.admissible_degree_eq_neg_contactSum line 471