valMinAbs_natCast_eq_self — Mathlib

English

Equivalent formulation: the previous statement holds equivalently for Nat indices; (a.cast).valMinAbs = a iff a ≤ n/2.

Русский

Эквивалентная формулировка: (a.cast).valMinAbs = a тогда и только тогда, когда a ≤ n/2.

LaTeX

$$$\\text{Eq}\ (a.cast).valMinAbs\ \ a\ \iff\ a \\le \\frac{n}{2}$$$

Lean4

@[simp]
theorem valMinAbs_natCast_eq_self [NeZero n] : (a : ZMod n).valMinAbs = a ↔ a ≤ n / 2 :=
  by
  refine ⟨fun ha => ?_, valMinAbs_natCast_of_le_half⟩
  rw [← Int.natAbs_natCast a, ← ha]
  exact natAbs_valMinAbs_le (n := n) a

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