isClopen_valuationSubring

Mathlib.Topology.Algebra.Valued.ValuationTopology

URI: https://scilib.ai/kg/mathlib#Valued.isClopen_valuationSubring

← MathLib Explorer

English

The valuation subring hv.v.valuationSubring is clopen.

Русский

Подкольцо оценки hv.v.valuationSubring является клипом (clopen).

LaTeX

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

Lean4

/-- The valuation subring of a valued field is clopen. -/
theorem isClopen_valuationSubring (K : Type u) [Field K] [hv : Valued K Γ₀] :
    IsClopen (hv.v.valuationSubring : Set K) :=
  isClopen_integer K

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru