AlgebraicCurve.Pic0.mem_closure_mk_single_sub_single
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
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.Pic0.mem_closure_mk_single_sub_single
{K F : Type*} [Field K] [Field F] [Algebra K F] (h1 : ∀ v : Place K F, v.deg = 1)
(V₀ : Place K F) (x : Pic0 K F) :
x ∈ AddSubgroup.closure
{y : Pic0 K F | ∃ (V : Place K F)
(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⟩}