valMinAbs_natCast_of_half_lt — Mathlib

English

For [NeZero n], ((a.cast) .valMinAbs = a) iff a ≤ n/2.

Русский

Для [NeZero n], ((a.cast).valMinAbs = a) эквивалентно a ≤ n/2.

LaTeX

$$$[\\mathrm{NeZero}\\ n] \\ (a : \\mathbb{Z}/n\\mathbb{Z}).valMinAbs = a \\iff a \\le \\frac{n}{2}$$$

Lean4

theorem valMinAbs_natCast_of_half_lt (ha : n / 2 < a) (ha' : a < n) : (a : ZMod n).valMinAbs = a - n :=
  by
  cases n
  · cases not_lt_bot ha'
  · simp [valMinAbs_def_pos, val_natCast, Nat.mod_eq_of_lt ha', ha.not_ge]

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