AlgebraicCurve.exists_pair_forall_ord_add_eq_zero_of_subset_riemannRochSpace
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.ExistsPairAllOrdAddZeroSubsetRR
open Submodule AlgebraicCurve inLean source · statement
theorem _root_.AlgebraicCurve.exists_pair_forall_ord_add_eq_zero_of_subset_riemannRochSpace
{K F : Type*} [Field K] [Infinite K] [Field F] [Algebra K F]
[AlgebraicCurve.HasPrincipalDivisors K F]
(D : AlgebraicCurve.Divisor K F) (V : Submodule K F) [FiniteDimensional K ↥V]
(hVD : V ≤ AlgebraicCurve.riemannRochSpace D)
(hbpf : ∀ w : AlgebraicCurve.Place K F, ∃ f ∈ V, f ≠ 0 ∧ w.ord f + D w = 0) :
∃ f₁ ∈ V, ∃ f₂ ∈ V, ∀ w : AlgebraicCurve.Place K F,
(f₁ ≠ 0 ∧ w.ord f₁ + D w = 0) ∨ (f₂ ≠ 0 ∧ w.ord f₂ + D w = 0)