proposition: Lemma introspec_fin_div (F : finFieldType) k n p (c : nat) : coprime k n -> p \in [char F] -> (p %| n)%N -> n ⋈[k] ('X + c%:R%:P : {poly F}) -> (n %/ p) ⋈[k] ('X + c%:R%:P : {poly F}).
proof: Proof. move=> kCn pC pDn nIkX. have pP : prime p by case/andP: pC. have k_gt0 : 0 < k. case: k {nIkX}kCn pDn pP => //. rewrite /coprime gcd0n => /eqP->. by rewrite dvdn1 => /eqP->. rewrite /introspective -!Pdiv.IdomainMonic.modpE ?monic_Xn_sub_1 //. have kNZ : k%:R != 0 :> F. rewrite -(dvdn_charf pC); apply/negP => pDk. move: pP. have : (p %| 1)%N by rewrite -(eqP kCn) dvdn_gcd pDk. by rewrite dvdn1 => /eqP->. have pCF : [char {poly F}].-nat p. rewrite /pnat prime_gt0 //=; apply/allP => q. rewrite primes_prime //= inE => /eqP->. rewrite inE pP -polyC_natr polyC_eq0 /=. by case/andP : pC. rewrite -subr_eq0 -modpN -modpD -[_ == 0]/(_ %| _). rewrite -(separable_exp _ (separable_polyXnsub1 _) (prime_gt0 pP)) //. rewrite exprDn_char // exprNn_char // -exprM divnK //. rewrite comp_polyD comp_polyC [_ ^+ p]exprDn_char //. rewrite comp_poly_exp comp_Xn_poly -exprM divnK //. rewrite -polyC_exp fin_little_fermat //. rewrite /dvdp modpD modpN subr_eq0 //. move: nIkX. rewrite /introspective -!Pdiv.IdomainMonic.modpE ?monic_Xn_sub_1 //. by rewrite comp_polyD comp_polyC comp_polyX. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound