Pic0_exists_mk_eq_and_dvd_ord_of_mem_torsion.lean

theorem exists_ord_eq_mul_of_mk_mem_torsion
    {K F : Type*} [Field K] [Field F] [Algebra K F] {n : ℕ} {x : Pic0 K F}
    (hx : x ∈ Pic0.torsion K F n) {D : Divisor.degZero (K := K) (F := F)}
    (hD : Pic0.mk D = x) :
    ∃ f : F, f ≠ 0 ∧ ∀ v : Place K F, v.ord f = n * (D : Divisor K F) v

theorem exists_mk_eq_and_ord_eq_mul_of_mem_torsion
    {K F : Type*} [Field K] [Field F] [Algebra K F] {n : ℕ} {x : Pic0 K F}
    (hx : x ∈ Pic0.torsion K F n) :
    ∃ (D : Divisor.degZero (K := K) (F := F)) (f : F),
      Pic0.mk D = x ∧ f ≠ 0 ∧ ∀ v : Place K F, v.ord f = n * (D : Divisor K F) v

theorem _root_.AlgebraicCurve.Pic0.exists_mk_eq_and_dvd_ord_of_mem_torsion
    {K F : Type*} [Field K] [Field F] [Algebra K F] {n : ℕ} {x : Pic0 K F}
    (hx : x ∈ Pic0.torsion K F n) :
    ∃ (D : Divisor.degZero (K := K) (F := F)) (f : F),
      Pic0.mk D = x ∧ f ≠ 0 ∧ (∀ v : Place K F, (n : ℤ) ∣ v.ord f) ∧
        ∀ v : Place K F, v.ord f = n * (D : Divisor K F) v