natAbs_valMinAbs_add_le — Mathlib

English

For any a,b ∈ ZMod n, the natAbs of valMinAbs of a+b is at most the natAbs of (valMinAbs a + valMinAbs b).

Русский

Для любых a,b ∈ ZMod n, natAbs((a+b).valMinAbs) ≤ natAbs(a.valMinAbs + b.valMinAbs).

LaTeX

$$$\\forall a,b \\in \\mathbb{Z}/n\\mathbb{Z},\\ (a+b).valMinAbs.natAbs \\le\\ (a.valMinAbs + b.valMinAbs).natAbs$$$

Lean4

theorem natAbs_valMinAbs_add_le (a b : ZMod n) : (a + b).valMinAbs.natAbs ≤ (a.valMinAbs + b.valMinAbs).natAbs :=
  by
  rcases n with - | n
  · rfl
  apply natAbs_min_of_le_div_two n.succ
  · simp_rw [Int.cast_add, coe_valMinAbs]
  · apply natAbs_valMinAbs_le

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