proposition: Lemma homocyclic_Ohm_Mho n p G : p.-group G -> homocyclic G -> 'Ohm_n(G) = 'Mho^(logn p (exponent G) - n)(G).
proof: Proof. move=> pG /andP[cGG homoG]; set e := exponent G. have{pG} p_e: p.-nat e by apply: pnat_dvd pG; apply: exponent_dvdn. have{homoG}: all (pred1 e) (abelian_type G). move: homoG; rewrite /abelian_type -(prednK (cardG_gt0 G)) /=. by case: (_ && _) (tag _); rewrite //= genGid eqxx. have{cGG} [b defG <-] := abelian_structure cGG. move: e => e in p_e *; elim: b => /= [|x b IHb] in G defG *. by rewrite -defG big_nil (trivgP (Ohm_sub _ _)) (trivgP (Mho_sub _ _)). case/andP=> /eqP ox e_b; rewrite big_cons in defG. rewrite -(Ohm_dprod _ defG) -(Mho_dprod _ defG). case/dprodP: defG => [[_ H _ defH] _ _ _]; rewrite defH IHb //; congr (_ \x _). by rewrite -ox in p_e *; rewrite (Ohm_p_cycle _ p_e) (Mho_p_cycle _ p_e). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism action) mathcomp(quotient gfunctor gproduct ssralg countalg finalg zmodp) mathcomp(cyclic pgroup gseries nilpotent sylow)