le_one_of_subsingleton

Mathlib.RingTheory.Valuation.Basic

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

English

If R is a subsingleton, then for every x in R, v(x) ≤ 1.

Русский

Если множество R состоит из одного элемента, то для каждого x ∈ R выполняется v(x) ≤ 1.

LaTeX

$$$\\forall x:\\, R,\\; v(x) \\le 1$$$

Lean4

@[simp]
theorem le_one_of_subsingleton [Subsingleton R] (v : Valuation R Γ₀) {x : R} : v x ≤ 1 := by
  rw [Subsingleton.elim x 1, Valuation.map_one]

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

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

Разделы

Аффилиация

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