From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 22 May 2019 13:43:08 +0200 Subject: htmldoc regenerated --- docs/htmldoc/mathcomp.character.inertia.html | 553 +++++++++++++-------------- 1 file changed, 276 insertions(+), 277 deletions(-) (limited to 'docs/htmldoc/mathcomp.character.inertia.html') diff --git a/docs/htmldoc/mathcomp.character.inertia.html b/docs/htmldoc/mathcomp.character.inertia.html index 7e00558..e3fece2 100644 --- a/docs/htmldoc/mathcomp.character.inertia.html +++ b/docs/htmldoc/mathcomp.character.inertia.html @@ -21,7 +21,6 @@
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.

Set Implicit Arguments.
@@ -62,45 +61,45 @@ Section ConjDef.

-Variables (gT : finGroupType) (B : {set gT}) (y : gT) (phi : 'CF(B)).
+Variables (gT : finGroupType) (B : {set gT}) (y : gT) (phi : 'CF(B)).

Fact cfConjg_subproof :
-  is_class_fun G [ffun x ⇒ phi (if y \in 'N(G) then x ^ y^-1 else x)].
+  is_class_fun G [ffun x ⇒ phi (if y \in 'N(G) then x ^ y^-1 else x)].
Definition cfConjg := Cfun 1 cfConjg_subproof.

End ConjDef.

-Notation "f ^ y" := (cfConjg y f) : cfun_scope.
+Notation "f ^ y" := (cfConjg y f) : cfun_scope.

Section Conj.

-Variables (gT : finGroupType) (G : {group gT}).
-Implicit Type phi : 'CF(G).
+Variables (gT : finGroupType) (G : {group gT}).
+Implicit Type phi : 'CF(G).

-Lemma cfConjgE phi y x : y \in 'N(G) → (phi ^ y)%CF x = phi (x ^ y^-1)%g.
+Lemma cfConjgE phi y x : y \in 'N(G) → (phi ^ y)%CF x = phi (x ^ y^-1)%g.

-Lemma cfConjgEJ phi y x : y \in 'N(G) → (phi ^ y)%CF (x ^ y) = phi x.
+Lemma cfConjgEJ phi y x : y \in 'N(G) → (phi ^ y)%CF (x ^ y) = phi x.

-Lemma cfConjgEout phi y : y \notin 'N(G) → (phi ^ y = phi)%CF.
+Lemma cfConjgEout phi y : y \notin 'N(G) → (phi ^ y = phi)%CF.

-Lemma cfConjgEin phi y (nGy : y \in 'N(G)) :
-  (phi ^ y)%CF = cfIsom (norm_conj_isom nGy) phi.
+Lemma cfConjgEin phi y (nGy : y \in 'N(G)) :
+  (phi ^ y)%CF = cfIsom (norm_conj_isom nGy) phi.

Lemma cfConjgMnorm phi :
-  {in 'N(G) &, ∀ y z, phi ^ (y × z) = (phi ^ y) ^ z}%CF.
+  {in 'N(G) &, ∀ y z, phi ^ (y × z) = (phi ^ y) ^ z}%CF.

-Lemma cfConjg_id phi y : y \in G → (phi ^ y)%CF = phi.
+Lemma cfConjg_id phi y : y \in G → (phi ^ y)%CF = phi.

@@ -110,53 +109,53 @@
Lemma cfConjgM L phi :
-  G <| L → {in L &, ∀ y z, phi ^ (y × z) = (phi ^ y) ^ z}%CF.
+  G <| L → {in L &, ∀ y z, phi ^ (y × z) = (phi ^ y) ^ z}%CF.

-Lemma cfConjgJ1 phi : (phi ^ 1)%CF = phi.
+Lemma cfConjgJ1 phi : (phi ^ 1)%CF = phi.

-Lemma cfConjgK y : cancel (cfConjg y) (cfConjg y^-1 : 'CF(G) → 'CF(G)).
+Lemma cfConjgK y : cancel (cfConjg y) (cfConjg y^-1 : 'CF(G) → 'CF(G)).

-Lemma cfConjgKV y : cancel (cfConjg y^-1) (cfConjg y : 'CF(G) → 'CF(G)).
+Lemma cfConjgKV y : cancel (cfConjg y^-1) (cfConjg y : 'CF(G) → 'CF(G)).

-Lemma cfConjg1 phi y : (phi ^ y)%CF 1%g = phi 1%g.
+Lemma cfConjg1 phi y : (phi ^ y)%CF 1%g = phi 1%g.

-Fact cfConjg_is_linear y : linear (cfConjg y : 'CF(G) → 'CF(G)).
+Fact cfConjg_is_linear y : linear (cfConjg y : 'CF(G) → 'CF(G)).
Canonical cfConjg_additive y := Additive (cfConjg_is_linear y).
Canonical cfConjg_linear y := AddLinear (cfConjg_is_linear y).

-Lemma cfConjg_cfuniJ A y : y \in 'N(G) → ('1_A ^ y)%CF = '1_(A :^ y) :> 'CF(G).
+Lemma cfConjg_cfuniJ A y : y \in 'N(G) → ('1_A ^ y)%CF = '1_(A :^ y) :> 'CF(G).

-Lemma cfConjg_cfuni A y : y \in 'N(A) → ('1_A ^ y)%CF = '1_A :> 'CF(G).
+Lemma cfConjg_cfuni A y : y \in 'N(A) → ('1_A ^ y)%CF = '1_A :> 'CF(G).

-Lemma cfConjg_cfun1 y : (1 ^ y)%CF = 1 :> 'CF(G).
+Lemma cfConjg_cfun1 y : (1 ^ y)%CF = 1 :> 'CF(G).

-Fact cfConjg_is_multiplicative y : multiplicative (cfConjg y : _ → 'CF(G)).
+Fact cfConjg_is_multiplicative y : multiplicative (cfConjg y : _ → 'CF(G)).
Canonical cfConjg_rmorphism y := AddRMorphism (cfConjg_is_multiplicative y).
-Canonical cfConjg_lrmorphism y := [lrmorphism of cfConjg y].
+Canonical cfConjg_lrmorphism y := [lrmorphism of cfConjg y].

-Lemma cfConjg_eq1 phi y : ((phi ^ y)%CF == 1) = (phi == 1).
+Lemma cfConjg_eq1 phi y : ((phi ^ y)%CF == 1) = (phi == 1).

-Lemma cfAutConjg phi u y : cfAut u (phi ^ y) = (cfAut u phi ^ y)%CF.
+Lemma cfAutConjg phi u y : cfAut u (phi ^ y) = (cfAut u phi ^ y)%CF.

-Lemma conj_cfConjg phi y : (phi ^ y)^*%CF = (phi^* ^ y)%CF.
+Lemma conj_cfConjg phi y : (phi ^ y)^*%CF = (phi^* ^ y)%CF.

-Lemma cfker_conjg phi y : y \in 'N(G) → cfker (phi ^ y) = cfker phi :^ y.
+Lemma cfker_conjg phi y : y \in 'N(G) → cfker (phi ^ y) = cfker phi :^ y.

-Lemma cfDetConjg phi y : cfDet (phi ^ y) = (cfDet phi ^ y)%CF.
+Lemma cfDetConjg phi y : cfDet (phi ^ y) = (cfDet phi ^ y)%CF.

End Conj.
@@ -168,26 +167,26 @@ Variable gT : finGroupType.

-Definition inertia (B : {set gT}) (phi : 'CF(B)) :=
-  [set y in 'N(B) | (phi ^ y)%CF == phi].
+Definition inertia (B : {set gT}) (phi : 'CF(B)) :=
+  [set y in 'N(B) | (phi ^ y)%CF == phi].


-Fact group_set_inertia (H : {group gT}) phi : group_set 'I[phi : 'CF(H)].
+Fact group_set_inertia (H : {group gT}) phi : group_set 'I[phi : 'CF(H)].
Canonical inertia_group H phi := Group (@group_set_inertia H phi).


-Variables G H : {group gT}.
-Implicit Type phi : 'CF(H).
+Variables G H : {group gT}.
+Implicit Type phi : 'CF(H).

-Lemma inertiaJ phi y : y \in 'I[phi] → (phi ^ y)%CF = phi.
+Lemma inertiaJ phi y : y \in 'I[phi] → (phi ^ y)%CF = phi.

-Lemma inertia_valJ phi x y : y \in 'I[phi] → phi (x ^ y)%g = phi x.
+Lemma inertia_valJ phi x y : y \in 'I[phi] → phi (x ^ y)%g = phi x.

@@ -197,87 +196,87 @@ lemmas concerning the localized inertia group 'I_G[phi].
-Lemma Inertia_sub phi : 'I_G[phi] \subset G.
+Lemma Inertia_sub phi : 'I_G[phi] \subset G.

-Lemma norm_inertia phi : 'I[phi] \subset 'N(H).
+Lemma norm_inertia phi : 'I[phi] \subset 'N(H).

-Lemma sub_inertia phi : H \subset 'I[phi].
+Lemma sub_inertia phi : H \subset 'I[phi].

-Lemma normal_inertia phi : H <| 'I[phi].
+Lemma normal_inertia phi : H <| 'I[phi].

-Lemma sub_Inertia phi : H \subset G → H \subset 'I_G[phi].
+Lemma sub_Inertia phi : H \subset G → H \subset 'I_G[phi].

-Lemma norm_Inertia phi : 'I_G[phi] \subset 'N(H).
+Lemma norm_Inertia phi : 'I_G[phi] \subset 'N(H).

-Lemma normal_Inertia phi : H \subset G → H <| 'I_G[phi].
+Lemma normal_Inertia phi : H \subset G → H <| 'I_G[phi].

Lemma cfConjg_eqE phi :
-    H <| G →
-  {in G &, ∀ y z, (phi ^ y == phi ^ z)%CF = (z \in 'I_G[phi] :* y)}.
+    H <| G →
+  {in G &, ∀ y z, (phi ^ y == phi ^ z)%CF = (z \in 'I_G[phi] :* y)}.

-Lemma cent_sub_inertia phi : 'C(H) \subset 'I[phi].
+Lemma cent_sub_inertia phi : 'C(H) \subset 'I[phi].

-Lemma cent_sub_Inertia phi : 'C_G(H) \subset 'I_G[phi].
+Lemma cent_sub_Inertia phi : 'C_G(H) \subset 'I_G[phi].

-Lemma center_sub_Inertia phi : H \subset G → 'Z(G) \subset 'I_G[phi].
+Lemma center_sub_Inertia phi : H \subset G → 'Z(G) \subset 'I_G[phi].

-Lemma conjg_inertia phi y : y \in 'N(H) → 'I[phi] :^ y = 'I[phi ^ y].
+Lemma conjg_inertia phi y : y \in 'N(H) → 'I[phi] :^ y = 'I[phi ^ y].

-Lemma inertia0 : 'I[0 : 'CF(H)] = 'N(H).
+Lemma inertia0 : 'I[0 : 'CF(H)] = 'N(H).

-Lemma inertia_add phi psi : 'I[phi] :&: 'I[psi] \subset 'I[phi + psi].
+Lemma inertia_add phi psi : 'I[phi] :&: 'I[psi] \subset 'I[phi + psi].

-Lemma inertia_sum I r (P : pred I) (Phi : I → 'CF(H)) :
-  'N(H) :&: \bigcap_(i <- r | P i) 'I[Phi i]
-     \subset 'I[\sum_(i <- r | P i) Phi i].
+Lemma inertia_sum I r (P : pred I) (Phi : I → 'CF(H)) :
+  'N(H) :&: \bigcap_(i <- r | P i) 'I[Phi i]
+     \subset 'I[\sum_(i <- r | P i) Phi i].

-Lemma inertia_scale a phi : 'I[phi] \subset 'I[a *: phi].
+Lemma inertia_scale a phi : 'I[phi] \subset 'I[a *: phi].

-Lemma inertia_scale_nz a phi : a != 0 → 'I[a *: phi] = 'I[phi].
+Lemma inertia_scale_nz a phi : a != 0 → 'I[a *: phi] = 'I[phi].

-Lemma inertia_opp phi : 'I[- phi] = 'I[phi].
+Lemma inertia_opp phi : 'I[- phi] = 'I[phi].

-Lemma inertia1 : 'I[1 : 'CF(H)] = 'N(H).
+Lemma inertia1 : 'I[1 : 'CF(H)] = 'N(H).

-Lemma Inertia1 : H <| G → 'I_G[1 : 'CF(H)] = G.
+Lemma Inertia1 : H <| G → 'I_G[1 : 'CF(H)] = G.

-Lemma inertia_mul phi psi : 'I[phi] :&: 'I[psi] \subset 'I[phi × psi].
+Lemma inertia_mul phi psi : 'I[phi] :&: 'I[psi] \subset 'I[phi × psi].

-Lemma inertia_prod I r (P : pred I) (Phi : I → 'CF(H)) :
-  'N(H) :&: \bigcap_(i <- r | P i) 'I[Phi i]
-     \subset 'I[\prod_(i <- r | P i) Phi i].
+Lemma inertia_prod I r (P : pred I) (Phi : I → 'CF(H)) :
+  'N(H) :&: \bigcap_(i <- r | P i) 'I[Phi i]
+     \subset 'I[\prod_(i <- r | P i) Phi i].

-Lemma inertia_injective (chi : 'CF(H)) :
-  {in H &, injective chi} → 'I[chi] = 'C(H).
+Lemma inertia_injective (chi : 'CF(H)) :
+  {in H &, injective chi} → 'I[chi] = 'C(H).

Lemma inertia_irr_prime p i :
-  #|H| = p → prime p → i != 0 → 'I['chi[H]_i] = 'C(H).
+  #|H| = p → prime p → i != 0 → 'I['chi[H]_i] = 'C(H).

-Lemma inertia_irr0 : 'I['chi[H]_0] = 'N(H).
+Lemma inertia_irr0 : 'I['chi[H]_0] = 'N(H).

@@ -286,7 +285,7 @@ Isaacs' 6.1.c
-Lemma cfConjg_iso y : isometry (cfConjg y : 'CF(H) → 'CF(H)).
+Lemma cfConjg_iso y : isometry (cfConjg y : 'CF(H) → 'CF(H)).

@@ -296,7 +295,7 @@
Lemma cfdot_Res_conjg psi phi y :
-  y \in G → '['Res[H, G] psi, phi ^ y] = '['Res[H] psi, phi].
+  y \in G → '['Res[H, G] psi, phi ^ y] = '['Res[H] psi, phi].

@@ -305,104 +304,104 @@ Isaac's 6.1.e
-Lemma cfConjg_char (chi : 'CF(H)) y :
-  chi \is a character → (chi ^ y)%CF \is a character.
+Lemma cfConjg_char (chi : 'CF(H)) y :
+  chi \is a character → (chi ^ y)%CF \is a character.

-Lemma cfConjg_lin_char (chi : 'CF(H)) y :
-  chi \is a linear_char → (chi ^ y)%CF \is a linear_char.
+Lemma cfConjg_lin_char (chi : 'CF(H)) y :
+  chi \is a linear_char → (chi ^ y)%CF \is a linear_char.

-Lemma cfConjg_irr y chi : chi \in irr H → (chi ^ y)%CF \in irr H.
+Lemma cfConjg_irr y chi : chi \in irr H → (chi ^ y)%CF \in irr H.

-Definition conjg_Iirr i y := cfIirr ('chi[H]_i ^ y)%CF.
+Definition conjg_Iirr i y := cfIirr ('chi[H]_i ^ y)%CF.

-Lemma conjg_IirrE i y : 'chi_(conjg_Iirr i y) = ('chi_i ^ y)%CF.
+Lemma conjg_IirrE i y : 'chi_(conjg_Iirr i y) = ('chi_i ^ y)%CF.

-Lemma conjg_IirrK y : cancel (conjg_Iirr^~ y) (conjg_Iirr^~ y^-1%g).
+Lemma conjg_IirrK y : cancel (conjg_Iirr^~ y) (conjg_Iirr^~ y^-1%g).

-Lemma conjg_IirrKV y : cancel (conjg_Iirr^~ y^-1%g) (conjg_Iirr^~ y).
+Lemma conjg_IirrKV y : cancel (conjg_Iirr^~ y^-1%g) (conjg_Iirr^~ y).

-Lemma conjg_Iirr_inj y : injective (conjg_Iirr^~ y).
+Lemma conjg_Iirr_inj y : injective (conjg_Iirr^~ y).

-Lemma conjg_Iirr_eq0 i y : (conjg_Iirr i y == 0) = (i == 0).
+Lemma conjg_Iirr_eq0 i y : (conjg_Iirr i y == 0) = (i == 0).

-Lemma conjg_Iirr0 x : conjg_Iirr 0 x = 0.
+Lemma conjg_Iirr0 x : conjg_Iirr 0 x = 0.

Lemma cfdot_irr_conjg i y :
-  H <| G → y \in G → '['chi_i, 'chi_i ^ y]_H = (y \in 'I_G['chi_i])%:R.
+  H <| G → y \in G → '['chi_i, 'chi_i ^ y]_H = (y \in 'I_G['chi_i])%:R.

-Definition cfclass (A : {set gT}) (phi : 'CF(A)) (B : {set gT}) :=
-  [seq (phi ^ repr Tx)%CF | Tx in rcosets 'I_B[phi] B].
+Definition cfclass (A : {set gT}) (phi : 'CF(A)) (B : {set gT}) :=
+  [seq (phi ^ repr Tx)%CF | Tx in rcosets 'I_B[phi] B].


-Lemma size_cfclass i : size ('chi[H]_i ^: G)%CF = #|G : 'I_G['chi_i]|.
+Lemma size_cfclass i : size ('chi[H]_i ^: G)%CF = #|G : 'I_G['chi_i]|.

-Lemma cfclassP (A : {group gT}) phi psi :
-  reflect (exists2 y, y \in A & psi = phi ^ y)%CF (psi \in phi ^: A)%CF.
+Lemma cfclassP (A : {group gT}) phi psi :
+  reflect (exists2 y, y \in A & psi = phi ^ y)%CF (psi \in phi ^: A)%CF.

-Lemma cfclassInorm phi : (phi ^: 'N_G(H) =i phi ^: G)%CF.
+Lemma cfclassInorm phi : (phi ^: 'N_G(H) =i phi ^: G)%CF.

-Lemma cfclass_refl phi : phi \in (phi ^: G)%CF.
+Lemma cfclass_refl phi : phi \in (phi ^: G)%CF.

Lemma cfclass_transr phi psi :
-  (psi \in phi ^: G)%CF → (phi ^: G =i psi ^: G)%CF.
+  (psi \in phi ^: G)%CF → (phi ^: G =i psi ^: G)%CF.

-Lemma cfclass_sym phi psi : (psi \in phi ^: G)%CF = (phi \in psi ^: G)%CF.
+Lemma cfclass_sym phi psi : (psi \in phi ^: G)%CF = (phi \in psi ^: G)%CF.

-Lemma cfclass_uniq phi : H <| G → uniq (phi ^: G)%CF.
+Lemma cfclass_uniq phi : H <| G → uniq (phi ^: G)%CF.

-Lemma cfclass_invariant phi : G \subset 'I[phi] → (phi ^: G)%CF = phi.
+Lemma cfclass_invariant phi : G \subset 'I[phi] → (phi ^: G)%CF = phi.

-Lemma cfclass1 : H <| G → (1 ^: G)%CF = [:: 1 : 'CF(H)].
+Lemma cfclass1 : H <| G → (1 ^: G)%CF = [:: 1 : 'CF(H)].

-Definition cfclass_Iirr (A : {set gT}) i := conjg_Iirr i @: A.
+Definition cfclass_Iirr (A : {set gT}) i := conjg_Iirr i @: A.

Lemma cfclass_IirrE i j :
-  (j \in cfclass_Iirr G i) = ('chi_j \in 'chi_i ^: G)%CF.
+  (j \in cfclass_Iirr G i) = ('chi_j \in 'chi_i ^: G)%CF.

Lemma eq_cfclass_IirrE i j :
-  (cfclass_Iirr G j == cfclass_Iirr G i) = (j \in cfclass_Iirr G i).
+  (cfclass_Iirr G j == cfclass_Iirr G i) = (j \in cfclass_Iirr G i).

Lemma im_cfclass_Iirr i :
-  H <| G → perm_eq [seq 'chi_j | j in cfclass_Iirr G i] ('chi_i ^: G)%CF.
+  H <| G → perm_eq [seq 'chi_j | j in cfclass_Iirr G i] ('chi_i ^: G)%CF.

-Lemma card_cfclass_Iirr i : H <| G → #|cfclass_Iirr G i| = #|G : 'I_G['chi_i]|.
+Lemma card_cfclass_Iirr i : H <| G → #|cfclass_Iirr G i| = #|G : 'I_G['chi_i]|.

-Lemma reindex_cfclass R idx (op : Monoid.com_law idx) (F : 'CF(H) → R) i :
-     H <| G →
-  \big[op/idx]_(chi <- ('chi_i ^: G)%CF) F chi
-     = \big[op/idx]_(j | 'chi_j \in ('chi_i ^: G)%CF) F 'chi_j.
+Lemma reindex_cfclass R idx (op : Monoid.com_law idx) (F : 'CF(H) → R) i :
+     H <| G →
+  \big[op/idx]_(chi <- ('chi_i ^: G)%CF) F chi
+     = \big[op/idx]_(j | 'chi_j \in ('chi_i ^: G)%CF) F 'chi_j.

Lemma cfResInd j:
-    H <| G →
-  'Res[H] ('Ind[G] 'chi_j) = #|H|%:R^-1 *: (\sum_(y in G) 'chi_j ^ y)%CF.
+    H <| G →
+  'Res[H] ('Ind[G] 'chi_j) = #|H|%:R^-1 *: (\sum_(y in G) 'chi_j ^ y)%CF.

@@ -412,13 +411,13 @@
Lemma Clifford_Res_sum_cfclass i j :
-     H <| G → j \in irr_constt ('Res[H, G] 'chi_i) →
-  'Res[H] 'chi_i =
-     '['Res[H] 'chi_i, 'chi_j] *: (\sum_(chi <- ('chi_j ^: G)%CF) chi).
+     H <| G → j \in irr_constt ('Res[H, G] 'chi_i) →
+  'Res[H] 'chi_i =
+     '['Res[H] 'chi_i, 'chi_j] *: (\sum_(chi <- ('chi_j ^: G)%CF) chi).

Lemma cfRes_Ind_invariant psi :
-  H <| G → G \subset 'I[psi] → 'Res ('Ind[G, H] psi) = #|G : H|%:R *: psi.
+  H <| G → G \subset 'I[psi] → 'Res ('Ind[G, H] psi) = #|G : H|%:R *: psi.

@@ -428,7 +427,7 @@
Corollary constt0_Res_cfker i :
-  H <| G → 0 \in irr_constt ('Res[H] 'chi[G]_i) → H \subset cfker 'chi[G]_i.
+  H <| G → 0 \in irr_constt ('Res[H] 'chi[G]_i) → H \subset cfker 'chi[G]_i.

@@ -438,12 +437,12 @@
Lemma dvdn_constt_Res1_irr1 i j :
-    H <| G → j \in irr_constt ('Res[H, G] 'chi_i) →
-  ∃ n, 'chi_i 1%g = n%:R × 'chi_j 1%g.
+    H <| G → j \in irr_constt ('Res[H, G] 'chi_i) →
+  ∃ n, 'chi_i 1%g = n%:R × 'chi_j 1%g.

Lemma cfclass_Ind phi psi :
-  H <| G → psi \in (phi ^: G)%CF → 'Ind[G] phi = 'Ind[G] psi.
+  H <| G → psi \in (phi ^: G)%CF → 'Ind[G] phi = 'Ind[G] psi.

End Inertia.
@@ -451,41 +450,41 @@

-Notation "''I[' phi ] " := (inertia phi) : group_scope.
-Notation "''I[' phi ] " := (inertia_group phi) : Group_scope.
-Notation "''I_' G [ phi ] " := (G%g :&: 'I[phi]) : group_scope.
-Notation "''I_' G [ phi ] " := (G :&: 'I[phi])%G : Group_scope.
-Notation "phi ^: G" := (cfclass phi G) : cfun_scope.
+Notation "''I[' phi ] " := (inertia phi) : group_scope.
+Notation "''I[' phi ] " := (inertia_group phi) : Group_scope.
+Notation "''I_' G [ phi ] " := (G%g :&: 'I[phi]) : group_scope.
+Notation "''I_' G [ phi ] " := (G :&: 'I[phi])%G : Group_scope.
+Notation "phi ^: G" := (cfclass phi G) : cfun_scope.

Section ConjRestrict.

-Variables (gT : finGroupType) (G H K : {group gT}).
+Variables (gT : finGroupType) (G H K : {group gT}).

Lemma cfConjgRes_norm phi y :
-  y \in 'N(K) → y \in 'N(H) → ('Res[K, H] phi ^ y)%CF = 'Res (phi ^ y)%CF.
+  y \in 'N(K) → y \in 'N(H) → ('Res[K, H] phi ^ y)%CF = 'Res (phi ^ y)%CF.

Lemma cfConjgRes phi y :
-  H <| G → K <| G → y \in G → ('Res[K, H] phi ^ y)%CF = 'Res (phi ^ y)%CF.
+  H <| G → K <| G → y \in G → ('Res[K, H] phi ^ y)%CF = 'Res (phi ^ y)%CF.

Lemma sub_inertia_Res phi :
-  G \subset 'N(K) → 'I_G[phi] \subset 'I_G['Res[K, H] phi].
+  G \subset 'N(K) → 'I_G[phi] \subset 'I_G['Res[K, H] phi].

Lemma cfConjgInd_norm phi y :
-  y \in 'N(K) → y \in 'N(H) → ('Ind[H, K] phi ^ y)%CF = 'Ind (phi ^ y)%CF.
+  y \in 'N(K) → y \in 'N(H) → ('Ind[H, K] phi ^ y)%CF = 'Ind (phi ^ y)%CF.

Lemma cfConjgInd phi y :
-  H <| G → K <| G → y \in G → ('Ind[H, K] phi ^ y)%CF = 'Ind (phi ^ y)%CF.
+  H <| G → K <| G → y \in G → ('Ind[H, K] phi ^ y)%CF = 'Ind (phi ^ y)%CF.

Lemma sub_inertia_Ind phi :
-  G \subset 'N(H) → 'I_G[phi] \subset 'I_G['Ind[H, K] phi].
+  G \subset 'N(H) → 'I_G[phi] \subset 'I_G['Ind[H, K] phi].

End ConjRestrict.
@@ -494,14 +493,14 @@ Section MoreInertia.

-Variables (gT : finGroupType) (G H : {group gT}) (i : Iirr H).
-Let T := 'I_G['chi_i].
+Variables (gT : finGroupType) (G H : {group gT}) (i : Iirr H).
+Let T := 'I_G['chi_i].

-Lemma inertia_id : 'I_T['chi_i] = T.
+Lemma inertia_id : 'I_T['chi_i] = T.

-Lemma cfclass_inertia : ('chi[H]_i ^: T)%CF = [:: 'chi_i].
+Lemma cfclass_inertia : ('chi[H]_i ^: T)%CF = [:: 'chi_i].

End MoreInertia.
@@ -510,25 +509,25 @@ Section ConjMorph.

-Variables (aT rT : finGroupType) (D G H : {group aT}) (f : {morphism D >-> rT}).
+Variables (aT rT : finGroupType) (D G H : {group aT}) (f : {morphism D >-> rT}).

-Lemma cfConjgMorph (phi : 'CF(f @* H)) y :
-  y \in D → y \in 'N(H) → (cfMorph phi ^ y)%CF = cfMorph (phi ^ f y).
+Lemma cfConjgMorph (phi : 'CF(f @* H)) y :
+  y \in D → y \in 'N(H) → (cfMorph phi ^ y)%CF = cfMorph (phi ^ f y).

-Lemma inertia_morph_pre (phi : 'CF(f @* H)) :
-  H <| G → G \subset D → 'I_G[cfMorph phi] = G :&: f @*^-1 'I_(f @* G)[phi].
+Lemma inertia_morph_pre (phi : 'CF(f @* H)) :
+  H <| G → G \subset D → 'I_G[cfMorph phi] = G :&: f @*^-1 'I_(f @* G)[phi].

-Lemma inertia_morph_im (phi : 'CF(f @* H)) :
-  H <| G → G \subset D → f @* 'I_G[cfMorph phi] = 'I_(f @* G)[phi].
+Lemma inertia_morph_im (phi : 'CF(f @* H)) :
+  H <| G → G \subset D → f @* 'I_G[cfMorph phi] = 'I_(f @* G)[phi].

-Variables (R S : {group rT}).
-Variables (g : {morphism G >-> rT}) (h : {morphism H >-> rT}).
+Variables (R S : {group rT}).
+Variables (g : {morphism G >-> rT}) (h : {morphism H >-> rT}).
Hypotheses (isoG : isom G R g) (isoH : isom H S h).
-Hypotheses (eq_hg : {in H, h =1 g}) (sHG : H \subset G).
+Hypotheses (eq_hg : {in H, h =1 g}) (sHG : H \subset G).

@@ -538,10 +537,10 @@
Lemma cfConjgIsom phi y :
-  y \in G → y \in 'N(H) → (cfIsom isoH phi ^ g y)%CF = cfIsom isoH (phi ^ y).
+  y \in G → y \in 'N(H) → (cfIsom isoH phi ^ g y)%CF = cfIsom isoH (phi ^ y).

-Lemma inertia_isom phi : 'I_R[cfIsom isoH phi] = g @* 'I_G[phi].
+Lemma inertia_isom phi : 'I_R[cfIsom isoH phi] = g @* 'I_G[phi].

End ConjMorph.
@@ -551,38 +550,38 @@
Variables gT : finGroupType.
-Implicit Types G H K : {group gT}.
+Implicit Types G H K : {group gT}.

-Lemma cfConjgMod_norm H K (phi : 'CF(H / K)) y :
-  y \in 'N(K) → y \in 'N(H) → ((phi %% K) ^ y)%CF = (phi ^ coset K y %% K)%CF.
+Lemma cfConjgMod_norm H K (phi : 'CF(H / K)) y :
+  y \in 'N(K) → y \in 'N(H) → ((phi %% K) ^ y)%CF = (phi ^ coset K y %% K)%CF.

-Lemma cfConjgMod G H K (phi : 'CF(H / K)) y :
-    H <| G → K <| G → y \in G →
-  ((phi %% K) ^ y)%CF = (phi ^ coset K y %% K)%CF.
+Lemma cfConjgMod G H K (phi : 'CF(H / K)) y :
+    H <| G → K <| G → y \in G →
+  ((phi %% K) ^ y)%CF = (phi ^ coset K y %% K)%CF.

-Lemma cfConjgQuo_norm H K (phi : 'CF(H)) y :
-  y \in 'N(K) → y \in 'N(H) → ((phi / K) ^ coset K y)%CF = (phi ^ y / K)%CF.
+Lemma cfConjgQuo_norm H K (phi : 'CF(H)) y :
+  y \in 'N(K) → y \in 'N(H) → ((phi / K) ^ coset K y)%CF = (phi ^ y / K)%CF.

-Lemma cfConjgQuo G H K (phi : 'CF(H)) y :
-    H <| G → K <| G → y \in G →
-  ((phi / K) ^ coset K y)%CF = (phi ^ y / K)%CF.
+Lemma cfConjgQuo G H K (phi : 'CF(H)) y :
+    H <| G → K <| G → y \in G →
+  ((phi / K) ^ coset K y)%CF = (phi ^ y / K)%CF.

-Lemma inertia_mod_pre G H K (phi : 'CF(H / K)) :
-  H <| G → K <| G → 'I_G[phi %% K] = G :&: coset K @*^-1 'I_(G / K)[phi].
+Lemma inertia_mod_pre G H K (phi : 'CF(H / K)) :
+  H <| G → K <| G → 'I_G[phi %% K] = G :&: coset K @*^-1 'I_(G / K)[phi].

-Lemma inertia_mod_quo G H K (phi : 'CF(H / K)) :
-  H <| G → K <| G → ('I_G[phi %% K] / K)%g = 'I_(G / K)[phi].
+Lemma inertia_mod_quo G H K (phi : 'CF(H / K)) :
+  H <| G → K <| G → ('I_G[phi %% K] / K)%g = 'I_(G / K)[phi].

-Lemma inertia_quo G H K (phi : 'CF(H)) :
-    H <| G → K <| G → K \subset cfker phi →
-  'I_(G / K)[phi / K] = ('I_G[phi] / K)%g.
+Lemma inertia_quo G H K (phi : 'CF(H)) :
+    H <| G → K <| G → K \subset cfker phi →
+  'I_(G / K)[phi / K] = ('I_G[phi] / K)%g.

End ConjQuotient.
@@ -591,19 +590,19 @@ Section InertiaSdprod.

-Variables (gT : finGroupType) (K H G : {group gT}).
+Variables (gT : finGroupType) (K H G : {group gT}).

-Hypothesis defG : K ><| H = G.
+Hypothesis defG : K ><| H = G.

Lemma cfConjgSdprod phi y :
-    y \in 'N(K) → y \in 'N(H) →
-  (cfSdprod defG phi ^ y = cfSdprod defG (phi ^ y))%CF.
+    y \in 'N(K) → y \in 'N(H) →
+  (cfSdprod defG phi ^ y = cfSdprod defG (phi ^ y))%CF.

-Lemma inertia_sdprod (L : {group gT}) phi :
-  L \subset 'N(K) → L \subset 'N(H) → 'I_L[cfSdprod defG phi] = 'I_L[phi].
+Lemma inertia_sdprod (L : {group gT}) phi :
+  L \subset 'N(K) → L \subset 'N(H) → 'I_L[cfSdprod defG phi] = 'I_L[phi].

End InertiaSdprod.
@@ -612,42 +611,42 @@ Section InertiaDprod.

-Variables (gT : finGroupType) (G K H : {group gT}).
-Implicit Type L : {group gT}.
-Hypothesis KxH : K \x H = G.
+Variables (gT : finGroupType) (G K H : {group gT}).
+Implicit Type L : {group gT}.
+Hypothesis KxH : K \x H = G.

Lemma cfConjgDprodl phi y :
-    y \in 'N(K) → y \in 'N(H) →
-  (cfDprodl KxH phi ^ y = cfDprodl KxH (phi ^ y))%CF.
+    y \in 'N(K) → y \in 'N(H) →
+  (cfDprodl KxH phi ^ y = cfDprodl KxH (phi ^ y))%CF.

Lemma cfConjgDprodr psi y :
-    y \in 'N(K) → y \in 'N(H) →
-  (cfDprodr KxH psi ^ y = cfDprodr KxH (psi ^ y))%CF.
+    y \in 'N(K) → y \in 'N(H) →
+  (cfDprodr KxH psi ^ y = cfDprodr KxH (psi ^ y))%CF.

Lemma cfConjgDprod phi psi y :
-    y \in 'N(K) → y \in 'N(H) →
-  (cfDprod KxH phi psi ^ y = cfDprod KxH (phi ^ y) (psi ^ y))%CF.
+    y \in 'N(K) → y \in 'N(H) →
+  (cfDprod KxH phi psi ^ y = cfDprod KxH (phi ^ y) (psi ^ y))%CF.

Lemma inertia_dprodl L phi :
-  L \subset 'N(K) → L \subset 'N(H) → 'I_L[cfDprodl KxH phi] = 'I_L[phi].
+  L \subset 'N(K) → L \subset 'N(H) → 'I_L[cfDprodl KxH phi] = 'I_L[phi].

Lemma inertia_dprodr L psi :
-  L \subset 'N(K) → L \subset 'N(H) → 'I_L[cfDprodr KxH psi] = 'I_L[psi].
+  L \subset 'N(K) → L \subset 'N(H) → 'I_L[cfDprodr KxH psi] = 'I_L[psi].

-Lemma inertia_dprod L (phi : 'CF(K)) (psi : 'CF(H)) :
-    L \subset 'N(K) → L \subset 'N(H) → phi 1%g != 0 → psi 1%g != 0 →
-  'I_L[cfDprod KxH phi psi] = 'I_L[phi] :&: 'I_L[psi].
+Lemma inertia_dprod L (phi : 'CF(K)) (psi : 'CF(H)) :
+    L \subset 'N(K) → L \subset 'N(H) → phi 1%g != 0 → psi 1%g != 0 →
+  'I_L[cfDprod KxH phi psi] = 'I_L[phi] :&: 'I_L[psi].

Lemma inertia_dprod_irr L i j :
-    L \subset 'N(K) → L \subset 'N(H) →
-  'I_L[cfDprod KxH 'chi_i 'chi_j] = 'I_L['chi_i] :&: 'I_L['chi_j].
+    L \subset 'N(K) → L \subset 'N(H) →
+  'I_L[cfDprod KxH 'chi_i 'chi_j] = 'I_L['chi_i] :&: 'I_L['chi_j].

End InertiaDprod.
@@ -656,25 +655,25 @@ Section InertiaBigdprod.

-Variables (gT : finGroupType) (I : finType) (P : pred I).
-Variables (A : I → {group gT}) (G : {group gT}).
-Implicit Type L : {group gT}.
-Hypothesis defG : \big[dprod/1%g]_(i | P i) A i = G.
+Variables (gT : finGroupType) (I : finType) (P : pred I).
+Variables (A : I → {group gT}) (G : {group gT}).
+Implicit Type L : {group gT}.
+Hypothesis defG : \big[dprod/1%g]_(i | P i) A i = G.

Section ConjBig.

Variable y : gT.
-Hypothesis nAy: ∀ i, P i → y \in 'N(A i).
+Hypothesis nAy: ∀ i, P i → y \in 'N(A i).

-Lemma cfConjgBigdprodi i (phi : 'CF(A i)) :
-   (cfBigdprodi defG phi ^ y = cfBigdprodi defG (phi ^ y))%CF.
+Lemma cfConjgBigdprodi i (phi : 'CF(A i)) :
+   (cfBigdprodi defG phi ^ y = cfBigdprodi defG (phi ^ y))%CF.

Lemma cfConjgBigdprod phi :
-  (cfBigdprod defG phi ^ y = cfBigdprod defG (fun i ⇒ phi i ^ y))%CF.
+  (cfBigdprod defG phi ^ y = cfBigdprod defG (fun i ⇒ phi i ^ y))%CF.

End ConjBig.
@@ -683,20 +682,20 @@ Section InertiaBig.

-Variable L : {group gT}.
-Hypothesis nAL : ∀ i, P i → L \subset 'N(A i).
+Variable L : {group gT}.
+Hypothesis nAL : ∀ i, P i → L \subset 'N(A i).

-Lemma inertia_bigdprodi i (phi : 'CF(A i)) :
-  P i → 'I_L[cfBigdprodi defG phi] = 'I_L[phi].
+Lemma inertia_bigdprodi i (phi : 'CF(A i)) :
+  P i → 'I_L[cfBigdprodi defG phi] = 'I_L[phi].

Lemma inertia_bigdprod phi (Phi := cfBigdprod defG phi) :
-  Phi 1%g != 0 → 'I_L[Phi] = L :&: \bigcap_(i | P i) 'I_L[phi i].
+  Phi 1%g != 0 → 'I_L[Phi] = L :&: \bigcap_(i | P i) 'I_L[phi i].

-Lemma inertia_bigdprod_irr Iphi (phi := fun i ⇒ 'chi_(Iphi i)) :
-  'I_L[cfBigdprod defG phi] = L :&: \bigcap_(i | P i) 'I_L[phi i].
+Lemma inertia_bigdprod_irr Iphi (phi := fun i ⇒ 'chi_(Iphi i)) :
+  'I_L[cfBigdprod defG phi] = L :&: \bigcap_(i | P i) 'I_L[phi i].

End InertiaBig.
@@ -708,14 +707,14 @@ Section ConsttInertiaBijection.

-Variables (gT : finGroupType) (H G : {group gT}) (t : Iirr H).
-Hypothesis nsHG : H <| G.
+Variables (gT : finGroupType) (H G : {group gT}) (t : Iirr H).
+Hypothesis nsHG : H <| G.


-Let calA := irr_constt ('Ind[T] theta).
-Let calB := irr_constt ('Ind[G] theta).
+Let calA := irr_constt ('Ind[T] theta).
+Let calB := irr_constt ('Ind[G] theta).

@@ -725,13 +724,13 @@
Theorem constt_Inertia_bijection :
- [/\ (*a*) {in calA, ∀ s, 'Ind[G] 'chi_s \in irr G},
-     (*b*) {in calA &, injective (Ind_Iirr G)},
-           Ind_Iirr G @: calA =i calB,
-     (*c*) {in calA, ∀ s (psi := 'chi_s) (chi := 'Ind[G] psi),
-             [predI irr_constt ('Res chi) & calA] =i pred1 s}
-   & (*d*) {in calA, ∀ s (psi := 'chi_s) (chi := 'Ind[G] psi),
-             '['Res psi, theta] = '['Res chi, theta]}].
+ [/\ (*a*) {in calA, ∀ s, 'Ind[G] 'chi_s \in irr G},
+     (*b*) {in calA &, injective (Ind_Iirr G)},
+           Ind_Iirr G @: calA =i calB,
+     (*c*) {in calA, ∀ s (psi := 'chi_s) (chi := 'Ind[G] psi),
+             [predI irr_constt ('Res chi) & calA] =i pred1 s}
+   & (*d*) {in calA, ∀ s (psi := 'chi_s) (chi := 'Ind[G] psi),
+             '['Res psi, theta] = '['Res chi, theta]}].

End ConsttInertiaBijection.
@@ -741,27 +740,27 @@
Variable gT : finGroupType.
-Implicit Types G H K L M N : {group gT}.
+Implicit Types G H K L M N : {group gT}.

Section ConsttIndExtendible.

-Variables (G N : {group gT}) (t : Iirr N) (c : Iirr G).
-Let theta := 'chi_t.
-Let chi := 'chi_c.
+Variables (G N : {group gT}) (t : Iirr N) (c : Iirr G).
+Let theta := 'chi_t.
+Let chi := 'chi_c.

-Definition mul_Iirr b := cfIirr ('chi_b × chi).
-Definition mul_mod_Iirr (b : Iirr (G / N)) := mul_Iirr (mod_Iirr b).
+Definition mul_Iirr b := cfIirr ('chi_b × chi).
+Definition mul_mod_Iirr (b : Iirr (G / N)) := mul_Iirr (mod_Iirr b).

-Hypotheses (nsNG : N <| G) (cNt : 'Res[N] chi = theta).
-Let sNG : N \subset G.
-Let nNG : G \subset 'N(N).
+Hypotheses (nsNG : N <| G) (cNt : 'Res[N] chi = theta).
+Let sNG : N \subset G.
+Let nNG : G \subset 'N(N).

-Lemma extendible_irr_invariant : G \subset 'I[theta].
+Lemma extendible_irr_invariant : G \subset 'I[theta].
Let IGtheta := extendible_irr_invariant.

@@ -771,13 +770,13 @@ This is Isaacs, Theorem (6.16)
-Theorem constt_Ind_mul_ext f (phi := 'chi_f) (psi := phi × theta) :
-  G \subset 'I[phi] → psi \in irr N →
-  let calS := irr_constt ('Ind phi) in
-  [/\ {in calS, ∀ b, 'chi_b × chi \in irr G},
-      {in calS &, injective mul_Iirr},
-      irr_constt ('Ind psi) =i [seq mul_Iirr b | b in calS]
-    & 'Ind psi = \sum_(b in calS) '['Ind phi, 'chi_b] *: 'chi_(mul_Iirr b)].
+Theorem constt_Ind_mul_ext f (phi := 'chi_f) (psi := phi × theta) :
+  G \subset 'I[phi] → psi \in irr N →
+  let calS := irr_constt ('Ind phi) in
+  [/\ {in calS, ∀ b, 'chi_b × chi \in irr G},
+      {in calS &, injective mul_Iirr},
+      irr_constt ('Ind psi) =i [seq mul_Iirr b | b in calS]
+    & 'Ind psi = \sum_(b in calS) '['Ind phi, 'chi_b] *: 'chi_(mul_Iirr b)].

@@ -787,10 +786,10 @@
Corollary constt_Ind_ext :
-  [/\ ∀ b : Iirr (G / N), 'chi_(mod_Iirr b) × chi \in irr G,
-      injective mul_mod_Iirr,
-      irr_constt ('Ind theta) =i codom mul_mod_Iirr
-    & 'Ind theta = \sum_b 'chi_b 1%g *: 'chi_(mul_mod_Iirr b)].
+  [/\ ∀ b : Iirr (G / N), 'chi_(mod_Iirr b) × chi \in irr G,
+      injective mul_mod_Iirr,
+      irr_constt ('Ind theta) =i codom mul_mod_Iirr
+    & 'Ind theta = \sum_b 'chi_b 1%g *: 'chi_(mul_mod_Iirr b)].

End ConsttIndExtendible.
@@ -802,12 +801,12 @@ This is Isaacs, Theorem (6.19).
-Theorem invariant_chief_irr_cases G K L s (theta := 'chi[K]_s) :
-    chief_factor G L K → abelian (K / L) → G \subset 'I[theta] →
-  let t := #|K : L| in
-  [\/ 'Res[L] theta \in irr L,
-      exists2 e, ∃ p, 'Res[L] theta = e%:R *: 'chi_p & (e ^ 2)%N = t
-   | exists2 p, injective p & 'Res[L] theta = \sum_(i < t) 'chi_(p i)].
+Theorem invariant_chief_irr_cases G K L s (theta := 'chi[K]_s) :
+    chief_factor G L K → abelian (K / L) → G \subset 'I[theta] →
+  let t := #|K : L| in
+  [\/ 'Res[L] theta \in irr L,
+      exists2 e, ∃ p, 'Res[L] theta = e%:R *: 'chi_p & (e ^ 2)%N = t
+   | exists2 p, injective p & 'Res[L] theta = \sum_(i < t) 'chi_(p i)].

@@ -816,10 +815,10 @@ This is Isaacs, Corollary (6.19).
-Corollary cfRes_prime_irr_cases G N s p (chi := 'chi[G]_s) :
-    N <| G → #|G : N| = p → prime p →
-  [\/ 'Res[N] chi \in irr N
-   | exists2 c, injective c & 'Res[N] chi = \sum_(i < p) 'chi_(c i)].
+Corollary cfRes_prime_irr_cases G N s p (chi := 'chi[G]_s) :
+    N <| G → #|G : N| = p → prime p →
+  [\/ 'Res[N] chi \in irr N
+   | exists2 c, injective c & 'Res[N] chi = \sum_(i < p) 'chi_(c i)].

@@ -829,8 +828,8 @@
Corollary prime_invariant_irr_extendible G N s p :
-    N <| G → #|G : N| = p → prime p → G \subset 'I['chi_s] →
-  {t | 'Res[N, G] 'chi_t = 'chi_s}.
+    N <| G → #|G : N| = p → prime p → G \subset 'I['chi_s] →
+  {t | 'Res[N, G] 'chi_t = 'chi_s}.

@@ -840,11 +839,11 @@
Lemma extend_to_cfdet G N s c0 u :
-    let theta := 'chi_s in let lambda := cfDet theta in let mu := 'chi_u in
-    N <| G → coprime #|G : N| (truncC (theta 1%g)) →
-    'Res[N, G] 'chi_c0 = theta → 'Res[N, G] mu = lambda →
-  exists2 c, 'Res 'chi_c = theta ∧ cfDet 'chi_c = mu
-          & ∀ c1, 'Res 'chi_c1 = theta → cfDet 'chi_c1 = mu → c1 = c.
+    let theta := 'chi_s in let lambda := cfDet theta in let mu := 'chi_u in
+    N <| G → coprime #|G : N| (truncC (theta 1%g)) →
+    'Res[N, G] 'chi_c0 = theta → 'Res[N, G] mu = lambda →
+  exists2 c, 'Res 'chi_c = theta ∧ cfDet 'chi_c = mu
+          & ∀ c1, 'Res 'chi_c1 = theta → cfDet 'chi_c1 = mu → c1 = c.

@@ -853,11 +852,11 @@ This is Isaacs, Theorem (6.25).
-Theorem solvable_irr_extendible_from_det G N s (theta := 'chi[N]_s) :
-    N <| G → solvable (G / N) →
-    G \subset 'I[theta] → coprime #|G : N| (truncC (theta 1%g)) →
-  [∃ c, 'Res 'chi[G]_c == theta]
-    = [∃ u, 'Res 'chi[G]_u == cfDet theta].
+Theorem solvable_irr_extendible_from_det G N s (theta := 'chi[N]_s) :
+    N <| G → solvable (G / N) →
+    G \subset 'I[theta] → coprime #|G : N| (truncC (theta 1%g)) →
+  [∃ c, 'Res 'chi[G]_c == theta]
+    = [∃ u, 'Res 'chi[G]_u == cfDet theta].

@@ -866,13 +865,13 @@ This is Isaacs, Theorem (6.26).
-Theorem extend_linear_char_from_Sylow G N (lambda : 'CF(N)) :
-    N <| G → lambda \is a linear_char → G \subset 'I[lambda] →
-    (∀ p, p \in \pi('o(lambda)%CF) →
-       exists2 Hp : {group gT},
-         [/\ N \subset Hp, Hp \subset G & p.-Sylow(G / N) (Hp / N)%g]
-       & ∃ u, 'Res 'chi[Hp]_u = lambda) →
-  ∃ u, 'Res[N, G] 'chi_u = lambda.
+Theorem extend_linear_char_from_Sylow G N (lambda : 'CF(N)) :
+    N <| G → lambda \is a linear_char → G \subset 'I[lambda] →
+    (∀ p, p \in \pi('o(lambda)%CF) →
+       exists2 Hp : {group gT},
+         [/\ N \subset Hp, Hp \subset G & p.-Sylow(G / N) (Hp / N)%g]
+       & ∃ u, 'Res 'chi[Hp]_u = lambda) →
+  ∃ u, 'Res[N, G] 'chi_u = lambda.

@@ -881,13 +880,13 @@ This is Isaacs, Corollary (6.27).
-Corollary extend_coprime_linear_char G N (lambda : 'CF(N)) :
-    N <| G → lambda \is a linear_char → G \subset 'I[lambda] →
-    coprime #|G : N| 'o(lambda)%CF →
-  ∃ u, [/\ 'Res 'chi[G]_u = lambda, 'o('chi_u)%CF = 'o(lambda)%CF
-              & ∀ v,
-                  'Res 'chi_v = lambda → coprime #|G : N| 'o('chi_v)%CF →
-                v = u].
+Corollary extend_coprime_linear_char G N (lambda : 'CF(N)) :
+    N <| G → lambda \is a linear_char → G \subset 'I[lambda] →
+    coprime #|G : N| 'o(lambda)%CF →
+  ∃ u, [/\ 'Res 'chi[G]_u = lambda, 'o('chi_u)%CF = 'o(lambda)%CF
+              & ∀ v,
+                  'Res 'chi_v = lambda → coprime #|G : N| 'o('chi_v)%CF →
+                v = u].

@@ -896,13 +895,13 @@ This is Isaacs, Corollary (6.28).
-Corollary extend_solvable_coprime_irr G N t (theta := 'chi[N]_t) :
-    N <| G → solvable (G / N) → G \subset 'I[theta] →
-    coprime #|G : N| ('o(theta)%CF × truncC (theta 1%g)) →
-  ∃ c, [/\ 'Res 'chi[G]_c = theta, 'o('chi_c)%CF = 'o(theta)%CF
-              & ∀ d,
-                  'Res 'chi_d = theta → coprime #|G : N| 'o('chi_d)%CF →
-                d = c].
+Corollary extend_solvable_coprime_irr G N t (theta := 'chi[N]_t) :
+    N <| G → solvable (G / N) → G \subset 'I[theta] →
+    coprime #|G : N| ('o(theta)%CF × truncC (theta 1%g)) →
+  ∃ c, [/\ 'Res 'chi[G]_c = theta, 'o('chi_c)%CF = 'o(theta)%CF
+              & ∀ d,
+                  'Res 'chi_d = theta → coprime #|G : N| 'o('chi_d)%CF →
+                d = c].

End ExtendInvariantIrr.
@@ -911,7 +910,7 @@ Section Frobenius.

-Variables (gT : finGroupType) (G K : {group gT}).
+Variables (gT : finGroupType) (G K : {group gT}).

@@ -921,7 +920,7 @@ state these theorems using the Frobenius property.
-Hypothesis frobGK : [Frobenius G with kernel K].
+Hypothesis frobGK : [Frobenius G with kernel K].

@@ -930,7 +929,7 @@ This is Isaacs, Theorem 6.34(a1).
-Theorem inertia_Frobenius_ker i : i != 0 → 'I_G['chi[K]_i] = K.
+Theorem inertia_Frobenius_ker i : i != 0 → 'I_G['chi[K]_i] = K.

@@ -939,7 +938,7 @@ This is Isaacs, Theorem 6.34(a2)
-Theorem irr_induced_Frobenius_ker i : i != 0 → 'Ind[G, K] 'chi_i \in irr G.
+Theorem irr_induced_Frobenius_ker i : i != 0 → 'Ind[G, K] 'chi_i \in irr G.

@@ -949,8 +948,8 @@
Theorem Frobenius_Ind_irrP j :
-  reflect (exists2 i, i != 0 & 'chi_j = 'Ind[G, K] 'chi_i)
-          (~~ (K \subset cfker 'chi_j)).
+  reflect (exists2 i, i != 0 & 'chi_j = 'Ind[G, K] 'chi_i)
+          (~~ (K \subset cfker 'chi_j)).

End Frobenius.
-- cgit v1.2.3