AlgebraicCurve.exists_ell_nsmul_eq_of_isAlgClosed_of_transcendental
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.Exists_ell_nsmul_eq_of_isAlgClosed_of_transcendental
attribute [-instance]
instIsPrimeCenter
instIsFractionRingIntegralClosureAt
instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
instIsDedekindDomainIntegralClosureAt
instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
AlgebraicCurve.Divisor.evalFun_zero AlgebraicCurve.Place.evalAt_one
AlgebraicCurve.Place.differentialCoeff_zero AlgebraicCurve.Place.differentialCoeff_dCoord
AlgebraicCurve.TranscendenceTower.mk.sizeOf_spec
attribute [-simp] AlgebraicCurve.IntegralBasisInLSpace.mk.injEq
AlgebraicCurve.TranscendenceTower.mk.injEq AlgebraicCurve.PoleDivisorPackage.mk.sizeOf_spec
AlgebraicCurve.IntegralBasisInLSpace.mk.sizeOf_spec AlgebraicCurve.PoleDivisorPackage.mk.injEq
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.exists_ell_nsmul_eq_of_isAlgClosed_of_transcendental
{K F : Type*} [Field K] [IsAlgClosed K] [Field F] [Algebra K F]
(x : F) (hx : Transcendental K x)
[FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
(D : Divisor K F) (hD : ∀ v : Place K F, D v = max 0 (-v.ord x)) :
ell (0 : Divisor K F) = 1 ∧
∃ M : ℕ, 1 ≤ M ∧ ∀ N, M ≤ N →
(ell (N • D) : ℤ) = N * Divisor.degree D + 1 - genusFF K F