proposition: Lemma div_ring_mul_group_cyclic (R : unitRingType) (f : gT -> R) : f 1 = 1%R -> {in G &, {morph f : u v / u * v >-> (u * v)%R}} -> {in G^#, forall x, f x - 1 \in GRing.unit}%R -> abelian G -> cyclic G.
proof: Proof. move=> f1 fM f1P abelG. have fX n: {in G, {morph f : u / u ^+ n >-> (u ^+ n)%R}}. by case: n => // n x Gx; elim: n => //= n IHn; rewrite expgS fM ?groupX ?IHn. have fU x: x \in G -> f x \in GRing.unit. by move=> Gx; apply/unitrP; exists (f x^-1); rewrite -!fM ?groupV ?gsimp. apply: order_inj_cyclic => x y Gx Gy; set n := #[x] => yn. apply/eqP; rewrite eq_sym eqEcard -[#|_|]/n yn leqnn andbT cycle_subG /=. suff{y Gy yn} ->: <[x]> = G :&: [set z | #[z] %| n] by rewrite !inE Gy yn /=. apply/eqP; rewrite eqEcard subsetI cycle_subG {}Gx /= cardE; set rs := enum _. apply/andP; split; first by apply/subsetP=> y xy; rewrite inE order_dvdG. pose P : {poly R} := ('X^n - 1)%R; have n_gt0: n > 0 by apply: order_gt0. have szP: size P = n.+1 by rewrite size_addl size_polyXn ?size_opp ?size_poly1. rewrite -ltnS -szP -(size_map f) max_ring_poly_roots -?size_poly_eq0 ?{}szP //. apply/allP=> fy /mapP[y]; rewrite mem_enum !inE order_dvdn => /andP[Gy]. move/eqP=> yn1 ->{fy}; apply/eqP. by rewrite !(hornerE, hornerXn) -fX // yn1 f1 subrr. have: uniq rs by apply: enum_uniq. have: all [in G] rs by apply/allP=> y; rewrite mem_enum; case/setIP. elim: rs => //= y rs IHrs /andP[Gy Grs] /andP[y_rs]; rewrite andbC. move/IHrs=> -> {IHrs}//; apply/allP=> _ /mapP[z rs_z ->]. have{Grs} Gz := allP Grs z rs_z; rewrite /diff_roots -!fM // (centsP abelG) //. rewrite eqxx -[f y]mul1r -(mulgKV y z) fM ?groupM ?groupV //=. rewrite -mulNr -mulrDl unitrMl ?fU ?f1P // !inE. by rewrite groupM ?groupV // andbT -eq_mulgV1; apply: contra y_rs; move/eqP <-. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice div) mathcomp(fintype bigop prime finset fingroup morphism) mathcomp(perm automorphism quotient gproduct ssralg) mathcomp(finalg zmodp poly)