valuationSubring_isDiscreteValuationRing

English

Under the same hypotheses, the valuation subring is a discrete valuation ring.

Русский

При тех же предпосылках оценочное подкольцо является дискретной кольцевой структурой.

LaTeX

$$$ IsDiscreteValuationRing\\ (Subtype\\ x\\mapsto x\\in v.valuationSubring). $$$

Lean4

/-- This is Chapter I, Section 1, Proposition 1 in Serre's Local Fields -/
instance valuationSubring_isDiscreteValuationRing [IsCyclic (valueGroup v)] [Nontrivial (valueGroup v)] :
    IsDiscreteValuationRing K₀
    where
  toIsPrincipalIdealRing := valuationSubring_isPrincipalIdealRing v
  toIsLocalRing := inferInstance
  not_a_field' := by rw [ne_eq, ← isField_iff_maximalIdeal_eq]; exact valuationSubring_not_isField v

Похожие утверждения