AlgebraicCurve.constantFieldDegreeFormula_of_isConstantFieldExtension_of_isCurveOver
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ConstantFieldDegreeFormula
attribute [-instance]
instIsPrimeCenter
instIsFractionRingIntegralClosureAt
instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
instIsDedekindDomainIntegralClosureAt
instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
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.Place.differentialCoeff_zero
AlgebraicCurve.Place.differentialCoeff_dCoord
AlgebraicCurve.RationalFunctionField.placeInfty_toValuationSubring
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
open AlgebraicCurve inLean source · statement
theorem _root_.AlgebraicCurve.constantFieldDegreeFormula_of_isConstantFieldExtension_of_isCurveOver
{K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
[Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
[Algebra K F] [Algebra F F'] [IsScalarTower K F F']
[PerfectField K] [Algebra.IsAlgebraic K K'] [Algebra.IsIntegral F F']
[Algebra.EssFiniteType K F] [AlgebraicCurve.IsCurveOver K F] [AlgebraicCurve.IsCurveOver K' F']
(hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
(hconst : ∀ y : F, IsAlgebraic K y → y ∈ (algebraMap K F).range) :
AlgebraicCurve.ConstantFieldDegreeFormula K K' F F'