proposition: Lemma fmorph_unity_root n z : n.-unity_root (f z) = n.-unity_root z.
proof: Proof. by rewrite !unity_rootE -(inj_eq (fmorph_inj f)) rmorphXn ?rmorph1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)