proposition: Lemma Cintr_Cyclotomic n z : n.-primitive_root z -> pZtoC 'Phi_n = cyclotomic z n.
proof: Proof. elim/ltn_ind: n z => n IHn z0 prim_z0. rewrite /'Phi_n; case: (C_prim_root_exists _) => z /=. have n_gt0 := prim_order_gt0 prim_z0; rewrite prednK // => prim_z. have [uDn _ inDn] := divisors_correct n_gt0. pose q := \prod_(d <- rem n (divisors n)) 'Phi_d. have mon_q: q \is monic by apply: monic_prod => d _; apply: Cyclotomic_monic. have defXn1: cyclotomic z n * pZtoC q = 'X^n - 1. rewrite (prod_cyclotomic prim_z) (big_rem n) ?inDn //=. rewrite divnn n_gt0 rmorph_prod /=; congr (_ * _). apply: eq_big_seq => d; rewrite mem_rem_uniq ?inE //= inDn => /andP[n'd ddvn]. by rewrite -IHn ?dvdn_prim_root // ltn_neqAle n'd dvdn_leq. have mapXn1 (R1 R2 : ringType) (f : {rmorphism R1 -> R2}): map_poly f ('X^n - 1) = 'X^n - 1. - by rewrite rmorphB /= rmorph1 map_polyXn. have nz_q: pZtoC q != 0. by rewrite -size_poly_eq0 size_map_inj_poly // size_poly_eq0 monic_neq0. have [r def_zn]: exists r, cyclotomic z n = pZtoC r. have defZtoC: ZtoC =1 QtoC \o ZtoQ by move=> a; rewrite /= rmorph_int. have /dvdpP[r0 Dr0]: map_poly ZtoQ q %| 'X^n - 1. rewrite -(dvdp_map (@ratr algC)) mapXn1 -map_poly_comp. by rewrite -(eq_map_poly defZtoC) -defXn1 dvdp_mull. have [r [a nz_a Dr]] := rat_poly_scale r0. exists (zprimitive r); apply: (mulIf nz_q); rewrite defXn1. rewrite -rmorphM -(zprimitive_monic mon_q) -zprimitiveM /=. have ->: r * q = a *: ('X^n - 1). apply: (map_inj_poly (intr_inj : injective ZtoQ)) => //. rewrite map_polyZ mapXn1 Dr0 Dr -scalerAl scalerKV ?intr_eq0 //. by rewrite rmorphM. by rewrite zprimitiveZ // zprimitive_monic ?monic_Xn_sub_1 ?mapXn1. rewrite floorpK; last by apply/polyOverP=> i; rewrite def_zn coef_map /=. pose f e (k : 'I_n) := Ordinal (ltn_pmod (k * e) n_gt0). have [e Dz0] := prim_rootP prim_z (prim_expr_order prim_z0). have co_e_n: coprime e n by rewrite -(prim_root_exp_coprime e prim_z) -Dz0. have injf: injective (f e). apply: can_inj (f (egcdn e n).1) _ => k; apply: val_inj => /=. rewrite modnMml -mulnA -modnMmr -{1}(mul1n e). by rewrite (chinese_modr co_e_n 0) modnMmr muln1 modn_small. rewrite [_ n](reindex_inj injf); apply: eq_big => k /=. by rewrite coprime_modl coprimeMl co_e_n andbT. by rewrite prim_expr_mod // mulnC exprM -Dz0. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly finset fingroup finalg zmodp cyclic) mathcomp(ssrnum ssrint archimedean polydiv intdiv mxpoly) mathcomp(rat vector falgebra fieldext separable galois algC)