mem_valuationSubring_iff

Mathlib.RingTheory.Valuation.ValuationSubring

URI: https://scilib.ai/kg/mathlib#Valuation.mem_valuationSubring_iff

English

An element x belongs to the valuation subring iff its valuation is at most 1.

Русский

Элемент x принадлежит valuationSubring тогда и только тогда, когда v(x) ≤ 1.

LaTeX

$$x \in v.valuationSubring \iff v x \le 1$$

Lean4

@[simp]
theorem mem_valuationSubring_iff (x : K) : x ∈ v.valuationSubring ↔ v x ≤ 1 :=
  Iff.refl _

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

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

Разделы

Аффилиация

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