Exists_forall_subsingleton_cechH1_nsmul_of_degree_pos_of_riemannGenusReachedAt.lean

theorem finrank_riemannRochSpace_add_eq {K F : Type*} [Field K] [Field F] [Algebra K F]
    (D P : Divisor K F) (h : F) (hh : h ≠ 0) (hP : ∀ v : Place K F, P v = v.ord h) :
    Module.finrank K ↥(riemannRochSpace (D + P)) = Module.finrank K ↥(riemannRochSpace D)

theorem exists_forall_subsingleton_cechH1_nsmul_of_degree_pos_of_riemannGenusReachedAt
    {K F : Type*} [Field K] [Field F] [Algebra K F] [IsCurveOver K F]
    [FiniteDimensional K ↥(riemannRochSpace (0 : Divisor K F))]
    {γ : ℤ} {D₀ : Divisor K F} (hγ : RiemannGenusReachedAt γ D₀)
    {S₀ S₁ : Set (Place K F)} (hcover : S₀ ∪ S₁ = Set.univ) (h₀ : ∃ v, v ∉ S₀) (h₁ : ∃ v, v ∉ S₁)
    (D : Divisor K F) (hD : 0 < Divisor.degree D) :
    ∃ N : ℕ, ∀ n : ℕ, N ≤ n → Subsingleton (cechH1 S₀ S₁ ((n : ℤ) • D))