proposition: Lemma Mk_root_Mk (R : comRingType) (h : {poly R}) k s (M : {set 'Z_k}) (p q : {poly R}) n : Mk_spec R s M -> h \is monic -> 1 < size h -> 0 < k -> rdvdp h ('X^k - 1) -> is_ipoly k s p -> is_ipoly k s q -> rmodp p h = rmodp q h -> n \in M -> rmodp ((p - q) \Po 'X^n) h = 0.
proof: Proof. move=> HM hM hS k_gt0 hDxk pI qI phEqh nIM; apply/eqP. case: HM nIM => // m nE mI _. have xkM := monic_Xn_sub_1 R k_gt0. have F : rmodp 'X^n ('X^k - 1) = rmodp 'X^m ('X^k - 1) :> {poly R}. have F1 : rmodp 'X^k ('X^k - 1) = 1 :> {poly R}. rewrite -{1}['X^k](subrK (1 : {poly R})) addrC rmodpD // rmodpp //. by rewrite addr0 rmodp_small // size_polyC oner_eq0 /= size_Xn_sub_1. rewrite (divn_eq m k) exprD mulnC exprM. rewrite mulrC -rmodp_mulmr // -[in RHS]rmodpX // F1 expr1n. by rewrite rmodp_mulmr // mulr1 nE. rewrite comp_polyB rmodpB // subr_eq0; apply/eqP. apply: etrans (_ : rmodp (p^+m) h = _). apply: rmodn_trans hDxk _ => //. rewrite -rmodp_compr // F rmodp_compr //. by apply/esym/eqP/pI. apply: etrans (_ : rmodp (q^+m) h = _). by rewrite -rmodpX // phEqh rmodpX. apply: esym. apply: rmodn_trans hDxk _ => //. rewrite -rmodp_compr // F rmodp_compr //. by apply/esym/eqP/qI. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound