valMinAbs_def_pos — Mathlib

English

For nonzero n, valMinAbs x equals x.val if x.val ≤ n/2, otherwise x.val − n.

Русский

Для непустого n valMinAbs x равен x.val, если x.val ≤ n/2, иначе x.val − n.

LaTeX

$$$$ \\mathrm{valMinAbs}(x) = \\begin{cases} x^{\\text{val}} & \\text{if } x^{\\text{val}} \\le n/2, \\\\ x^{\\text{val}} - n & \\text{otherwise}. \\end{cases} $$$$

Lean4

theorem valMinAbs_def_pos :
    ∀ {n : ℕ} [NeZero n] (x : ZMod n), valMinAbs x = if x.val ≤ n / 2 then (x.val : ℤ) else x.val - n
  | 0, _, x => by cases NeZero.ne 0 rfl
  | n + 1, _, x => rfl

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