Residues of integers and words, and squares in ZMod n

Candidates for Mathlib.Data.ZMod.Basic: the cast to ZMod n of the least non-negative residue of an integer (ZMod.natCast_toNat_emod, which is ZMod.natCast_toNat without its hypothesis 0 ≤ z), the cast to ZMod n of the word s x + a for n ∣ 2 ^ 64, as the arithmetic of words is that modulo 2 ^ 64 (UInt64.natCast_toNat_mul_add), and a residue that is a square in ZMod n as the residue of the square of a natural number below n (ZMod.exists_eq_mul_self_mod_of_isSquare), and for odd n and a residue other than 0 as that of the square of a number from 1 to n / 2 (ZMod.isSquare_natCast_iff_exists_mul_self_mod_eq).

theorem ZMod.natCast_toNat_emod {n : ℕ} [NeZero n] (a : ℤ) : ↑(a % ↑n).toNat = ↑a

The cast to ZMod n of the least non-negative residue of a modulo n is the cast of a; ZMod.natCast_toNat without its hypothesis 0 ≤ z.

theorem ZMod.exists_eq_mul_self_mod_of_isSquare {n v : ℕ} (hv : v < n) (h : IsSquare ↑v) : ∃ s < n, v = s * s % n

A residue v < n that is a square in ZMod n is the residue of the square of a natural number below n.

theorem ZMod.isSquare_natCast_iff_exists_mul_self_mod_eq {n v : ℕ} (hn : n % 2 = 1) (hv0 : v ≠ 0) (hv : v < n) : IsSquare ↑v ↔ ∃ (x : ℕ), 1 ≤ x ∧ x ≤ n / 2 ∧ x * x % n = v

Modulo an odd n, a residue 0 < v < n is a square exactly when it is the square of one of 1, …, n / 2, since x and n - x have the same square.

theorem UInt64.natCast_toNat_mul_add {n : ℕ} (hn : n ∣ 2 ^ 64) (s x a : UInt64) : ↑(s * x + a).toNat = ↑s.toNat * ↑x.toNat + ↑a.toNat

The cast to ZMod n of the word s x + a is s x + a computed in ZMod n, for n ∣ 2 ^ 64, since the arithmetic of words is that modulo 2 ^ 64.