AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FiniteDimLSpaceZeroEllZeroOneAlg.E97cEllZero.main
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Cohomology.RiemannRoch.Proofs.FiniteDimLSpaceZeroEllZeroOneAlg
attribute [-instance]
AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
instIsScalarTowerResidueFieldRestrictPushforward
instAlgebraResidueFieldRestrictPushforward
instIsLocalHomRestrictInclusion
instIsPrimeCenter
instIsFractionRingIntegralClosureAt
instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
instIsDedekindDomainIntegralClosureAt
instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
attribute [-simp] AlgebraicCurve.Divisor.mapRestrict_single
AlgebraicCurve.Divisor.pushforward_single AlgebraicCurve.Place.coe_restrictInclusion
AlgebraicCurve.Place.mem_fiber AlgebraicCurve.Place.restrict_toValuationSubring
AlgebraicCurve.Divisor.degree_pushforward AlgebraicCurve.Place.restrictResidueMap_residue
AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
AlgebraicCurve.Place.placeOfPrime_toValuationSubring AlgebraicCurve.Place.mem_fiberOver
AlgebraicCurve.Place.fiberEquiv_symm_apply AlgebraicCurve.Place.fiberEquiv_apply
AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal AlgebraicCurve.Place.congrEquiv_symm_apply
AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
attribute [-simp] AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
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.TranscendenceTower.mk.sizeOf_spec AlgebraicCurve.IntegralBasisInLSpace.mk.injEq
AlgebraicCurve.TranscendenceTower.mk.injEq AlgebraicCurve.PoleDivisorPackage.mk.sizeOf_spec
AlgebraicCurve.IntegralBasisInLSpace.mk.sizeOf_spec AlgebraicCurve.PoleDivisorPackage.mk.injEq
open AlgebraicCurve
open scoped IntermediateField
namespace E97cEllZeroLean source · statement
theorem main (k : Type*) [Field k] [IsAlgClosed k] {F : Type*} [Field F] [Algebra k F]
(x : F) (hx : Transcendental k x)
(hfin : FiniteDimensional (IntermediateField.adjoin k ({x} : Set F)) F) :
FiniteDimensional k ↥(LSpace (0 : Divisor k F)) ∧ ell (0 : Divisor k F) = 1