def Hex.Modular.symMod (a : Int) (m : Nat) : Int

The representative of a modulo m in the interval (-m/2, m/2]. For the degenerate modulus zero, this returns a, matching Int.emod's zero-modulus convention.

Equations

• Hex.Modular.symMod a m = if m = 0 then a else have r := a % ↑m; if ↑m < 2 * r then r - ↑m else r

theorem Hex.Modular.symMod_emod {a : Int} {m : Nat} (h : 0 < m) : symMod a m % ↑m = a % ↑m

Symmetric reduction preserves the ordinary nonnegative residue at every positive modulus.

@[simp]

theorem Hex.Modular.symMod_symMod {a : Int} {m : Nat} (h : 0 < m) : symMod (symMod a m) m = symMod a m

Symmetric reduction is idempotent at every positive modulus.

theorem Hex.Modular.symMod_le {a : Int} {m : Nat} (h : 0 < m) : 2 * (symMod a m).natAbs ≤ m

A symmetric representative has absolute value at most half its positive modulus, with the positive representative selected at an even tie.

theorem Hex.Modular.symMod_unique {a x : Int} {m : Nat} (h : 2 * x.natAbs < m) (hx : x % ↑m = a % ↑m) : symMod a m = x

A strictly-half-bounded integer congruent to a is the unique symmetric representative. The strict bound excludes the two representatives at an even tie.