Documentation

Atlas.ArithmeticGeometry.code.CompletenessResidueK

source
def HasResidueFieldK {k : Type u} [Field k] {V : AlgebraicGeometry.CompletenessValuationCriterion.AlgVariety k} (R : AlgebraicGeometry.CompletenessValuationCriterion.ValRingOver V) :
Prop
Instances For
    source
    def SatisfiesValuationCriterionResidueK {k : Type u} [Field k] (X : AlgebraicGeometry.CompletenessValuationCriterion.AlgVariety k) :
    Prop
    Instances For
      source
      theorem corollary_16_31 {k : Type u} [Field k] [IsAlgClosed k] (X : AlgebraicGeometry.CompletenessValuationCriterion.AlgVariety k) (hX : SatisfiesValuationCriterionResidueK X) :
      IsCompleteVariety X.carrier