isClosed_valuationSubring — Mathlib

English

For a valued field K with hv, the valuationSubring hv.v.valuationSubring is a closed subset of K.

Русский

Для поля K с hv, подкольцо оценки hv.v.valuationSubring замкнуто в K.

LaTeX

$$IsClosed( hv.v.valuationSubring : Set K )$$

Lean4

/-- The valuation subring of a valued field is closed. -/
theorem isClosed_valuationSubring (K : Type u) [Field K] [hv : Valued K Γ₀] :
    IsClosed (hv.v.valuationSubring : Set K) :=
  isClosed_integer K

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