mem_subring_iff

Mathlib.NumberTheory.Padics.PadicIntegers

URI: https://scilib.ai/kg/mathlib#PadicInt.mem_subring_iff

English

For any x in ℚ_p, x belongs to the p-adic integers ℤ_p if and only if the p-adic norm is at most 1.

Русский

Для любого x ∈ ℚ_p принадлежность x к п-адическим целым ℤ_p эквивалентна условию ‖x‖ ≤ 1.

LaTeX

$$$x \in \mathbb{Z}_p \iff \|x\|_p \le 1$$$

Lean4

@[simp]
theorem mem_subring_iff {x : ℚ_[p]} : x ∈ subring p ↔ ‖x‖ ≤ 1 :=
  Iff.rfl

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

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

Разделы

Аффилиация

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