AlgebraicCurve.Pic0.torsion.move_of_forall_isRational
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_torsion_move_of_forall_isRational
noncomputable section
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.Pic0.torsion.move_of_forall_isRational {K F : Type*} [Field K]
[Field F] [Algebra K F] [HasPrincipalDivisors K F] (hrat : ∀ v : Place K F, v.IsRational)
(n : ℕ) (x : Pic0.torsion K F n) (S : Finset (Place K F)) :
∃ D : Divisor.degZero (K := K) (F := F),
Pic0.mk D = (x : Pic0 K F) ∧
(∀ v ∈ (D : Divisor K F).support, Place.IsRational v) ∧
(∀ v ∈ (D : Divisor K F).support, v ∉ S)