AlgebraicCurve.Pic0.exists_ord_eq_mul_of_nsmul_mk_eq_zero
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_exists_ord_eq_mul_of_nsmul_mk_eq_zero
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.Pic0.exists_ord_eq_mul_of_nsmul_mk_eq_zero
{K F : Type*} [Field K] [Field F] [Algebra K F]
(D : ↥(Divisor.degZero (K := K) (F := F))) (n : ℕ) (h : n • Pic0.mk D = 0) :
∃ f : F, f ≠ 0 ∧ ∀ v : Place K F, v.ord f = (n : ℤ) * (D : Divisor K F) v