Documentation

Mathlib.Data.ZMod.ValMinAbs

Absolute value in ZMod n #

def ZMod.valMinAbs {n : } :
ZMod n

Returns the integer in the same equivalence class as x that is closest to 0.

The result will be in the interval (-n/2, n/2].

Equations
Instances For
    @[simp]
    @[simp]
    theorem ZMod.coe_valMinAbs {n : } (x : ZMod n) :
    theorem ZMod.valMinAbs_mem_Ioc {n : } [NeZero n] (x : ZMod n) :
    x.valMinAbs * 2 Set.Ioc (-n) n
    theorem ZMod.valMinAbs_spec {n : } [NeZero n] (x : ZMod n) (y : ) :
    x.valMinAbs = y x = y y * 2 Set.Ioc (-n) n
    @[simp]
    theorem ZMod.valMinAbs_zero (n : ) :
    @[simp]
    theorem ZMod.valMinAbs_eq_zero {n : } (x : ZMod n) :
    theorem ZMod.prime_ne_zero (p q : ) [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (hpq : p q) :
    theorem ZMod.valMinAbs_natCast_of_half_lt {n a : } (ha : n / 2 < a) (ha' : a < n) :