instTop

Mathlib.RingTheory.Valuation.ValuationSubring

URI: https://scilib.ai/kg/mathlib#ValuationSubring.instTop

English

There is a top valuation subring given by the entire field K.

Русский

Существуют верхнее значение (top) валюационное подкольцо, соответствующее всему полю K.

LaTeX

$$Top$(\text{ValuationSubring } K)$ corresponds to $\top = (\text{Subring }K)$$$

Lean4

instance : Top (ValuationSubring K) :=
  Top.mk <| { (⊤ : Subring K) with mem_or_inv_mem' := fun _ => Or.inl trivial }

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

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

Разделы

Аффилиация

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