fact: Definition primitive_root_of_unity n z := (n > 0) && [forall i : 'I_n, i.+1.-unity_root z == (i.+1 == n)].
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)