proposition: Lemma minCpoly_cyclotomic n z : n.-primitive_root z -> minCpoly z = cyclotomic z n.
proof: Proof. move=> prim_z; have n_gt0 := prim_order_gt0 prim_z. have Dpz := Cintr_Cyclotomic prim_z; set pz := cyclotomic z n in Dpz *. have mon_pz: pz \is monic by apply: cyclotomic_monic. have pz0: root pz z by rewrite root_cyclotomic. have [pf [Dpf mon_pf] dv_pf] := minCpolyP z. have /dvdpP_rat_int[f [af nz_af Df] [g /esym Dfg]]: pf %| pZtoQ 'Phi_n. rewrite -dv_pf; congr (root _ z): pz0; rewrite -Dpz -map_poly_comp. by apply: eq_map_poly => b; rewrite /= rmorph_int. without loss{nz_af} [mon_f mon_g]: af f g Df Dfg / f \is monic /\ g \is monic. move=> IH; pose cf := lead_coef f; pose cg := lead_coef g. have cfg1: cf * cg = 1. by rewrite -lead_coefM Dfg (monicP (Cyclotomic_monic n)). apply: (IH (af *~ cf) (f *~ cg) (g *~ cf)). - by rewrite rmorphMz -scalerMzr scalerMzl -mulrzA cfg1. - by rewrite mulrzAl mulrzAr -mulrzA cfg1. by rewrite !(intz, =^~ scaler_int) !monicE !lead_coefZ mulrC cfg1. have{af} Df: pQtoC pf = pZtoC f. have:= congr1 lead_coef Df. rewrite lead_coefZ lead_coef_map_inj //; last exact: intr_inj. rewrite !(monicP _) // mulr1 Df => <-; rewrite scale1r -map_poly_comp. by apply: eq_map_poly => b; rewrite /= rmorph_int. have [/size1_polyC Dg | g_gt1] := leqP (size g) 1. rewrite monicE Dg lead_coefC in mon_g. by rewrite -Dpz -Dfg Dg (eqP mon_g) mulr1 Dpf. have [zk gzk0]: exists zk, root (pZtoC g) zk. have [rg] := closed_field_poly_normal (pZtoC g). rewrite lead_coef_map_inj // (monicP mon_g) scale1r => Dg. rewrite -(size_map_inj_poly (can_inj intCK)) // Dg in g_gt1. rewrite size_prod_XsubC in g_gt1. by exists rg`_0; rewrite Dg root_prod_XsubC mem_nth. have [k cokn Dzk]: exists2 k, coprime k n & zk = z ^+ k. have: root pz zk by rewrite -Dpz -Dfg rmorphM rootM gzk0 orbT. rewrite -[pz](big_image _ _ _ _ (fun r => 'X - r%:P)) root_prod_XsubC. by case/imageP=> k; exists k. have co_fg (R : idomainType): n%:R != 0 :> R -> @coprimep R (intrp f) (intrp g). move=> nz_n; have: separable_poly (intrp ('X^n - 1) : {poly R}). by rewrite rmorphB rmorph1 /= map_polyXn separable_Xn_sub_1. rewrite -prod_Cyclotomic // (big_rem n) -?dvdn_divisors //= -Dfg. by rewrite !rmorphM /= !separable_mul => /and3P[] /and3P[]. suffices fzk0: root (pZtoC f) zk. have [] // := negP (coprimep_root (co_fg _ _) fzk0). by rewrite pnatr_eq0 -lt0n. move: gzk0 cokn; rewrite {zk}Dzk; elim/ltn_ind: k => k IHk gzk0 cokn. have [|k_gt1] := leqP k 1; last have [p p_pr /dvdnP[k1 Dk]] := pdivP k_gt1. rewrite -[leq k 1](mem_iota 0 2) !inE => /pred2P[k0 | ->]; last first. by rewrite -Df dv_pf. have /eqP := size_Cyclotomic n; rewrite -Dfg size_Mmonic ?monic_neq0 //. rewrite k0 /coprime gcd0n in cokn; rewrite (eqP cokn). rewrite -(size_map_inj_poly (can_inj intCK)) // -Df -Dpf. by rewrite -(subnKC g_gt1) -(subnKC (size_minCpoly z)) !addnS. move: cokn; rewrite Dk coprimeMl => /andP[cok1n]. rewrite prime_coprime // (dvdn_charf (char_Fp p_pr)) => /co_fg {co_fg}. have charFpX: p \in [char {poly 'F_p}] by rewrite (rmorph_char polyC) ?char_Fp. rewrite -(coprimep_pexpr _ _ (prime_gt0 p_pr)) -(Frobenius_autE charFpX). rewrite -[g]comp_polyXr map_comp_poly -horner_map /= Frobenius_autE -rmorphXn. rewrite -!map_poly_comp (@eq_map_poly _ _ _ (polyC \o *~%R 1)); last first. by move=> a; rewrite /= !rmorph_int. rewrite map_poly_comp -[_.[_]]map_comp_poly /= => co_fg. suffices: coprimep (pZtoC f) (pZtoC (g \Po 'X^p)). move/coprimep_root=> /=/(_ (z ^+ k1))/implyP. rewrite map_comp_poly map_polyXn horner_comp hornerXn. rewrite -exprM -Dk [_ == 0]gzk0 implybF => /negP[]. have: root pz (z ^+ k1). by rewrite root_cyclotomic // prim_root_exp_coprime. rewrite -Dpz -Dfg rmorphM rootM => /orP[] //= /IHk-> //. rewrite -[k1]muln1 Dk ltn_pmul2l ?prime_gt1 //. by have:= ltnW k_gt1; rewrite Dk muln_gt0 => /andP[]. suffices: coprimep f (g \Po 'X^p). case/Bezout_coprimepP=> [[u v]]; rewrite -size_poly_eq1. rewrite -(size_map_inj_poly (can_inj intCK)) // rmorphD !rmorphM /=. rewrite size_poly_eq1 => {}co_fg; apply/Bezout_coprimepP. by exists (pZtoC u, pZtoC v). apply: contraLR co_fg => /coprimepPn[|d]; first exact: monic_neq0. rewrite andbC -size_poly_eq1 dvdp_gcd => /and3P[sz_d]. pose d1 := zprimitive d. have d_dv_mon h: d %| h -> h \is monic -> exists h1, h = d1 * h1. case/Pdiv.Idomain.dvdpP=> [[c h1] /= nz_c Dh] mon_h; exists (zprimitive h1). by rewrite -zprimitiveM mulrC -Dh zprimitiveZ ?zprimitive_monic. case/d_dv_mon=> // f1 Df1 /d_dv_mon[|f2 ->]. rewrite monicE lead_coefE size_comp_poly size_polyXn /=. rewrite comp_polyE coef_sum polySpred ?monic_neq0 //= mulnC. rewrite big_ord_recr /= -lead_coefE (monicP mon_g) scale1r. rewrite -exprM coefXn eqxx big1 ?add0r // => i _. rewrite coefZ -exprM coefXn eqn_pmul2l ?prime_gt0 //. by rewrite eqn_leq leqNgt ltn_ord mulr0. have monFp h: h \is monic -> size (map_poly intr h) = size h. by move=> mon_h; rewrite size_poly_eq // -lead_coefE (monicP mon_h) oner_eq0. apply/coprimepPn; last exists (map_poly intr d1). by rewrite -size_poly_eq0 monFp // size_poly_eq0 monic_neq0. rewrite Df1 !rmorphM dvdp_gcd !dvdp_mulr //= -size_poly_eq1. rewrite monFp ?size_zprimitive //. rewrite monicE [_ d1]intEsg sgz_lead_primitive -zprimitive_eq0 -/d1. rewrite -lead_coef_eq0 -absz_eq0. have/esym/eqP := congr1 (absz \o lead_coef) Df1. by rewrite /= (monicP mon_f) lead_coefM abszM muln_eq1 => /andP[/eqP-> _]. 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)