Module

ConstantsAreBase_of_isAlgClosed.lean

Nyll.AlgebraicCurves.FunctionFields.ConstantsAreBase_of_isAlgClosed

1 declaration indexed from sourceView source ↗

Module documentation

Constants Are Base of is Alg Closed

Imports9

Imported by13

theorem

constantsAreBase_of_isAlgClosed

L51 ↗

AlgebraicCurve.constantsAreBase_of_isAlgClosed

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.ConstantsAreBase_of_isAlgClosed
attribute [-instance]
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
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
open AlgebraicCurve

Lean source · statement

theorem _root_.AlgebraicCurve.constantsAreBase_of_isAlgClosed (K F : Type*) [Field K] [Field F]
  [Algebra K F]
    [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F]
    [FiniteDimensional (RatFunc K) F] [Algebra.IsSeparable (RatFunc K) F]
    [IsAlgClosed K] [AlgebraicCurve.IsCurveOver K F] :
    AlgebraicCurve.ConstantsAreBase K F

Module documentation

Constants Are Base of is Alg Closed

Declarations

constantsAreBase_of_isAlgClosed