Library mathcomp.solvable.frobenius
+ +
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+
++ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+ Definition of Frobenius groups, some basic results, and the Frobenius
+ theorem on the number of solutions of x ^+ n = 1.
+ semiregular K H <->
+ the internal action of H on K is semiregular, i.e., no nontrivial
+ elements of H and K commute; note that this is actually a symmetric
+ condition.
+ semiprime K H <->
+ the internal action of H on K is "prime", i.e., an element of K that
+ centralises a nontrivial element of H must centralise all of H.
+ normedTI A G L <=>
+ A is nonempty, strictly disjoint from its conjugates in G, and has
+ normaliser L in G.
+ [Frobenius G = K ><| H] <=>
+ G is (isomorphic to) a Frobenius group with kernel K and complement
+ H. This is an effective predicate (in bool), which tests the
+ equality with the semidirect product, and then the fact that H is a
+ proper self-normalizing TI-subgroup of G.
+ [Frobenius G with kernel H] <=>
+ G is (isomorphic to) a Frobenius group with kernel K; same as above,
+ but without the semi-direct product.
+ [Frobenius G with complement H] <=>
+ G is (isomorphic to) a Frobenius group with complement H; same as
+ above, but without the semi-direct product. The proof that this form
+ is equivalent to the above (i.e., the existence of Frobenius
+ kernels) requires character theory and will only be proved in the
+ vcharacter.v file.
+ [Frobenius G] <=> G is a Frobenius group.
+ Frobenius_action G H S to <->
+ The action to of G on S defines an isomorphism of G with a
+ (permutation) Frobenius group, i.e., to is faithful and transitive
+ on S, no nontrivial element of G fixes more than one point in S, and
+ H is the stabilizer of some element of S, and non-trivial. Thus,
+ Frobenius_action G H S 'P
+ asserts that G is a Frobenius group in the classic sense.
+ has_Frobenius_action G H <->
+ Frobenius_action G H S to holds for some sT : finType, S : {set st}
+ and to : {action gT &-> sT}. This is a predicate in Prop, but is
+ exactly reflected by [Frobenius G with complement H] : bool.
+
+
+
+
+Set Implicit Arguments.
+ +
+Import GroupScope.
+ +
+Section Definitions.
+ +
+Variable gT : finGroupType.
+Implicit Types A G K H L : {set gT}.
+ +
+
+
++Set Implicit Arguments.
+ +
+Import GroupScope.
+ +
+Section Definitions.
+ +
+Variable gT : finGroupType.
+Implicit Types A G K H L : {set gT}.
+ +
+
+ Corresponds to "H acts on K in a regular manner" in B & G.
+
+
+
+
+ Corresponds to "H acts on K in a prime manner" in B & G.
+
+
+Definition semiprime K H := {in H^#, ∀ x, 'C_K[x] = 'C_K(H)}.
+ +
+Definition normedTI A G L := [&& A != set0, trivIset (A :^: G) & 'N_G(A) == L].
+ +
+Definition Frobenius_group_with_complement G H := (H != G) && normedTI H^# G H.
+ +
+Definition Frobenius_group G :=
+ [∃ H : {group gT}, Frobenius_group_with_complement G H].
+ +
+Definition Frobenius_group_with_kernel_and_complement G K H :=
+ (K ><| H == G) && Frobenius_group_with_complement G H.
+ +
+Definition Frobenius_group_with_kernel G K :=
+ [∃ H : {group gT}, Frobenius_group_with_kernel_and_complement G K H].
+ +
+Section FrobeniusAction.
+ +
+Variables G H : {set gT}.
+Variables (sT : finType) (S : {set sT}) (to : {action gT &-> sT}).
+ +
+Definition Frobenius_action :=
+ [/\ [faithful G, on S | to],
+ [transitive G, on S | to],
+ {in G^#, ∀ x, #|'Fix_(S | to)[x]| ≤ 1},
+ H != 1
+ & exists2 u, u \in S & H = 'C_G[u | to]].
+ +
+End FrobeniusAction.
+ +
+CoInductive has_Frobenius_action G H : Prop :=
+ HasFrobeniusAction sT S to of @Frobenius_action G H sT S to.
+ +
+End Definitions.
+ +
+ +
+Notation "[ 'Frobenius' G 'with' 'complement' H ]" :=
+ (Frobenius_group_with_complement G H)
+ (at level 0, G at level 50, H at level 35,
+ format "[ 'Frobenius' G 'with' 'complement' H ]") : group_scope.
+ +
+Notation "[ 'Frobenius' G 'with' 'kernel' K ]" :=
+ (Frobenius_group_with_kernel G K)
+ (at level 0, G at level 50, K at level 35,
+ format "[ 'Frobenius' G 'with' 'kernel' K ]") : group_scope.
+ +
+Notation "[ 'Frobenius' G ]" :=
+ (Frobenius_group G)
+ (at level 0, G at level 50,
+ format "[ 'Frobenius' G ]") : group_scope.
+ +
+Notation "[ 'Frobenius' G = K ><| H ]" :=
+ (Frobenius_group_with_kernel_and_complement G K H)
+ (at level 0, G at level 50, K, H at level 35,
+ format "[ 'Frobenius' G = K ><| H ]") : group_scope.
+ +
+Section FrobeniusBasics.
+ +
+Variable gT : finGroupType.
+Implicit Types (A B : {set gT}) (G H K L R X : {group gT}).
+ +
+Lemma semiregular1l H : semiregular 1 H.
+ +
+Lemma semiregular1r K : semiregular K 1.
+ +
+Lemma semiregular_sym H K : semiregular K H → semiregular H K.
+ +
+Lemma semiregularS K1 K2 A1 A2 :
+ K1 \subset K2 → A1 \subset A2 → semiregular K2 A2 → semiregular K1 A1.
+ +
+Lemma semiregular_prime H K : semiregular K H → semiprime K H.
+ +
+Lemma semiprime_regular H K : semiprime K H → 'C_K(H) = 1 → semiregular K H.
+ +
+Lemma semiprimeS K1 K2 A1 A2 :
+ K1 \subset K2 → A1 \subset A2 → semiprime K2 A2 → semiprime K1 A1.
+ +
+Lemma cent_semiprime H K X :
+ semiprime K H → X \subset H → X :!=: 1 → 'C_K(X) = 'C_K(H).
+ +
+Lemma stab_semiprime H K X :
+ semiprime K H → X \subset K → 'C_H(X) != 1 → 'C_H(X) = H.
+ +
+Lemma cent_semiregular H K X :
+ semiregular K H → X \subset H → X :!=: 1 → 'C_K(X) = 1.
+ +
+Lemma regular_norm_dvd_pred K H :
+ H \subset 'N(K) → semiregular K H → #|H| %| #|K|.-1.
+ +
+Lemma regular_norm_coprime K H :
+ H \subset 'N(K) → semiregular K H → coprime #|K| #|H|.
+ +
+Lemma semiregularJ K H x : semiregular K H → semiregular (K :^ x) (H :^ x).
+ +
+Lemma semiprimeJ K H x : semiprime K H → semiprime (K :^ x) (H :^ x).
+ +
+Lemma normedTI_P A G L :
+ reflect [/\ A != set0, L \subset 'N_G(A)
+ & {in G, ∀ g, ~~ [disjoint A & A :^ g] → g \in L}]
+ (normedTI A G L).
+ +
+Lemma normedTI_memJ_P A G L :
+ reflect [/\ A != set0, L \subset G
+ & {in A & G, ∀ a g, (a ^ g \in A) = (g \in L)}]
+ (normedTI A G L).
+ +
+Lemma partition_class_support A G :
+ A != set0 → trivIset (A :^: G) → partition (A :^: G) (class_support A G).
+ +
+Lemma partition_normedTI A G L :
+ normedTI A G L → partition (A :^: G) (class_support A G).
+ +
+Lemma card_support_normedTI A G L :
+ normedTI A G L → #|class_support A G| = (#|A| × #|G : L|)%N.
+ +
+Lemma normedTI_S A B G L :
+ A != set0 → L \subset 'N(A) → A \subset B → normedTI B G L →
+ normedTI A G L.
+ +
+Lemma cent1_normedTI A G L :
+ normedTI A G L → {in A, ∀ x, 'C_G[x] \subset L}.
+ +
+Lemma Frobenius_actionP G H :
+ reflect (has_Frobenius_action G H) [Frobenius G with complement H].
+ +
+Section FrobeniusProperties.
+ +
+Variables G H K : {group gT}.
+Hypothesis frobG : [Frobenius G = K ><| H].
+ +
+Lemma FrobeniusWker : [Frobenius G with kernel K].
+ +
+Lemma FrobeniusWcompl : [Frobenius G with complement H].
+ +
+Lemma FrobeniusW : [Frobenius G].
+ +
+Lemma Frobenius_context :
+ [/\ K ><| H = G, K :!=: 1, H :!=: 1, K \proper G & H \proper G].
+ +
+Lemma Frobenius_partition : partition (gval K |: (H^# :^: K)) G.
+ +
+Lemma Frobenius_cent1_ker : {in K^#, ∀ x, 'C_G[x] \subset K}.
+ +
+Lemma Frobenius_reg_ker : semiregular K H.
+ +
+Lemma Frobenius_reg_compl : semiregular H K.
+ +
+Lemma Frobenius_dvd_ker1 : #|H| %| #|K|.-1.
+ +
+Lemma ltn_odd_Frobenius_ker : odd #|G| → #|H|.*2 < #|K|.
+ +
+Lemma Frobenius_index_dvd_ker1 : #|G : K| %| #|K|.-1.
+ +
+Lemma Frobenius_coprime : coprime #|K| #|H|.
+ +
+Lemma Frobenius_trivg_cent : 'C_K(H) = 1.
+ +
+Lemma Frobenius_index_coprime : coprime #|K| #|G : K|.
+ +
+Lemma Frobenius_ker_Hall : Hall G K.
+ +
+Lemma Frobenius_compl_Hall : Hall G H.
+ +
+End FrobeniusProperties.
+ +
+Lemma normedTI_J x A G L : normedTI (A :^ x) (G :^ x) (L :^ x) = normedTI A G L.
+ +
+Lemma FrobeniusJcompl x G H :
+ [Frobenius G :^ x with complement H :^ x] = [Frobenius G with complement H].
+ +
+Lemma FrobeniusJ x G K H :
+ [Frobenius G :^ x = K :^ x ><| H :^ x] = [Frobenius G = K ><| H].
+ +
+Lemma FrobeniusJker x G K :
+ [Frobenius G :^ x with kernel K :^ x] = [Frobenius G with kernel K].
+ +
+Lemma FrobeniusJgroup x G : [Frobenius G :^ x] = [Frobenius G].
+ +
+Lemma Frobenius_ker_dvd_ker1 G K :
+ [Frobenius G with kernel K] → #|G : K| %| #|K|.-1.
+ +
+Lemma Frobenius_ker_coprime G K :
+ [Frobenius G with kernel K] → coprime #|K| #|G : K|.
+ +
+Lemma Frobenius_semiregularP G K H :
+ K ><| H = G → K :!=: 1 → H :!=: 1 →
+ reflect (semiregular K H) [Frobenius G = K ><| H].
+ +
+Lemma prime_FrobeniusP G K H :
+ K :!=: 1 → prime #|H| →
+ reflect (K ><| H = G ∧ 'C_K(H) = 1) [Frobenius G = K ><| H].
+ +
+Lemma Frobenius_subl G K K1 H :
+ K1 :!=: 1 → K1 \subset K → H \subset 'N(K1) → [Frobenius G = K ><| H] →
+ [Frobenius K1 <*> H = K1 ><| H].
+ +
+Lemma Frobenius_subr G K H H1 :
+ H1 :!=: 1 → H1 \subset H → [Frobenius G = K ><| H] →
+ [Frobenius K <*> H1 = K ><| H1].
+ +
+Lemma Frobenius_kerP G K :
+ reflect [/\ K :!=: 1, K \proper G, K <| G
+ & {in K^#, ∀ x, 'C_G[x] \subset K}]
+ [Frobenius G with kernel K].
+ +
+Lemma set_Frobenius_compl G K H :
+ K ><| H = G → [Frobenius G with kernel K] → [Frobenius G = K ><| H].
+ +
+Lemma Frobenius_kerS G K G1 :
+ G1 \subset G → K \proper G1 →
+ [Frobenius G with kernel K] → [Frobenius G1 with kernel K].
+ +
+Lemma Frobenius_action_kernel_def G H K sT S to :
+ K ><| H = G → @Frobenius_action _ G H sT S to →
+ K :=: 1 :|: [set x in G | 'Fix_(S | to)[x] == set0].
+ +
+End FrobeniusBasics.
+ +
+ +
+Lemma Frobenius_coprime_quotient (gT : finGroupType) (G K H N : {group gT}) :
+ K ><| H = G → N <| G → coprime #|K| #|H| ∧ H :!=: 1%g →
+ N \proper K ∧ {in H^#, ∀ x, 'C_K[x] \subset N} →
+ [Frobenius G / N = (K / N) ><| (H / N)]%g.
+ +
+Section InjmFrobenius.
+ +
+Variables (gT rT : finGroupType) (D G : {group gT}) (f : {morphism D >-> rT}).
+Implicit Types (H K : {group gT}) (sGD : G \subset D) (injf : 'injm f).
+ +
+Lemma injm_Frobenius_compl H sGD injf :
+ [Frobenius G with complement H] → [Frobenius f @* G with complement f @* H].
+ +
+Lemma injm_Frobenius H K sGD injf :
+ [Frobenius G = K ><| H] → [Frobenius f @* G = f @* K ><| f @* H].
+ +
+Lemma injm_Frobenius_ker K sGD injf :
+ [Frobenius G with kernel K] → [Frobenius f @* G with kernel f @* K].
+ +
+Lemma injm_Frobenius_group sGD injf : [Frobenius G] → [Frobenius f @* G].
+ +
+End InjmFrobenius.
+ +
+Theorem Frobenius_Ldiv (gT : finGroupType) (G : {group gT}) n :
+ n %| #|G| → n %| #|'Ldiv_n(G)|.
+
++ +
+Definition normedTI A G L := [&& A != set0, trivIset (A :^: G) & 'N_G(A) == L].
+ +
+Definition Frobenius_group_with_complement G H := (H != G) && normedTI H^# G H.
+ +
+Definition Frobenius_group G :=
+ [∃ H : {group gT}, Frobenius_group_with_complement G H].
+ +
+Definition Frobenius_group_with_kernel_and_complement G K H :=
+ (K ><| H == G) && Frobenius_group_with_complement G H.
+ +
+Definition Frobenius_group_with_kernel G K :=
+ [∃ H : {group gT}, Frobenius_group_with_kernel_and_complement G K H].
+ +
+Section FrobeniusAction.
+ +
+Variables G H : {set gT}.
+Variables (sT : finType) (S : {set sT}) (to : {action gT &-> sT}).
+ +
+Definition Frobenius_action :=
+ [/\ [faithful G, on S | to],
+ [transitive G, on S | to],
+ {in G^#, ∀ x, #|'Fix_(S | to)[x]| ≤ 1},
+ H != 1
+ & exists2 u, u \in S & H = 'C_G[u | to]].
+ +
+End FrobeniusAction.
+ +
+CoInductive has_Frobenius_action G H : Prop :=
+ HasFrobeniusAction sT S to of @Frobenius_action G H sT S to.
+ +
+End Definitions.
+ +
+ +
+Notation "[ 'Frobenius' G 'with' 'complement' H ]" :=
+ (Frobenius_group_with_complement G H)
+ (at level 0, G at level 50, H at level 35,
+ format "[ 'Frobenius' G 'with' 'complement' H ]") : group_scope.
+ +
+Notation "[ 'Frobenius' G 'with' 'kernel' K ]" :=
+ (Frobenius_group_with_kernel G K)
+ (at level 0, G at level 50, K at level 35,
+ format "[ 'Frobenius' G 'with' 'kernel' K ]") : group_scope.
+ +
+Notation "[ 'Frobenius' G ]" :=
+ (Frobenius_group G)
+ (at level 0, G at level 50,
+ format "[ 'Frobenius' G ]") : group_scope.
+ +
+Notation "[ 'Frobenius' G = K ><| H ]" :=
+ (Frobenius_group_with_kernel_and_complement G K H)
+ (at level 0, G at level 50, K, H at level 35,
+ format "[ 'Frobenius' G = K ><| H ]") : group_scope.
+ +
+Section FrobeniusBasics.
+ +
+Variable gT : finGroupType.
+Implicit Types (A B : {set gT}) (G H K L R X : {group gT}).
+ +
+Lemma semiregular1l H : semiregular 1 H.
+ +
+Lemma semiregular1r K : semiregular K 1.
+ +
+Lemma semiregular_sym H K : semiregular K H → semiregular H K.
+ +
+Lemma semiregularS K1 K2 A1 A2 :
+ K1 \subset K2 → A1 \subset A2 → semiregular K2 A2 → semiregular K1 A1.
+ +
+Lemma semiregular_prime H K : semiregular K H → semiprime K H.
+ +
+Lemma semiprime_regular H K : semiprime K H → 'C_K(H) = 1 → semiregular K H.
+ +
+Lemma semiprimeS K1 K2 A1 A2 :
+ K1 \subset K2 → A1 \subset A2 → semiprime K2 A2 → semiprime K1 A1.
+ +
+Lemma cent_semiprime H K X :
+ semiprime K H → X \subset H → X :!=: 1 → 'C_K(X) = 'C_K(H).
+ +
+Lemma stab_semiprime H K X :
+ semiprime K H → X \subset K → 'C_H(X) != 1 → 'C_H(X) = H.
+ +
+Lemma cent_semiregular H K X :
+ semiregular K H → X \subset H → X :!=: 1 → 'C_K(X) = 1.
+ +
+Lemma regular_norm_dvd_pred K H :
+ H \subset 'N(K) → semiregular K H → #|H| %| #|K|.-1.
+ +
+Lemma regular_norm_coprime K H :
+ H \subset 'N(K) → semiregular K H → coprime #|K| #|H|.
+ +
+Lemma semiregularJ K H x : semiregular K H → semiregular (K :^ x) (H :^ x).
+ +
+Lemma semiprimeJ K H x : semiprime K H → semiprime (K :^ x) (H :^ x).
+ +
+Lemma normedTI_P A G L :
+ reflect [/\ A != set0, L \subset 'N_G(A)
+ & {in G, ∀ g, ~~ [disjoint A & A :^ g] → g \in L}]
+ (normedTI A G L).
+ +
+Lemma normedTI_memJ_P A G L :
+ reflect [/\ A != set0, L \subset G
+ & {in A & G, ∀ a g, (a ^ g \in A) = (g \in L)}]
+ (normedTI A G L).
+ +
+Lemma partition_class_support A G :
+ A != set0 → trivIset (A :^: G) → partition (A :^: G) (class_support A G).
+ +
+Lemma partition_normedTI A G L :
+ normedTI A G L → partition (A :^: G) (class_support A G).
+ +
+Lemma card_support_normedTI A G L :
+ normedTI A G L → #|class_support A G| = (#|A| × #|G : L|)%N.
+ +
+Lemma normedTI_S A B G L :
+ A != set0 → L \subset 'N(A) → A \subset B → normedTI B G L →
+ normedTI A G L.
+ +
+Lemma cent1_normedTI A G L :
+ normedTI A G L → {in A, ∀ x, 'C_G[x] \subset L}.
+ +
+Lemma Frobenius_actionP G H :
+ reflect (has_Frobenius_action G H) [Frobenius G with complement H].
+ +
+Section FrobeniusProperties.
+ +
+Variables G H K : {group gT}.
+Hypothesis frobG : [Frobenius G = K ><| H].
+ +
+Lemma FrobeniusWker : [Frobenius G with kernel K].
+ +
+Lemma FrobeniusWcompl : [Frobenius G with complement H].
+ +
+Lemma FrobeniusW : [Frobenius G].
+ +
+Lemma Frobenius_context :
+ [/\ K ><| H = G, K :!=: 1, H :!=: 1, K \proper G & H \proper G].
+ +
+Lemma Frobenius_partition : partition (gval K |: (H^# :^: K)) G.
+ +
+Lemma Frobenius_cent1_ker : {in K^#, ∀ x, 'C_G[x] \subset K}.
+ +
+Lemma Frobenius_reg_ker : semiregular K H.
+ +
+Lemma Frobenius_reg_compl : semiregular H K.
+ +
+Lemma Frobenius_dvd_ker1 : #|H| %| #|K|.-1.
+ +
+Lemma ltn_odd_Frobenius_ker : odd #|G| → #|H|.*2 < #|K|.
+ +
+Lemma Frobenius_index_dvd_ker1 : #|G : K| %| #|K|.-1.
+ +
+Lemma Frobenius_coprime : coprime #|K| #|H|.
+ +
+Lemma Frobenius_trivg_cent : 'C_K(H) = 1.
+ +
+Lemma Frobenius_index_coprime : coprime #|K| #|G : K|.
+ +
+Lemma Frobenius_ker_Hall : Hall G K.
+ +
+Lemma Frobenius_compl_Hall : Hall G H.
+ +
+End FrobeniusProperties.
+ +
+Lemma normedTI_J x A G L : normedTI (A :^ x) (G :^ x) (L :^ x) = normedTI A G L.
+ +
+Lemma FrobeniusJcompl x G H :
+ [Frobenius G :^ x with complement H :^ x] = [Frobenius G with complement H].
+ +
+Lemma FrobeniusJ x G K H :
+ [Frobenius G :^ x = K :^ x ><| H :^ x] = [Frobenius G = K ><| H].
+ +
+Lemma FrobeniusJker x G K :
+ [Frobenius G :^ x with kernel K :^ x] = [Frobenius G with kernel K].
+ +
+Lemma FrobeniusJgroup x G : [Frobenius G :^ x] = [Frobenius G].
+ +
+Lemma Frobenius_ker_dvd_ker1 G K :
+ [Frobenius G with kernel K] → #|G : K| %| #|K|.-1.
+ +
+Lemma Frobenius_ker_coprime G K :
+ [Frobenius G with kernel K] → coprime #|K| #|G : K|.
+ +
+Lemma Frobenius_semiregularP G K H :
+ K ><| H = G → K :!=: 1 → H :!=: 1 →
+ reflect (semiregular K H) [Frobenius G = K ><| H].
+ +
+Lemma prime_FrobeniusP G K H :
+ K :!=: 1 → prime #|H| →
+ reflect (K ><| H = G ∧ 'C_K(H) = 1) [Frobenius G = K ><| H].
+ +
+Lemma Frobenius_subl G K K1 H :
+ K1 :!=: 1 → K1 \subset K → H \subset 'N(K1) → [Frobenius G = K ><| H] →
+ [Frobenius K1 <*> H = K1 ><| H].
+ +
+Lemma Frobenius_subr G K H H1 :
+ H1 :!=: 1 → H1 \subset H → [Frobenius G = K ><| H] →
+ [Frobenius K <*> H1 = K ><| H1].
+ +
+Lemma Frobenius_kerP G K :
+ reflect [/\ K :!=: 1, K \proper G, K <| G
+ & {in K^#, ∀ x, 'C_G[x] \subset K}]
+ [Frobenius G with kernel K].
+ +
+Lemma set_Frobenius_compl G K H :
+ K ><| H = G → [Frobenius G with kernel K] → [Frobenius G = K ><| H].
+ +
+Lemma Frobenius_kerS G K G1 :
+ G1 \subset G → K \proper G1 →
+ [Frobenius G with kernel K] → [Frobenius G1 with kernel K].
+ +
+Lemma Frobenius_action_kernel_def G H K sT S to :
+ K ><| H = G → @Frobenius_action _ G H sT S to →
+ K :=: 1 :|: [set x in G | 'Fix_(S | to)[x] == set0].
+ +
+End FrobeniusBasics.
+ +
+ +
+Lemma Frobenius_coprime_quotient (gT : finGroupType) (G K H N : {group gT}) :
+ K ><| H = G → N <| G → coprime #|K| #|H| ∧ H :!=: 1%g →
+ N \proper K ∧ {in H^#, ∀ x, 'C_K[x] \subset N} →
+ [Frobenius G / N = (K / N) ><| (H / N)]%g.
+ +
+Section InjmFrobenius.
+ +
+Variables (gT rT : finGroupType) (D G : {group gT}) (f : {morphism D >-> rT}).
+Implicit Types (H K : {group gT}) (sGD : G \subset D) (injf : 'injm f).
+ +
+Lemma injm_Frobenius_compl H sGD injf :
+ [Frobenius G with complement H] → [Frobenius f @* G with complement f @* H].
+ +
+Lemma injm_Frobenius H K sGD injf :
+ [Frobenius G = K ><| H] → [Frobenius f @* G = f @* K ><| f @* H].
+ +
+Lemma injm_Frobenius_ker K sGD injf :
+ [Frobenius G with kernel K] → [Frobenius f @* G with kernel f @* K].
+ +
+Lemma injm_Frobenius_group sGD injf : [Frobenius G] → [Frobenius f @* G].
+ +
+End InjmFrobenius.
+ +
+Theorem Frobenius_Ldiv (gT : finGroupType) (G : {group gT}) n :
+ n %| #|G| → n %| #|'Ldiv_n(G)|.
+