natAbs_valMinAbs_neg

Mathlib.Data.ZMod.ValMinAbs

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

← MathLib Explorer

English

natAbs((-a).valMinAbs) = natAbs(a.valMinAbs).

Русский

natAbs((-a).valMinAbs) = natAbs(a.valMinAbs).

LaTeX

$$$\\operatorname{natAbs}((-a).valMinAbs) = \\operatorname{natAbs}(a.valMinAbs)$$$

Lean4

@[simp]
theorem natAbs_valMinAbs_neg (a : ZMod n) : (-a).valMinAbs.natAbs = a.valMinAbs.natAbs :=
  by
  by_cases h2a : 2 * a.val = n
  · rw [a.neg_eq_self_iff.2 (Or.inr h2a)]
  · rw [valMinAbs_neg_of_ne_half h2a, Int.natAbs_neg]

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

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

Разделы

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

Аффилиация

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