# Absolute value in `ZMod n` #

source
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

Instances For

source
@[simp]
theorem ZMod.valMinAbs_def_zero (x : ZMod 0) :
x.valMinAbs = x
source
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
source
@[simp]
theorem ZMod.coe_valMinAbs {n : ℕ} (x : ZMod n) :
↑x.valMinAbs = x
source
theorem ZMod.injective_valMinAbs {n : ℕ} :
Function.Injective valMinAbs
source
@[simp]
theorem ZMod.valMinAbs_inj {n : ℕ} {a b : ZMod n} :
a.valMinAbs = b.valMinAbs ↔ a = b
source
theorem ZMod.valMinAbs_nonneg_iff {n : ℕ} [NeZero n] (x : ZMod n) :
0 ≤ x.valMinAbs ↔ x.val ≤ n / 2
source
theorem ZMod.valMinAbs_mul_two_eq_iff {n : ℕ} (a : ZMod n) :
a.valMinAbs * 2 = ↑n ↔ 2 * a.val = n
source
theorem ZMod.valMinAbs_mem_Ioc {n : ℕ} [NeZero n] (x : ZMod n) :
x.valMinAbs * 2 ∈ Set.Ioc (-↑n) ↑n
source
theorem ZMod.valMinAbs_spec {n : ℕ} [NeZero n] (x : ZMod n) (y : ℤ) :
x.valMinAbs = y ↔ x = ↑y ∧ y * 2 ∈ Set.Ioc (-↑n) ↑n
source
theorem ZMod.natAbs_valMinAbs_le {n : ℕ} [NeZero n] (x : ZMod n) :
x.valMinAbs.natAbs ≤ n / 2
source
theorem ZMod.eq_neg_of_valMinAbs_eq_neg_valMinAbs {n : ℕ} {a b : ZMod n} (h : a.valMinAbs = -b.valMinAbs) :
a = -b
source
@[simp]
theorem ZMod.valMinAbs_zero (n : ℕ) :
valMinAbs 0 = 0
source
@[simp]
theorem ZMod.valMinAbs_eq_zero {n : ℕ} (x : ZMod n) :
x.valMinAbs = 0 ↔ x = 0
source
theorem ZMod.natCast_natAbs_valMinAbs {n : ℕ} [NeZero n] (a : ZMod n) :
↑a.valMinAbs.natAbs = if a.val ≤ n / 2 then a else -a
source
theorem ZMod.valMinAbs_neg_of_ne_half {n : ℕ} {a : ZMod n} (ha : 2 * a.val ≠ n) :
(-a).valMinAbs = -a.valMinAbs
source
@[simp]
theorem ZMod.natAbs_valMinAbs_neg {n : ℕ} (a : ZMod n) :
(-a).valMinAbs.natAbs = a.valMinAbs.natAbs
source
theorem ZMod.natAbs_valMinAbs_eq_natAbs_valMinAbs {n : ℕ} {a b : ZMod n} :
a.valMinAbs.natAbs = b.valMinAbs.natAbs ↔ a = b ∨ a = -b
source
theorem ZMod.abs_valMinAbs_eq_abs_valMinAbs {n : ℕ} {a b : ZMod n} :
|a.valMinAbs| = |b.valMinAbs| ↔ a = b ∨ a = -b
source
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)
source
theorem ZMod.prime_ne_zero (p q : ℕ) [hp : Fact (Nat.Prime p)] [hq : Fact (Nat.Prime q)] (hpq : p ≠ q) :
↑q ≠ 0
source
theorem ZMod.valMinAbs_natAbs_eq_min {n : ℕ} [hpos : NeZero n] (a : ZMod n) :
a.valMinAbs.natAbs = min a.val (n - a.val)
source
theorem ZMod.valMinAbs_natCast_of_le_half {n a : ℕ} (ha : a ≤ n / 2) :
(↑a).valMinAbs = ↑a
source
theorem ZMod.valMinAbs_natCast_of_half_lt {n a : ℕ} (ha : n / 2 < a) (ha' : a < n) :
(↑a).valMinAbs = ↑a - ↑n
source
@[simp]
theorem ZMod.valMinAbs_natCast_eq_self {n a : ℕ} [NeZero n] :
(↑a).valMinAbs = ↑a ↔ a ≤ n / 2
source
theorem ZMod.natAbs_valMinAbs_add_le {n : ℕ} (a b : ZMod n) :
(a + b).valMinAbs.natAbs ≤ (a.valMinAbs + b.valMinAbs).natAbs