AlgebraicCurve.Pic0.mem_closure_mk_single_sub_single_of_notMem
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_mem_closure_mk_single_sub_single_of_notMem
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.Pic0.mem_closure_mk_single_sub_single_of_notMem
{K : Type*} [Field K] [IsAlgClosed K] {F : Type*} [Field F] [Algebra K F]
[Algebra.EssFiniteType K F] [IsCurveOver K F]
(S : Finset (Place K F)) (V₀ : Place K F) (hV₀ : V₀ ∉ S) (x : Pic0 K F) :
x ∈ AddSubgroup.closure
{y : Pic0 K F | ∃ (V : Place K F) (_ : V ∉ S)
(h : Finsupp.single V (1 : ℤ) - Finsupp.single V₀ 1 ∈ Divisor.degZero (K := K) (F := F)),
y = Pic0.mk ⟨Finsupp.single V (1 : ℤ) - Finsupp.single V₀ 1, h⟩}