proposition: Lemma primitive_root_pow (F : fieldType) (m : nat) (w w' : F) : m.-primitive_root w' -> m.-primitive_root w -> exists2 k, coprime k m & w = w' ^+ k.
proof: Proof. move/root_cyclotomic<-. rewrite /cyclotomic -big_filter; have [t et [uniqs tP /= perms]] := big_enumP. pose rs := [seq w' ^+ (val i) | i <- t]; set p := (X in root X). have {p} -> : p = \prod_(w <- rs) ('X - w%:P) by rewrite /p big_map. rewrite root_prod_XsubC; case/mapP=> [[i ltim]]; rewrite tP /= => coprim ew. by exists i. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(char0 various)