val_eq_ite_valMinAbs

Mathlib.Data.ZMod.ValMinAbs

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

← MathLib Explorer

English

x.valMinAbs = y iff x = y.cast and 2y ∈ Ioc(-n, n).

Русский

x.valMinAbs = y тогда и только тогда, когда x = y.cast и 2y ∈ Ioc(-n, n).

LaTeX

$$$x.valMinAbs = y \\iff (x = y.cast) \\land (2 y \\in (-n, n])$$$

Lean4

theorem val_eq_ite_valMinAbs [NeZero n] (a : ZMod n) : (a.val : ℤ) = a.valMinAbs + if a.val ≤ n / 2 then 0 else n :=
  by
  rw [valMinAbs_def_pos]
  split_ifs <;> simp [add_zero, sub_add_cancel]

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

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

Разделы

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

Аффилиация

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