English
For [NeZero n], x ∈ ZMod n and y ∈ ℤ, x.valMinAbs = y holds exactly when x = y.cast and y satisfies -n < 2y ≤ n.
Русский
Для [NeZero n], x ∈ ZMod n и y ∈ ℤ: x.valMinAbs = y эквивалентно x = y.cast и y удовлетворяет -n < 2y ≤ n.
LaTeX
$$$x.valMinAbs = y \\iff (x = y.cast) \\land (y \\cdot 2 \\in (-n, n])$$$
Lean4
theorem valMinAbs_spec [NeZero n] (x : ZMod n) (y : ℤ) : x.valMinAbs = y ↔ x = y ∧ y * 2 ∈ Set.Ioc (-n : ℤ) n
where
mp := by rintro rfl; exact ⟨x.coe_valMinAbs.symm, x.valMinAbs_mem_Ioc⟩
mpr
h := by
rw [← sub_eq_zero]
apply @Int.eq_zero_of_abs_lt_dvd n
· rw [← intCast_zmod_eq_zero_iff_dvd, Int.cast_sub, coe_valMinAbs, h.1, sub_self]
rw [← mul_lt_mul_iff_left₀ (@zero_lt_two ℤ _ _ _ _ _)]
nth_rw 1 [← abs_eq_self.2 (@zero_le_two ℤ _ _ _ _)]
rw [← abs_mul, sub_mul, abs_lt]
constructor <;> linarith only [x.valMinAbs_mem_Ioc.1, x.valMinAbs_mem_Ioc.2, h.2.1, h.2.2]
