OAI/NumberTheory/PiExponent/Cohomology/FiniteLineEuler.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponentSeshadri.Geometry.overFrame line 13
  2. def OAI.PiExponentSeshadri.FiniteSupport.pointOpen line 28
  3. lemma OAI.PiExponentSeshadri.FiniteSupport.pointOpen_basis line 30
  4. def OAI.PiExponentSeshadri.FiniteSupport.pointFrame line 35
  5. theorem OAI.PiExponentSeshadri.FiniteSupport.lineBundle_trivial line 45
  6. theorem OAI.PiExponentSeshadri.FiniteSupport.finite_line_pushforward_euler line 113
  7. theorem OAI.PiExponentSeshadri.FiniteSupport.finite_line_pushforward_finiteDimensional line 124
  8. theorem OAI.PiExponentSeshadri.FiniteSupport.finite_line_euler_eq_sum_stalks line 141
  9. theorem OAI.PiExponentSeshadri.FiniteSupport.finite_line_euler_eq_sum_stalk_lengths line 153