proposition: Lemma field_mul_group_cyclic (F : fieldType) (f : gT -> F) : {in G &, {morph f : u v / u * v >-> (u * v)%R}} -> {in G, forall x, f x = 1%R <-> x = 1} -> cyclic G.
proof: Proof. move=> fM f1P; have f1 : f 1 = 1%R by apply/f1P. apply: (div_ring_mul_group_cyclic f1 fM) => [x|]. case/setD1P=> x1 Gx; rewrite unitfE; apply: contra x1. by rewrite subr_eq0 => /eqP/f1P->. apply/centsP=> x Gx y Gy; apply/commgP/eqP. apply/f1P; rewrite ?fM ?groupM ?groupV //. by rewrite mulrCA -!fM ?groupM ?groupV // mulKg mulVg. 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)