norm_sub_zmodRepr_lt_one

Mathlib.NumberTheory.Padics.RingHoms

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

← MathLib Explorer

English

The norm of x − zmodRepr x is less than 1: ∥x − zmodRepr x∥ < 1.

Русский

Норма разности x − zmodRepr(x) меньше 1: ∥x − zmodRepr(x)∥ < 1.

LaTeX

$$∥x - zmodRepr(x)∥ < 1$$

Lean4

theorem norm_sub_zmodRepr_lt_one (x : ℤ_[p]) : ‖x - x.zmodRepr‖ < 1 :=
  by
  rw [← mem_nonunits, ← IsLocalRing.mem_maximalIdeal]
  exact sub_zmodRepr_mem _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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