proposition: Lemma minPoly_rp x : x \in rp -> minPoly 1%VS x %= map_poly ratr p.
proof: Proof. move=> xrp; have : minPoly 1 x %| map_poly ratr p. by rewrite minPoly_dvdp ?ratr_p_over ?[root _ _]root_p//=. have : size (minPoly 1 x) != 1%N by rewrite size_minPoly. have /polyOver1P[q ->] := minPolyOver 1 x. have /eq_map_poly -> : in_alg L =1 ratr. by move=> r; rewrite in_algE alg_num_field. rewrite -char0_ratrE /eqp. rewrite 2!(dvdp_map (char0_ratr charL)). by rewrite -/(_ %= _) size_map_poly; apply: p_irr. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field polyrcf) Abel(various classic_ext map_gal algR) Abel(char0 cyclotomic_ext real_closed_ext)