Torsion group of ZMod p for prime p

This file shows that the ZMod p has p - 1 roots-of-unity.

theorem ZMod.rootsOfUnity_eq_top {p : ℕ} [Fact (Nat.Prime p)] : rootsOfUnity (p - 1) (ZMod p) = ⊤

instance ZMod.instHasEnoughRootsOfUnityHSubNatOfNat {p : ℕ} [Fact (Nat.Prime p)] : HasEnoughRootsOfUnity (ZMod p) (p - 1)