mem_integer_iff

Mathlib.RingTheory.Valuation.Integers

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

English

An element r lies in the integer subring if and only if its valuation is at most 1.

Русский

Элемент r принадлежит подкольцу целых, если и только если его оценка не превосходит 1.

LaTeX

$$$r \\in v.integer \\;\\Leftrightarrow\\; v(r) \\le 1$$$

Lean4

theorem mem_integer_iff (r : R) : r ∈ v.integer ↔ v r ≤ 1 := by rfl

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

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

Разделы

Аффилиация

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