Documentation

Mathlib.Data.ZMod.ValMinAbs

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
    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
      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
      @[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.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