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

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

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

@[simp]

theorem ZMod.valMinAbs_inj {n : ℕ} {a b : ZMod n} :

a.valMinAbs = b.valMinAbs ↔ a = b

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

theorem ZMod.eq_neg_of_valMinAbs_eq_neg_valMinAbs {n : ℕ} {a b : ZMod n} (h : a.valMinAbs = -b.valMinAbs) :

a = -b

@[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.natAbs_valMinAbs_eq_natAbs_valMinAbs {n : ℕ} {a b : ZMod n} :

a.valMinAbs.natAbs = b.valMinAbs.natAbs ↔ a = b ∨ a = -b

theorem ZMod.abs_valMinAbs_eq_abs_valMinAbs {n : ℕ} {a b : ZMod n} :

|a.valMinAbs| = |b.valMinAbs| ↔ a = b ∨ a = -b

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