valMinAbs_nonneg_iff — Mathlib

English

For [NeZero n], 0 ≤ x.valMinAbs if and only if x.val ≤ n/2.

Русский

Пусть [NeZero n]. Тогда 0 ≤ x.valMinAbs тогда и только тогда, когда x.val ≤ n/2.

LaTeX

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

Lean4

theorem valMinAbs_nonneg_iff [NeZero n] (x : ZMod n) : 0 ≤ x.valMinAbs ↔ x.val ≤ n / 2 :=
  by
  rw [valMinAbs_def_pos]; split_ifs with h
  · exact iff_of_true (Nat.cast_nonneg _) h
  · exact iff_of_false (sub_lt_zero.2 <| Int.ofNat_lt.2 x.val_lt).not_ge h

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