proposition: Lemma algCpfactorCE (x : algC) : x \isn't Num.real -> algCpfactor x = ('X - x%:P) * ('X - x^*%:P).
proof: Proof. move=> xNR; rewrite algRpfactorCE//=. rewrite rmorphD /= rmorphB/= !map_polyZ !map_polyXn/= map_polyX. rewrite (map_polyC algRval)/=. rewrite mulrBl !mulrBr -!addrA; congr (_ + _). rewrite opprD addrA opprK -opprD -rmorphM/= -normCK; congr (- _ + _). rewrite mulrC !mul_polyC -scalerDl. rewrite [x in RHS]algCrect conjC_rect ?Creal_Re ?Creal_Im//. by rewrite addrACA addNr addr0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various)