natAbs_valMinAbs_le — Mathlib

English

For [NeZero n], natAbs(x.valMinAbs) ≤ n/2 for all x ∈ ZMod n.

Русский

Для [NeZero n] выполняется natAbs(x.valMinAbs) ≤ n/2 для любого x ∈ ZMod n.

LaTeX

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

Lean4

theorem natAbs_valMinAbs_le [NeZero n] (x : ZMod n) : x.valMinAbs.natAbs ≤ n / 2 :=
  by
  rw [Nat.le_div_two_iff_mul_two_le]
  rcases x.valMinAbs.natAbs_eq with h | h
  · rw [← h]
    exact x.valMinAbs_mem_Ioc.2
  · rw [← neg_le_neg_iff, ← neg_mul, ← h]
    exact x.valMinAbs_mem_Ioc.1.le

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