AlgebraicCurve.exists_injective_ell_sub_sum_single_eq_zero_of_card_le
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Proofs.Exists_injective_ell_sub_sum_single_eq_zero_of_card_le
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.exists_injective_ell_sub_sum_single_eq_zero_of_card_le
{K F : Type*} [Field K] [Field F] [Algebra K F] [IsCurveOver K F]
[Algebra.EssFiniteType K F]
(G : Divisor K F) {n : ℕ} (hn : ell G = n)
(X S : Finset (Place K F)) (hS : ∀ v ∈ S, v.deg = 1)
(hcard : (X.card : ℤ) + Divisor.degree G + 1 ≤ S.card) :
∃ Q : Fin n → Place K F, Function.Injective Q ∧ (∀ l, Q l ∈ S ∧ Q l ∉ X) ∧
ell (G - ∑ l, Finsupp.single (Q l) 1) = 0