OAI/NumberTheory/PiExponent/Geometry/FiniteCurveZeros.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PiExponentSeshadri.Geometry.proper_finite_scheme_isFinite line 15
  2. lemma OAI.PiExponentSeshadri.Geometry.proper_finite_scheme_isAffine line 19
  3. lemma OAI.PiExponentSeshadri.Geometry.proper_finite_functions line 24
  4. lemma OAI.PiExponentSeshadri.Geometry.proper_finite_germ_surjective line 35
  5. theorem OAI.PiExponentSeshadri.Geometry.proper_finite_stalk_finrank_le line 50
  6. lemma OAI.PiExponentSeshadri.Geometry.proper_irreducible_closed_subsingleton line 82
  7. theorem OAI.PiExponentSeshadri.Geometry.proper_closed_finite_of_dimension_one line 101
  8. theorem OAI.PiExponentSeshadri.Geometry.integral_curve_proper_closed_finite line 119
  9. theorem OAI.PiExponentSeshadri.Geometry.finite_subscheme_of_curve line 130
  10. theorem OAI.PiExponentSeshadri.Geometry.curve_subscheme_isFinite line 148
  11. abbrev OAI.PiExponentSeshadri.Geometry.structuralStalkAlgebra line 155
  12. theorem OAI.PiExponentSeshadri.Geometry.proper_finite_finrank_eq_sum_stalks line 160
  13. theorem OAI.PiExponentSeshadri.Geometry.proper_finite_euler line 195
  14. theorem OAI.PiExponentSeshadri.Geometry.proper_finite_euler_eq_sum_stalk_finrank line 209
  15. theorem OAI.PiExponentSeshadri.Geometry.proper_finite_euler_eq_sum_stalk_lengths line 220