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