proposition: Lemma prod_cyclotomic : 'X^n - 1 = \prod_(d <- divisors n) cyclotomic (z ^+ (n %/ d)) d.
proof: Proof. have in_d d: (d %| n)%N -> val (@inord n d) = d by move/dvdn_leq/inordK=> /= ->. have dv_n k: (n %/ gcdn k n %| n)%N. by rewrite -{3}(divnK (dvdn_gcdr k n)) dvdn_mulr. have [uDn _ inDn] := divisors_correct n_gt0. have defDn: divisors n = map val (map (@inord n) (divisors n)). by rewrite -map_comp map_id_in // => d; rewrite inDn => /in_d. rewrite defDn big_map big_uniq /=; last first. by rewrite -(map_inj_uniq val_inj) -defDn. pose h (k : 'I_n) : 'I_n.+1 := inord (n %/ gcdn k n). rewrite -(factor_Xn_sub_1 prim_z) big_mkord. rewrite (partition_big h (dvdn^~ n)) /= => [|k _]; last by rewrite in_d ?dv_n. apply: eq_big => d; first by rewrite -(mem_map val_inj) -defDn inDn. set q := (n %/ d)%N => d_dv_n. have [q_gt0 d_gt0]: (0 < q /\ 0 < d)%N by apply/andP; rewrite -muln_gt0 divnK. have fP (k : 'I_d): (q * k < n)%N by rewrite divn_mulAC ?ltn_divLR ?ltn_pmul2l. rewrite (reindex (fun k => Ordinal (fP k))); last first. have f'P (k : 'I_n): (k %/ q < d)%N by rewrite ltn_divLR // mulnC divnK. exists (fun k => Ordinal (f'P k)) => [k _ | k /eqnP/=]. by apply: val_inj; rewrite /= mulKn. rewrite in_d // => Dd; apply: val_inj; rewrite /= mulnC divnK // /q -Dd. by rewrite divnA ?mulKn ?dvdn_gcdl ?dvdn_gcdr. apply: eq_big => k; rewrite ?exprM // -val_eqE in_d //=. rewrite -eqn_mul ?dvdn_gcdr ?gcdn_gt0 ?n_gt0 ?orbT //. rewrite -[n in gcdn _ n](divnK d_dv_n) -muln_gcdr mulnCA mulnA divnK //. by rewrite mulnC eqn_mul // divnn n_gt0 eq_sym. 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)