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

• x_2.valMinAbs = x_2
• x_2.valMinAbs = if x_2.val ≤ n.succ / 2 then ↑x_2.val else ↑x_2.val - ↑n.succ

@[simp]

theorem ZMod.valMinAbs_def_zero (x : ZMod 0) : x.valMinAbs = x

theorem ZMod.valMinAbs_def_pos {n : ℕ} [NeZero n] (x : ZMod n) : x.valMinAbs = if x.val ≤ n / 2 then ↑x.val else ↑x.val - ↑n

@[simp]

theorem ZMod.coe_valMinAbs {n : ℕ} (x : ZMod n) : ↑x.valMinAbs = x

theorem ZMod.injective_valMinAbs {n : ℕ} : Function.Injective valMinAbs

theorem ZMod.valMinAbs_nonneg_iff {n : ℕ} [NeZero n] (x : ZMod n) : 0 ≤ x.valMinAbs ↔ x.val ≤ n / 2

theorem ZMod.valMinAbs_mul_two_eq_iff {n : ℕ} (a : ZMod n) : a.valMinAbs * 2 = ↑n ↔ 2 * a.val = 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

theorem ZMod.natAbs_valMinAbs_le {n : ℕ} [NeZero n] (x : ZMod n) : x.valMinAbs.natAbs ≤ n / 2

@[simp]

theorem ZMod.valMinAbs_zero (n : ℕ) : valMinAbs 0 = 0

@[simp]

theorem ZMod.valMinAbs_eq_zero {n : ℕ} (x : ZMod n) : x.valMinAbs = 0 ↔ x = 0

theorem ZMod.natCast_natAbs_valMinAbs {n : ℕ} [NeZero n] (a : ZMod n) : ↑a.valMinAbs.natAbs = if a.val ≤ n / 2 then a else -a

theorem ZMod.valMinAbs_neg_of_ne_half {n : ℕ} {a : ZMod n} (ha : 2 * a.val ≠ n) : (-a).valMinAbs = -a.valMinAbs

@[simp]

theorem ZMod.natAbs_valMinAbs_neg {n : ℕ} (a : ZMod n) : (-a).valMinAbs.natAbs = a.valMinAbs.natAbs

theorem ZMod.val_eq_ite_valMinAbs {n : ℕ} [NeZero n] (a : ZMod n) : ↑a.val = a.valMinAbs + ↑(if a.val ≤ n / 2 then 0 else n)

theorem ZMod.prime_ne_zero (p q : ℕ) [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (hpq : p ≠ q) : ↑q ≠ 0

theorem ZMod.valMinAbs_natAbs_eq_min {n : ℕ} [hpos : NeZero n] (a : ZMod n) : a.valMinAbs.natAbs = min a.val (n - a.val)

theorem ZMod.valMinAbs_natCast_of_le_half {n a : ℕ} (ha : a ≤ n / 2) : (↑a).valMinAbs = ↑a

theorem ZMod.valMinAbs_natCast_of_half_lt {n a : ℕ} (ha : n / 2 < a) (ha' : a < n) : (↑a).valMinAbs = ↑a - ↑n

@[simp]

theorem ZMod.valMinAbs_natCast_eq_self {n a : ℕ} [NeZero n] : (↑a).valMinAbs = ↑a ↔ a ≤ n / 2

theorem ZMod.natAbs_valMinAbs_add_le {n : ℕ} (a b : ZMod n) : (a + b).valMinAbs.natAbs ≤ (a.valMinAbs + b.valMinAbs).natAbs