mem_of_integral

Mathlib.RingTheory.Valuation.Integral

URI: https://scilib.ai/kg/mathlib#Valuation.Integers.mem_of_integral

English

If x is integral over O, then x lies in the valuation integer subring.

Русский

Если x интегрировано над O, то x принадлежит подкольцу v.integer.

LaTeX

$$x ∈ v.integer, если IsIntegral O x$$

Lean4

theorem mem_of_integral {x : R} (hx : IsIntegral O x) : x ∈ v.integer :=
  hv.isIntegral_iff_v_le_one.mp hx

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

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

Разделы

Аффилиация

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