zmodRepr_lt_p

Mathlib.NumberTheory.Padics.RingHoms

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

English

For every x ∈ ℤ_p, the residue representative zmodRepr x is strictly less than p.

Русский

Для каждого x ∈ ℤ_p остаток zmodRepr x строго меньше p.

LaTeX

$$$x \in \mathbb{Z}_{(p)} \implies zmodRepr(x) < p$$$

Lean4

theorem zmodRepr_lt_p : zmodRepr x < p :=
  (zmodRepr_spec _).1

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

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

Разделы

Аффилиация

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