valMinAbs_natAbs_eq_min — Mathlib

English

For [NeZero n], (a.valMinAbs.natAbs : ZMod n) equals if a.val ≤ n/2 then a else -a.

Русский

Для [NeZero n], (a.valMinAbs.natAbs : ZMod n) равно если a.val ≤ n/2 то a иначе -a.

LaTeX

$$$[\\mathrm{NeZero}\\ n]\\ (a : \\mathbb{Z}/n\\mathbb{Z}).valMinAbs.natAbs = \\text{if } a.val \\le \\frac{n}{2} \\text{ then } a \\text{ else } -a$$$

Lean4

theorem valMinAbs_natAbs_eq_min [hpos : NeZero n] (a : ZMod n) : a.valMinAbs.natAbs = min a.val (n - a.val) :=
  by
  rw [valMinAbs_def_pos]
  have := a.val_lt
  omega

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