proposition: Lemma primitive_polyP (p : {poly F}) : reflect (let v := #|{poly %/ p}|.-1 in [/\ monic_irreducible_poly p, p %| 'X^v - 1 & forall n, 0 < n < v -> ~~ (p %| 'X^n - 1)]) (primitive_poly p).
proof: Proof. apply: (iffP and4P) => [[H1 H2 H3 /forallP H4] v|[[H1 H2] H3 H4]]; split => //. - by split => //; apply/irreducibleP. - move=> n /andP[n_gt0 nLv]; apply/negP => /(implyP (H4 (Ordinal nLv))) /=. by rewrite eqn0Ngt n_gt0. - by apply/irreducibleP. apply/forallP=> [] [[|n] Hn] /=; apply/implyP => pDX //. by case/negP: (H4 n.+1 Hn). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(div bigop binomial finset finfun ssralg countalg finalg) mathcomp(poly polydiv qpoly perm fingroup falgebra fieldext finfield galois) mathcomp(finalg zmodp matrix vector)