proposition: Lemma introspecMl (R : comRingType) (k m n : nat) (p : {poly R}) : m ⋈[k] p -> n ⋈[k] p -> m * n ⋈[k] p.
proof: Proof. case: m => // m. have XmD1 : 'X^m.+1 != 1 :> {poly R}. apply/eqP => /(congr1 (size : {poly R} -> _)). by rewrite size_polyXn size_polyC oner_eq0. case: k => [|k mIp nIp]. rewrite /introspective !subrr !rmodp0 exprM => /eqP->. rewrite comp_poly_exp => /eqP->. by rewrite -comp_polyA comp_Xn_poly -exprM. have XM : ('X^k.+1 - 1 : {poly R}) \is monic. rewrite qualifE /= lead_coefDl ?lead_coefXn ?unitr1 //. by rewrite size_polyXn size_opp size_polyC oner_neq0. rewrite /introspective exprM -rmodpX // (eqP mIp) rmodpX //. rewrite exprM -['X^m.+1 ^+_]comp_Xn_poly comp_poly_exp comp_polyA. rewrite -subr_eq0 -rmodpB // -comp_polyB. apply: rdvdp_trans (_ : rdvdp (('X^k.+1 -1) \Po 'X^m.+1) _) => //. - by apply: monic_comp_poly => //; rewrite qualifE /= lead_coefXn. - rewrite comp_polyB comp_Xn_poly comp_polyC -exprM mulnC exprM. by apply: dvdp_geom. apply: rdvdp_comp_poly => //; first by rewrite qualifE /= lead_coefXn. by rewrite /rdvdp rmodpB // subr_eq0. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly) more_thm rootn lcm_lbound