valMinAbs_natCast_of_le_half

Mathlib.Data.ZMod.ValMinAbs

URI: https://scilib.ai/kg/mathlib#ZMod.valMinAbs_natCast_of_le_half

← MathLib Explorer

English

If n/2 < a < n, then (a : ZMod n).valMinAbs = a - n.

Русский

Если n/2 < a < n, то (a : ZMod n).valMinAbs = a - n.

LaTeX

$$$ (ha : n/2 < a) (ha' : a < n) \\Rightarrow (a : \\mathbb{Z}/n\\mathbb{Z}).valMinAbs = a - n$$$

Lean4

theorem valMinAbs_natCast_of_le_half (ha : a ≤ n / 2) : (a : ZMod n).valMinAbs = a :=
  by
  cases n
  · simp
  · simp [valMinAbs_def_pos, val_natCast, Nat.mod_eq_of_lt (ha.trans_lt <| Nat.div_lt_self' _ 0), ha]

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

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

Разделы

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

Аффилиация

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