sub_zmodRepr_mem

Mathlib.NumberTheory.Padics.RingHoms

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

English

The difference x − zmodRepr x lies in the maximal ideal of ℤ_p; i.e., x − zmodRepr x is a nonunit in ℤ_p.

Русский

Разность x − zmodRepr(x) принадлежит максимальному идеалу ℤ_p; то есть она не является обратимой.

LaTeX

$$$x - zmodRepr(x) \in \mathfrak{m}_{\mathbb{Z}_{(p)}}$$$

Lean4

theorem sub_zmodRepr_mem : x - zmodRepr x ∈ maximalIdeal ℤ_[p] :=
  (zmodRepr_spec _).2

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

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

Разделы

Аффилиация

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