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.character.html | 1151 ++++++++++++------------ 1 file changed, 576 insertions(+), 575 deletions(-) (limited to 'docs/htmldoc/mathcomp.character.character.html') diff --git a/docs/htmldoc/mathcomp.character.character.html b/docs/htmldoc/mathcomp.character.character.html index b8cf2f4..54edc9e 100644 --- a/docs/htmldoc/mathcomp.character.character.html +++ b/docs/htmldoc/mathcomp.character.character.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.

@@ -110,77 +109,77 @@ Variable (F : fieldType).

-Fixpoint trow (n1 : nat) :
-  ∀ (A : 'rV[F]_n1) m2 n2 (B : 'M[F]_(m2,n2)), 'M[F]_(m2,n1 × n2) :=
-  if n1 is n'1.+1
+Fixpoint trow (n1 : nat) :
+  ∀ (A : 'rV[F]_n1) m2 n2 (B : 'M[F]_(m2,n2)), 'M[F]_(m2,n1 × n2) :=
+  if n1 is n'1.+1
  then
-    fun (A : 'M[F]_(1,(1 + n'1))) m2 n2 (B : 'M[F]_(m2,n2)) ⇒
-       (row_mx (lsubmx A 0 0 *: B) (trow (rsubmx A) B))
+    fun (A : 'M[F]_(1,(1 + n'1))) m2 n2 (B : 'M[F]_(m2,n2)) ⇒
+       (row_mx (lsubmx A 0 0 *: B) (trow (rsubmx A) B))
   else (fun _ _ _ _ ⇒ 0).

-Lemma trow0 n1 m2 n2 B : @trow n1 0 m2 n2 B = 0.
+Lemma trow0 n1 m2 n2 B : @trow n1 0 m2 n2 B = 0.

Definition trowb n1 m2 n2 B A := @trow n1 A m2 n2 B.

-Lemma trowbE n1 m2 n2 A B : trowb B A = @trow n1 A m2 n2 B.
+Lemma trowbE n1 m2 n2 A B : trowb B A = @trow n1 A m2 n2 B.

-Lemma trowb_is_linear n1 m2 n2 (B : 'M_(m2,n2)) : linear (@trowb n1 m2 n2 B).
+Lemma trowb_is_linear n1 m2 n2 (B : 'M_(m2,n2)) : linear (@trowb n1 m2 n2 B).

Canonical Structure trowb_linear n1 m2 n2 B :=
  Linear (@trowb_is_linear n1 m2 n2 B).

-Lemma trow_is_linear n1 m2 n2 (A : 'rV_n1) : linear (@trow n1 A m2 n2).
+Lemma trow_is_linear n1 m2 n2 (A : 'rV_n1) : linear (@trow n1 A m2 n2).

Canonical Structure trow_linear n1 m2 n2 A :=
  Linear (@trow_is_linear n1 m2 n2 A).

-Fixpoint tprod (m1 : nat) :
-  ∀ n1 (A : 'M[F]_(m1,n1)) m2 n2 (B : 'M[F]_(m2,n2)),
-        'M[F]_(m1 × m2,n1 × n2) :=
-  if m1 is m'1.+1
-    return ∀ n1 (A : 'M[F]_(m1,n1)) m2 n2 (B : 'M[F]_(m2,n2)),
-           'M[F]_(m1 × m2,n1 × n2)
+Fixpoint tprod (m1 : nat) :
+  ∀ n1 (A : 'M[F]_(m1,n1)) m2 n2 (B : 'M[F]_(m2,n2)),
+        'M[F]_(m1 × m2,n1 × n2) :=
+  if m1 is m'1.+1
+    return ∀ n1 (A : 'M[F]_(m1,n1)) m2 n2 (B : 'M[F]_(m2,n2)),
+           'M[F]_(m1 × m2,n1 × n2)
  then
-    fun n1 (A : 'M[F]_(1 + m'1,n1)) m2 n2 B ⇒
+    fun n1 (A : 'M[F]_(1 + m'1,n1)) m2 n2 B ⇒
        (col_mx (trow (usubmx A) B) (tprod (dsubmx A) B))
   else (fun _ _ _ _ _ ⇒ 0).

Lemma dsumx_mul m1 m2 n p A B :
-  dsubmx ((A ×m B) : 'M[F]_(m1 + m2, n)) = dsubmx (A : 'M_(m1 + m2, p)) ×m B.
+  dsubmx ((A ×m B) : 'M[F]_(m1 + m2, n)) = dsubmx (A : 'M_(m1 + m2, p)) ×m B.

Lemma usumx_mul m1 m2 n p A B :
-  usubmx ((A ×m B) : 'M[F]_(m1 + m2, n)) = usubmx (A : 'M_(m1 + m2, p)) ×m B.
+  usubmx ((A ×m B) : 'M[F]_(m1 + m2, n)) = usubmx (A : 'M_(m1 + m2, p)) ×m B.

-Let trow_mul (m1 m2 n2 p2 : nat)
-         (A : 'rV_m1) (B1: 'M[F]_(m2,n2)) (B2 :'M[F]_(n2,p2)) :
-  trow A (B1 ×m B2) = B1 ×m trow A B2.
+Let trow_mul (m1 m2 n2 p2 : nat)
+         (A : 'rV_m1) (B1: 'M[F]_(m2,n2)) (B2 :'M[F]_(n2,p2)) :
+  trow A (B1 ×m B2) = B1 ×m trow A B2.

-Lemma tprodE m1 n1 p1 (A1 :'M[F]_(m1,n1)) (A2 :'M[F]_(n1,p1))
-             m2 n2 p2 (B1 :'M[F]_(m2,n2)) (B2 :'M[F]_(n2,p2)) :
-  tprod (A1 ×m A2) (B1 ×m B2) = (tprod A1 B1) ×m (tprod A2 B2).
+Lemma tprodE m1 n1 p1 (A1 :'M[F]_(m1,n1)) (A2 :'M[F]_(n1,p1))
+             m2 n2 p2 (B1 :'M[F]_(m2,n2)) (B2 :'M[F]_(n2,p2)) :
+  tprod (A1 ×m A2) (B1 ×m B2) = (tprod A1 B1) ×m (tprod A2 B2).

-Let tprod_tr m1 n1 (A :'M[F]_(m1, 1 + n1)) m2 n2 (B :'M[F]_(m2, n2)) :
-  tprod A B = row_mx (trow (lsubmx A)^T B^T)^T (tprod (rsubmx A) B).
+Let tprod_tr m1 n1 (A :'M[F]_(m1, 1 + n1)) m2 n2 (B :'M[F]_(m2, n2)) :
+  tprod A B = row_mx (trow (lsubmx A)^T B^T)^T (tprod (rsubmx A) B).

-Lemma tprod1 m n : tprod (1%:M : 'M[F]_(m,m)) (1%:M : 'M[F]_(n,n)) = 1%:M.
+Lemma tprod1 m n : tprod (1%:M : 'M[F]_(m,m)) (1%:M : 'M[F]_(n,n)) = 1%:M.

-Lemma mxtrace_prod m n (A :'M[F]_(m)) (B :'M[F]_(n)) :
-  \tr (tprod A B) = \tr A × \tr B.
+Lemma mxtrace_prod m n (A :'M[F]_(m)) (B :'M[F]_(n)) :
+  \tr (tprod A B) = \tr A × \tr B.

End Tensor.
@@ -195,14 +194,14 @@ Section StandardRepresentation.

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

Record representation :=
  Representation {rdegree; mx_repr_of_repr :> reprG rdegree}.

-Lemma mx_repr0 : mx_repr G (fun _ : gT ⇒ 1%:M : 'M[R]_0).
+Lemma mx_repr0 : mx_repr G (fun _ : gT ⇒ 1%:M : 'M[R]_0).

Definition grepr0 := Representation (MxRepresentation mx_repr0).
@@ -219,29 +218,29 @@ Section DsumRepr.

-Variables (n : nat) (rG : reprG n).
+Variables (n : nat) (rG : reprG n).

-Lemma mx_rsim_dadd (U V W : 'M_n) (rU rV : representation)
+Lemma mx_rsim_dadd (U V W : 'M_n) (rU rV : representation)
    (modU : mxmodule rG U) (modV : mxmodule rG V) (modW : mxmodule rG W) :
-    (U + V :=: W)%MS → mxdirect (U + V) →
-    mx_rsim (submod_repr modU) rU → mx_rsim (submod_repr modV) rV →
+    (U + V :=: W)%MS → mxdirect (U + V) →
+    mx_rsim (submod_repr modU) rU → mx_rsim (submod_repr modV) rV →
  mx_rsim (submod_repr modW) (dadd_grepr rU rV).

-Lemma mx_rsim_dsum (I : finType) (P : pred I) U rU (W : 'M_n)
+Lemma mx_rsim_dsum (I : finType) (P : pred I) U rU (W : 'M_n)
    (modU : ∀ i, mxmodule rG (U i)) (modW : mxmodule rG W) :
-    let S := (\sum_(i | P i) U i)%MS in (S :=: W)%MS → mxdirect S →
-    (∀ i, mx_rsim (submod_repr (modU i)) (rU i : representation)) →
-  mx_rsim (submod_repr modW) (\big[dadd_grepr/grepr0]_(i | P i) rU i).
+    let S := (\sum_(i | P i) U i)%MS in (S :=: W)%MS → mxdirect S →
+    (∀ i, mx_rsim (submod_repr (modU i)) (rU i : representation)) →
+  mx_rsim (submod_repr modW) (\big[dadd_grepr/grepr0]_(i | P i) rU i).

-Definition muln_grepr rW k := \big[dadd_grepr/grepr0]_(i < k) rW.
+Definition muln_grepr rW k := \big[dadd_grepr/grepr0]_(i < k) rW.

Lemma mx_rsim_socle (sG : socleType rG) (W : sG) (rW : representation) :
    let modW : mxmodule rG W := component_mx_module rG (socle_base W) in
-    mx_rsim (socle_repr W) rW →
+    mx_rsim (socle_repr W) rW →
  mx_rsim (submod_repr modW) (muln_grepr rW (socle_mult W)).

@@ -251,7 +250,7 @@ Section ProdRepr.

-Variables (n1 n2 : nat) (rG1 : reprG n1) (rG2 : reprG n2).
+Variables (n1 n2 : nat) (rG1 : reprG n1) (rG2 : reprG n2).

Lemma prod_mx_repr : mx_repr G (fun g ⇒ tprod (rG1 g) (rG2 g)).
@@ -264,8 +263,8 @@
Lemma prod_repr_lin n2 (rG1 : reprG 1) (rG2 : reprG n2) :
-  {in G, ∀ x, let cast_n2 := esym (mul1n n2) in
-      prod_repr rG1 rG2 x = castmx (cast_n2, cast_n2) (rG1 x 0 0 *: rG2 x)}.
+  {in G, ∀ x, let cast_n2 := esym (mul1n n2) in
+      prod_repr rG1 rG2 x = castmx (cast_n2, cast_n2) (rG1 x 0 0 *: rG2 x)}.

End StandardRepresentation.
@@ -276,40 +275,40 @@ Section Char.

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

Fact cfRepr_subproof n (rG : mx_representation algCF G n) :
-  is_class_fun <<G>> [ffun x ⇒ \tr (rG x) *+ (x \in G)].
+  is_class_fun <<G>> [ffun x ⇒ \tr (rG x) *+ (x \in G)].
Definition cfRepr n rG := Cfun 0 (@cfRepr_subproof n rG).

-Lemma cfRepr1 n rG : @cfRepr n rG 1%g = n%:R.
+Lemma cfRepr1 n rG : @cfRepr n rG 1%g = n%:R.

Lemma cfRepr_sim n1 n2 rG1 rG2 :
-  mx_rsim rG1 rG2 → @cfRepr n1 rG1 = @cfRepr n2 rG2.
+  mx_rsim rG1 rG2 → @cfRepr n1 rG1 = @cfRepr n2 rG2.

-Lemma cfRepr0 : cfRepr grepr0 = 0.
+Lemma cfRepr0 : cfRepr grepr0 = 0.

Lemma cfRepr_dadd rG1 rG2 :
-  cfRepr (dadd_grepr rG1 rG2) = cfRepr rG1 + cfRepr rG2.
+  cfRepr (dadd_grepr rG1 rG2) = cfRepr rG1 + cfRepr rG2.

-Lemma cfRepr_dsum I r (P : pred I) rG :
-  cfRepr (\big[dadd_grepr/grepr0]_(i <- r | P i) rG i)
-    = \sum_(i <- r | P i) cfRepr (rG i).
+Lemma cfRepr_dsum I r (P : pred I) rG :
+  cfRepr (\big[dadd_grepr/grepr0]_(i <- r | P i) rG i)
+    = \sum_(i <- r | P i) cfRepr (rG i).

-Lemma cfRepr_muln rG k : cfRepr (muln_grepr rG k) = cfRepr rG *+ k.
+Lemma cfRepr_muln rG k : cfRepr (muln_grepr rG k) = cfRepr rG *+ k.

Section StandardRepr.

-Variables (n : nat) (rG : mx_representation algCF G n).
+Variables (n : nat) (rG : mx_representation algCF G n).
Let sG := DecSocleType rG.
Let iG : irrType algCF G := DecSocleType _.
@@ -317,14 +316,14 @@ Definition standard_irr (W : sG) := irr_comp iG (socle_repr W).

-Definition standard_socle i := pick [pred W | standard_irr W == i].
+Definition standard_socle i := pick [pred W | standard_irr W == i].

-Definition standard_irr_coef i := oapp (fun W ⇒ socle_mult W) 0%N (soc i).
+Definition standard_irr_coef i := oapp (fun W ⇒ socle_mult W) 0%N (soc i).

Definition standard_grepr :=
-  \big[dadd_grepr/grepr0]_i
+  \big[dadd_grepr/grepr0]_i
     muln_grepr (Representation (socle_repr i)) (standard_irr_coef i).

@@ -334,10 +333,10 @@ End StandardRepr.

-Definition cfReg (B : {set gT}) : 'CF(B) := #|B|%:R *: '1_[1].
+Definition cfReg (B : {set gT}) : 'CF(B) := #|B|%:R *: '1_[1].

-Lemma cfRegE x : @cfReg G x = #|G|%:R *+ (x == 1%g).
+Lemma cfRegE x : @cfReg G x = #|G|%:R *+ (x == 1%g).

@@ -346,18 +345,18 @@ This is Isaacs, Lemma (2.10).
-Lemma cfReprReg : cfRepr (regular_repr algCF G) = cfReg G.
+Lemma cfReprReg : cfRepr (regular_repr algCF G) = cfReg G.

-Definition xcfun (chi : 'CF(G)) A :=
-  (gring_row A ×m (\col_(i < #|G|) chi (enum_val i))) 0 0.
+Definition xcfun (chi : 'CF(G)) A :=
+  (gring_row A ×m (\col_(i < #|G|) chi (enum_val i))) 0 0.

Lemma xcfun_is_additive phi : additive (xcfun phi).
Canonical xcfun_additive phi := Additive (xcfun_is_additive phi).

-Lemma xcfunZr a phi A : xcfun phi (a *: A) = a × xcfun phi A.
+Lemma xcfunZr a phi A : xcfun phi (a *: A) = a × xcfun phi A.

@@ -366,70 +365,70 @@ In order to add a second canonical structure on xcfun
-Definition xcfun_r_head k A phi := let: tt := k in xcfun phi A.
+Definition xcfun_r_head k A phi := let: tt := k in xcfun phi A.

-Lemma xcfun_rE A chi : xcfun_r A chi = xcfun chi A.
+Lemma xcfun_rE A chi : xcfun_r A chi = xcfun chi A.

Fact xcfun_r_is_additive A : additive (xcfun_r A).
Canonical xcfun_r_additive A := Additive (xcfun_r_is_additive A).

-Lemma xcfunZl a phi A : xcfun (a *: phi) A = a × xcfun phi A.
+Lemma xcfunZl a phi A : xcfun (a *: phi) A = a × xcfun phi A.

-Lemma xcfun_repr n rG A : xcfun (@cfRepr n rG) A = \tr (gring_op rG A).
+Lemma xcfun_repr n rG A : xcfun (@cfRepr n rG) A = \tr (gring_op rG A).

End Char.
-Notation xcfun_r A := (xcfun_r_head tt A).
-Notation "phi .[ A ]" := (xcfun phi A) : cfun_scope.
+Notation xcfun_r A := (xcfun_r_head tt A).
+Notation "phi .[ A ]" := (xcfun phi A) : cfun_scope.

-Definition pred_Nirr gT B := #|@classes gT B|.-1.
-Notation Nirr G := (pred_Nirr G).+1.
-Notation Iirr G := 'I_(Nirr G).
+Definition pred_Nirr gT B := #|@classes gT B|.-1.
+Notation Nirr G := (pred_Nirr G).+1.
+Notation Iirr G := 'I_(Nirr G).

Section IrrClassDef.

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

Let sG := DecSocleType (regular_repr algCF G).

-Lemma NirrE : Nirr G = #|classes G|.
+Lemma NirrE : Nirr G = #|classes G|.

-Fact Iirr_cast : Nirr G = #|sG|.
+Fact Iirr_cast : Nirr G = #|sG|.

-Let offset := cast_ord (esym Iirr_cast) (enum_rank [1 sG]%irr).
+Let offset := cast_ord (esym Iirr_cast) (enum_rank [1 sG]%irr).

Definition socle_of_Iirr (i : Iirr G) : sG :=
-  enum_val (cast_ord Iirr_cast (i + offset)).
+  enum_val (cast_ord Iirr_cast (i + offset)).
Definition irr_of_socle (Wi : sG) : Iirr G :=
-  cast_ord (esym Iirr_cast) (enum_rank Wi) - offset.
+  cast_ord (esym Iirr_cast) (enum_rank Wi) - offset.

-Lemma socle_Iirr0 : W 0 = [1 sG]%irr.
+Lemma socle_Iirr0 : W 0 = [1 sG]%irr.

-Lemma socle_of_IirrK : cancel W irr_of_socle.
+Lemma socle_of_IirrK : cancel W irr_of_socle.

-Lemma irr_of_socleK : cancel irr_of_socle W.
- Hint Resolve socle_of_IirrK irr_of_socleK.
+Lemma irr_of_socleK : cancel irr_of_socle W.
+ Hint Resolve socle_of_IirrK irr_of_socleK : core.

-Lemma irr_of_socle_bij (A : pred (Iirr G)) : {on A, bijective irr_of_socle}.
+Lemma irr_of_socle_bij (A : {pred (Iirr G)}) : {on A, bijective irr_of_socle}.

-Lemma socle_of_Iirr_bij (A : pred sG) : {on A, bijective W}.
+Lemma socle_of_Iirr_bij (A : {pred sG}) : {on A, bijective W}.

End IrrClassDef.
@@ -437,55 +436,55 @@

-Notation "''Chi_' i" := (irr_repr (socle_of_Iirr i))
+Notation "''Chi_' i" := (irr_repr (socle_of_Iirr i))
  (at level 8, i at level 2, format "''Chi_' i").

-Fact irr_key : unit.
-Definition irr_def gT B : (Nirr B).-tuple 'CF(B) :=
-   let irr_of i := 'Res[B, <<B>>] (@cfRepr gT _ _ 'Chi_(inord i)) in
-   [tuple of mkseq irr_of (Nirr B)].
-Definition irr := locked_with irr_key irr_def.
+Fact irr_key : unit.
+Definition irr_def gT B : (Nirr B).-tuple 'CF(B) :=
+   let irr_of i := 'Res[B, <<B>>] (@cfRepr gT _ _ 'Chi_(inord i)) in
+   [tuple of mkseq irr_of (Nirr B)].
+Definition irr := locked_with irr_key irr_def.


-Notation "''chi_' i" := (tnth (irr _) i%R)
+Notation "''chi_' i" := (tnth (irr _) i%R)
  (at level 8, i at level 2, format "''chi_' i") : ring_scope.
-Notation "''chi[' G ]_ i" := (tnth (irr G) i%R)
+Notation "''chi[' G ]_ i" := (tnth (irr G) i%R)
  (at level 8, i at level 2, only parsing) : ring_scope.

Section IrrClass.

-Variable (gT : finGroupType) (G : {group gT}).
-Implicit Types (i : Iirr G) (B : {set gT}).
+Variable (gT : finGroupType) (G : {group gT}).
+Implicit Types (i : Iirr G) (B : {set gT}).
Open Scope group_ring_scope.

-Lemma congr_irr i1 i2 : i1 = i2 → 'chi_i1 = 'chi_i2.
+Lemma congr_irr i1 i2 : i1 = i2 → 'chi_i1 = 'chi_i2.

-Lemma Iirr1_neq0 : G :!=: 1%g → inord 1 != 0 :> Iirr G.
+Lemma Iirr1_neq0 : G :!=: 1%g → inord 1 != 0 :> Iirr G.

-Lemma has_nonprincipal_irr : G :!=: 1%g → {i : Iirr G | i != 0}.
+Lemma has_nonprincipal_irr : G :!=: 1%g → {i : Iirr G | i != 0}.

-Lemma irrRepr i : cfRepr 'Chi_i = 'chi_i.
+Lemma irrRepr i : cfRepr 'Chi_i = 'chi_i.

-Lemma irr0 : 'chi[G]_0 = 1.
+Lemma irr0 : 'chi[G]_0 = 1.

-Lemma cfun1_irr : 1 \in irr G.
+Lemma cfun1_irr : 1 \in irr G.

-Lemma mem_irr i : 'chi_i \in irr G.
+Lemma mem_irr i : 'chi_i \in irr G.

-Lemma irrP xi : reflect (∃ i, xi = 'chi_i) (xi \in irr G).
+Lemma irrP xi : reflect (∃ i, xi = 'chi_i) (xi \in irr G).

Let sG := DecSocleType (regular_repr algCF G).
@@ -493,30 +492,32 @@ Let closG := @groupC _ G.

-Lemma irr1_degree i : 'chi_i 1%g = ('n_i)%:R.
+Lemma irr1_degree i : 'chi_i 1%g = ('n_i)%:R.

-Lemma Cnat_irr1 i : 'chi_i 1%g \in Cnat.
+Lemma Cnat_irr1 i : 'chi_i 1%g \in Cnat.

-Lemma irr1_gt0 i : 0 < 'chi_i 1%g.
+Lemma irr1_gt0 i : 0 < 'chi_i 1%g.

-Lemma irr1_neq0 i : 'chi_i 1%g != 0.
+Lemma irr1_neq0 i : 'chi_i 1%g != 0.

-Lemma irr_neq0 i : 'chi_i != 0.
+Lemma irr_neq0 i : 'chi_i != 0.

-Definition cfIirr B (chi : 'CF(B)) : Iirr B := inord (index chi (irr B)).
+
+Definition cfIirr : ∀ B, 'CF(B) → Iirr B :=
+  locked_with cfIirr_key (fun B chi ⇒ inord (index chi (irr B))).

-Lemma cfIirrE chi : chi \in irr G → 'chi_(cfIirr chi) = chi.
+Lemma cfIirrE chi : chi \in irr G → 'chi_(cfIirr chi) = chi.

-Lemma cfIirrPE J (f : J → 'CF(G)) (P : pred J) :
-    (∀ j, P j → f j \in irr G) →
-  ∀ j, P j → 'chi_(cfIirr (f j)) = f j.
+Lemma cfIirrPE J (f : J → 'CF(G)) (P : pred J) :
+    (∀ j, P j → f j \in irr G) →
+  ∀ j, P j → 'chi_(cfIirr (f j)) = f j.

@@ -525,7 +526,7 @@ This is Isaacs, Corollary (2.7).
-Corollary irr_sum_square : \sum_i ('chi[G]_i 1%g) ^+ 2 = #|G|%:R.
+Corollary irr_sum_square : \sum_i ('chi[G]_i 1%g) ^+ 2 = #|G|%:R.

@@ -534,45 +535,45 @@ This is Isaacs, Lemma (2.11).
-Lemma cfReg_sum : cfReg G = \sum_i 'chi_i 1%g *: 'chi_i.
+Lemma cfReg_sum : cfReg G = \sum_i 'chi_i 1%g *: 'chi_i.

Let aG := regular_repr algCF G.
Let R_G := group_ring algCF G.

-Lemma xcfun_annihilate i j A : i != j → (A \in 'R_j)%MS → ('chi_i).[A]%CF = 0.
+Lemma xcfun_annihilate i j A : i != j → (A \in 'R_j)%MS → ('chi_i).[A]%CF = 0.

-Lemma xcfunG phi x : x \in G → phi.[aG x]%CF = phi x.
+Lemma xcfunG phi x : x \in G → phi.[aG x]%CF = phi x.

Lemma xcfun_mul_id i A :
-  (A \in R_G)%MS → ('chi_i).['e_i ×m A]%CF = ('chi_i).[A]%CF.
+  (A \in R_G)%MS → ('chi_i).['e_i ×m A]%CF = ('chi_i).[A]%CF.

-Lemma xcfun_id i j : ('chi_i).['e_j]%CF = 'chi_i 1%g *+ (i == j).
+Lemma xcfun_id i j : ('chi_i).['e_j]%CF = 'chi_i 1%g *+ (i == j).

Lemma irr_free : free (irr G).

-Lemma irr_inj : injective (tnth (irr G)).
+Lemma irr_inj : injective (tnth (irr G)).

-Lemma irrK : cancel (tnth (irr G)) (@cfIirr G).
+Lemma irrK : cancel (tnth (irr G)) (@cfIirr G).

-Lemma irr_eq1 i : ('chi_i == 1) = (i == 0).
+Lemma irr_eq1 i : ('chi_i == 1) = (i == 0).

-Lemma cforder_irr_eq1 i : (#['chi_i]%CF == 1%N) = (i == 0).
+Lemma cforder_irr_eq1 i : (#['chi_i]%CF == 1%N) = (i == 0).

-Lemma irr_basis : basis_of 'CF(G)%VS (irr G).
+Lemma irr_basis : basis_of 'CF(G)%VS (irr G).

-Lemma eq_sum_nth_irr a : \sum_i a i *: 'chi[G]_i = \sum_i a i *: (irr G)`_i.
+Lemma eq_sum_nth_irr a : \sum_i a i *: 'chi[G]_i = \sum_i a i *: (irr G)`_i.

@@ -581,25 +582,25 @@ This is Isaacs, Theorem (2.8).
-Theorem cfun_irr_sum phi : {a | phi = \sum_i a i *: 'chi[G]_i}.
+Theorem cfun_irr_sum phi : {a | phi = \sum_i a i *: 'chi[G]_i}.

Lemma cfRepr_standard n (rG : mx_representation algCF G n) :
  cfRepr (standard_grepr rG)
-    = \sum_i (standard_irr_coef rG (W i))%:R *: 'chi_i.
+    = \sum_i (standard_irr_coef rG (W i))%:R *: 'chi_i.

Lemma cfRepr_inj n1 n2 rG1 rG2 :
-  @cfRepr _ G n1 rG1 = @cfRepr _ G n2 rG2 → mx_rsim rG1 rG2.
+  @cfRepr _ G n1 rG1 = @cfRepr _ G n2 rG2 → mx_rsim rG1 rG2.

Lemma cfRepr_rsimP n1 n2 rG1 rG2 :
-  reflect (mx_rsim rG1 rG2) (@cfRepr _ G n1 rG1 == @cfRepr _ G n2 rG2).
+  reflect (mx_rsim rG1 rG2) (@cfRepr _ G n1 rG1 == @cfRepr _ G n2 rG2).

Lemma irr_reprP xi :
-  reflect (exists2 rG : representation _ G, mx_irreducible rG & xi = cfRepr rG)
-          (xi \in irr G).
+  reflect (exists2 rG : representation _ G, mx_irreducible rG & xi = cfRepr rG)
+          (xi \in irr G).

@@ -609,7 +610,7 @@
Lemma Wedderburn_id_expansion i :
-  'e_i = #|G|%:R^-1 *: \sum_(x in G) 'chi_i 1%g × 'chi_i x^-1%g *: aG x.
+  'e_i = #|G|%:R^-1 *: \sum_(x in G) 'chi_i 1%g × 'chi_i x^-1%g *: aG x.

End IrrClass.
@@ -623,23 +624,23 @@ Variable gT : finGroupType.

-Definition character {G : {set gT}} :=
-  [qualify a phi : 'CF(G) | [∀ i, coord (irr G) i phi \in Cnat]].
-Fact character_key G : pred_key (@character G).
-Canonical character_keyed G := KeyedQualifier (character_key G).
+Definition character {G : {set gT}} :=
+  [qualify a phi : 'CF(G) | [∀ i, coord (irr G) i phi \in Cnat]].
+Fact character_key G : pred_key (@character G).
+Canonical character_keyed G := KeyedQualifier (character_key G).

-Variable G : {group gT}.
-Implicit Types (phi chi xi : 'CF(G)) (i : Iirr G).
+Variable G : {group gT}.
+Implicit Types (phi chi xi : 'CF(G)) (i : Iirr G).

-Lemma irr_char i : 'chi_i \is a character.
+Lemma irr_char i : 'chi_i \is a character.

-Lemma cfun1_char : (1 : 'CF(G)) \is a character.
+Lemma cfun1_char : (1 : 'CF(G)) \is a character.

-Lemma cfun0_char : (0 : 'CF(G)) \is a character.
+Lemma cfun0_char : (0 : 'CF(G)) \is a character.

Fact add_char : addr_closed (@character G).
@@ -647,40 +648,40 @@
Lemma char_sum_irrP {phi} :
-  reflect (∃ n, phi = \sum_i (n i)%:R *: 'chi_i) (phi \is a character).
+  reflect (∃ n, phi = \sum_i (n i)%:R *: 'chi_i) (phi \is a character).

Lemma char_sum_irr chi :
-  chi \is a character → {r | chi = \sum_(i <- r) 'chi_i}.
+  chi \is a character → {r | chi = \sum_(i <- r) 'chi_i}.

-Lemma Cnat_char1 chi : chi \is a character → chi 1%g \in Cnat.
+Lemma Cnat_char1 chi : chi \is a character → chi 1%g \in Cnat.

-Lemma char1_ge0 chi : chi \is a character → 0 ≤ chi 1%g.
+Lemma char1_ge0 chi : chi \is a character → 0 ≤ chi 1%g.

-Lemma char1_eq0 chi : chi \is a character → (chi 1%g == 0) = (chi == 0).
+Lemma char1_eq0 chi : chi \is a character → (chi 1%g == 0) = (chi == 0).

-Lemma char1_gt0 chi : chi \is a character → (0 < chi 1%g) = (chi != 0).
+Lemma char1_gt0 chi : chi \is a character → (0 < chi 1%g) = (chi != 0).

Lemma char_reprP phi :
-  reflect (∃ rG : representation algCF G, phi = cfRepr rG)
-          (phi \is a character).
+  reflect (∃ rG : representation algCF G, phi = cfRepr rG)
+          (phi \is a character).


-Lemma cfRepr_char n (rG : reprG n) : cfRepr rG \is a character.
+Lemma cfRepr_char n (rG : reprG n) : cfRepr rG \is a character.

-Lemma cfReg_char : cfReg G \is a character.
+Lemma cfReg_char : cfReg G \is a character.

Lemma cfRepr_prod n1 n2 (rG1 : reprG n1) (rG2 : reprG n2) :
-  cfRepr rG1 × cfRepr rG2 = cfRepr (prod_repr rG1 rG2).
+  cfRepr rG1 × cfRepr rG2 = cfRepr (prod_repr rG1 rG2).

Lemma mul_char : mulr_closed (@character G).
@@ -694,33 +695,33 @@ Section AutChar.

-Variables (gT : finGroupType) (G : {group gT}).
-Implicit Type u : {rmorphism algC → algC}.
-Implicit Type chi : 'CF(G).
+Variables (gT : finGroupType) (G : {group gT}).
+Implicit Type u : {rmorphism algC → algC}.
+Implicit Type chi : 'CF(G).

Lemma cfRepr_map u n (rG : mx_representation algCF G n) :
-  cfRepr (map_repr u rG) = cfAut u (cfRepr rG).
+  cfRepr (map_repr u rG) = cfAut u (cfRepr rG).

-Lemma cfAut_char u chi : (cfAut u chi \is a character) = (chi \is a character).
+Lemma cfAut_char u chi : (cfAut u chi \is a character) = (chi \is a character).

-Lemma cfConjC_char chi : (chi^*%CF \is a character) = (chi \is a character).
+Lemma cfConjC_char chi : (chi^*%CF \is a character) = (chi \is a character).

-Lemma cfAut_char1 u (chi : 'CF(G)) :
-  chi \is a character → cfAut u chi 1%g = chi 1%g.
+Lemma cfAut_char1 u (chi : 'CF(G)) :
+  chi \is a character → cfAut u chi 1%g = chi 1%g.

-Lemma cfAut_irr1 u i : (cfAut u 'chi[G]_i) 1%g = 'chi_i 1%g.
+Lemma cfAut_irr1 u i : (cfAut u 'chi[G]_i) 1%g = 'chi_i 1%g.

-Lemma cfConjC_char1 (chi : 'CF(G)) :
-  chi \is a character → chi^*%CF 1%g = chi 1%g.
+Lemma cfConjC_char1 (chi : 'CF(G)) :
+  chi \is a character → chi^*%CF 1%g = chi 1%g.

-Lemma cfConjC_irr1 u i : ('chi[G]_i)^*%CF 1%g = 'chi_i 1%g.
+Lemma cfConjC_irr1 u i : ('chi[G]_i)^*%CF 1%g = 'chi_i 1%g.

End AutChar.
@@ -729,110 +730,110 @@ Section Linear.

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

-Definition linear_char {B : {set gT}} :=
-  [qualify a phi : 'CF(B) | (phi \is a character) && (phi 1%g == 1)].
+Definition linear_char {B : {set gT}} :=
+  [qualify a phi : 'CF(B) | (phi \is a character) && (phi 1%g == 1)].

Section OneChar.

-Variable xi : 'CF(G).
-Hypothesis CFxi : xi \is a linear_char.
+Variable xi : 'CF(G).
+Hypothesis CFxi : xi \is a linear_char.

-Lemma lin_char1: xi 1%g = 1.
+Lemma lin_char1: xi 1%g = 1.

-Lemma lin_charW : xi \is a character.
+Lemma lin_charW : xi \is a character.

-Lemma cfun1_lin_char : (1 : 'CF(G)) \is a linear_char.
+Lemma cfun1_lin_char : (1 : 'CF(G)) \is a linear_char.

-Lemma lin_charM : {in G &, {morph xi : x y / (x × y)%g >-> x × y}}.
+Lemma lin_charM : {in G &, {morph xi : x y / (x × y)%g >-> x × y}}.

-Lemma lin_char_prod I r (P : pred I) (x : I → gT) :
-    (∀ i, P i → x i \in G) →
-  xi (\prod_(i <- r | P i) x i)%g = \prod_(i <- r | P i) xi (x i).
+Lemma lin_char_prod I r (P : pred I) (x : I → gT) :
+    (∀ i, P i → x i \in G) →
+  xi (\prod_(i <- r | P i) x i)%g = \prod_(i <- r | P i) xi (x i).

-Let xiMV x : x \in G → xi x × xi (x^-1)%g = 1.
+Let xiMV x : x \in G → xi x × xi (x^-1)%g = 1.

-Lemma lin_char_neq0 x : x \in G → xi x != 0.
+Lemma lin_char_neq0 x : x \in G → xi x != 0.

-Lemma lin_charV x : x \in G → xi x^-1%g = (xi x)^-1.
+Lemma lin_charV x : x \in G → xi x^-1%g = (xi x)^-1.

-Lemma lin_charX x n : x \in G → xi (x ^+ n)%g = xi x ^+ n.
+Lemma lin_charX x n : x \in G → xi (x ^+ n)%g = xi x ^+ n.

-Lemma lin_char_unity_root x : x \in G → xi x ^+ #[x] = 1.
+Lemma lin_char_unity_root x : x \in G → xi x ^+ #[x] = 1.

-Lemma normC_lin_char x : x \in G → `|xi x| = 1.
+Lemma normC_lin_char x : x \in G → `|xi x| = 1.

-Lemma lin_charV_conj x : x \in G → xi x^-1%g = (xi x)^*.
+Lemma lin_charV_conj x : x \in G → xi x^-1%g = (xi x)^*.

-Lemma lin_char_irr : xi \in irr G.
+Lemma lin_char_irr : xi \in irr G.

-Lemma mul_conjC_lin_char : xi × xi^*%CF = 1.
+Lemma mul_conjC_lin_char : xi × xi^*%CF = 1.

-Lemma lin_char_unitr : xi \in GRing.unit.
+Lemma lin_char_unitr : xi \in GRing.unit.

-Lemma invr_lin_char : xi^-1 = xi^*%CF.
+Lemma invr_lin_char : xi^-1 = xi^*%CF.

-Lemma fful_lin_char_inj : cfaithful xi → {in G &, injective xi}.
+Lemma fful_lin_char_inj : cfaithful xi → {in G &, injective xi}.

End OneChar.

-Lemma cfAut_lin_char u (xi : 'CF(G)) :
-  (cfAut u xi \is a linear_char) = (xi \is a linear_char).
+Lemma cfAut_lin_char u (xi : 'CF(G)) :
+  (cfAut u xi \is a linear_char) = (xi \is a linear_char).

-Lemma cfConjC_lin_char (xi : 'CF(G)) :
-  (xi^*%CF \is a linear_char) = (xi \is a linear_char).
+Lemma cfConjC_lin_char (xi : 'CF(G)) :
+  (xi^*%CF \is a linear_char) = (xi \is a linear_char).

-Lemma card_Iirr_abelian : abelian G → #|Iirr G| = #|G|.
+Lemma card_Iirr_abelian : abelian G → #|Iirr G| = #|G|.

-Lemma card_Iirr_cyclic : cyclic G → #|Iirr G| = #|G|.
+Lemma card_Iirr_cyclic : cyclic G → #|Iirr G| = #|G|.

Lemma char_abelianP :
-  reflect (∀ i : Iirr G, 'chi_i \is a linear_char) (abelian G).
+  reflect (∀ i : Iirr G, 'chi_i \is a linear_char) (abelian G).

Lemma irr_repr_lin_char (i : Iirr G) x :
-    x \in G → 'chi_i \is a linear_char →
-  irr_repr (socle_of_Iirr i) x = ('chi_i x)%:M.
+    x \in G → 'chi_i \is a linear_char →
+  irr_repr (socle_of_Iirr i) x = ('chi_i x)%:M.

-Fact linear_char_key B : pred_key (@linear_char B).
-Canonical linear_char_keted B := KeyedQualifier (linear_char_key B).
+Fact linear_char_key B : pred_key (@linear_char B).
+Canonical linear_char_keted B := KeyedQualifier (linear_char_key B).
Fact linear_char_divr : divr_closed (@linear_char G).
Canonical lin_char_mulrPred := MulrPred linear_char_divr.
Canonical lin_char_divrPred := DivrPred linear_char_divr.

-Lemma irr_cyclic_lin i : cyclic G → 'chi[G]_i \is a linear_char.
+Lemma irr_cyclic_lin i : cyclic G → 'chi[G]_i \is a linear_char.

-Lemma irr_prime_lin i : prime #|G| → 'chi[G]_i \is a linear_char.
+Lemma irr_prime_lin i : prime #|G| → 'chi[G]_i \is a linear_char.

End Linear.
@@ -852,16 +853,16 @@ This is Isaacs, Lemma (2.15)
-Lemma repr_rsim_diag (G : {group gT}) f (rG : mx_representation algCF G f) x :
-    x \in G → let chi := cfRepr rG in
-  ∃ e,
- [/\ (*a*) exists2 B, B \in unitmx & rG x = invmx B ×m diag_mx e ×m B,
-     (*b*) (∀ i, e 0 i ^+ #[x] = 1) ∧ (∀ i, `|e 0 i| = 1),
-     (*c*) chi x = \sum_i e 0 i ∧ `|chi x| ≤ chi 1%g
-   & (*d*) chi x^-1%g = (chi x)^*].
+Lemma repr_rsim_diag (G : {group gT}) f (rG : mx_representation algCF G f) x :
+    x \in G → let chi := cfRepr rG in
+  ∃ e,
+ [/\ (*a*) exists2 B, B \in unitmx & rG x = invmx B ×m diag_mx e ×m B,
+     (*b*) (∀ i, e 0 i ^+ #[x] = 1) ∧ (∀ i, `|e 0 i| = 1),
+     (*c*) chi x = \sum_i e 0 i ∧ `|chi x| ≤ chi 1%g
+   & (*d*) chi x^-1%g = (chi x)^*].

-Variables (A : {group aT}) (G : {group gT}).
+Variables (A : {group aT}) (G : {group gT}).

@@ -870,10 +871,10 @@ This is Isaacs, Lemma (2.15) (d).
-Lemma char_inv (chi : 'CF(G)) x : chi \is a character → chi x^-1%g = (chi x)^*.
+Lemma char_inv (chi : 'CF(G)) x : chi \is a character → chi x^-1%g = (chi x)^*.

-Lemma irr_inv i x : 'chi[G]_i x^-1%g = ('chi_i x)^*.
+Lemma irr_inv i x : 'chi[G]_i x^-1%g = ('chi_i x)^*.

@@ -883,8 +884,8 @@
Theorem generalized_orthogonality_relation y (i j : Iirr G) :
-  #|G|%:R^-1 × (\sum_(x in G) 'chi_i (x × y)%g × 'chi_j x^-1%g)
-    = (i == j)%:R × ('chi_i y / 'chi_i 1%g).
+  #|G|%:R^-1 × (\sum_(x in G) 'chi_i (x × y)%g × 'chi_j x^-1%g)
+    = (i == j)%:R × ('chi_i y / 'chi_i 1%g).

@@ -894,7 +895,7 @@
Corollary first_orthogonality_relation (i j : Iirr G) :
-  #|G|%:R^-1 × (\sum_(x in G) 'chi_i x × 'chi_j x^-1%g) = (i == j)%:R.
+  #|G|%:R^-1 × (\sum_(x in G) 'chi_i x × 'chi_j x^-1%g) = (i == j)%:R.

@@ -907,28 +908,28 @@
Definition irr_class i := enum_val (cast_ord (NirrE G) i).
Definition class_Iirr xG :=
-  cast_ord (esym (NirrE G)) (enum_rank_in (classes1 G) xG).
+  cast_ord (esym (NirrE G)) (enum_rank_in (classes1 G) xG).


-Definition character_table := \matrix_(i, j) 'chi[G]_i (g j).
+Definition character_table := \matrix_(i, j) 'chi[G]_i (g j).

-Lemma irr_classP i : c i \in classes G.
+Lemma irr_classP i : c i \in classes G.

-Lemma repr_irr_classK i : g i ^: G = c i.
+Lemma repr_irr_classK i : g i ^: G = c i.

-Lemma irr_classK : cancel c iC.
+Lemma irr_classK : cancel c iC.

-Lemma class_IirrK : {in classes G, cancel iC c}.
+Lemma class_IirrK : {in classes G, cancel iC c}.

Lemma reindex_irr_class R idx (op : @Monoid.com_law R idx) F :
-  \big[op/idx]_(xG in classes G) F xG = \big[op/idx]_i F (c i).
+  \big[op/idx]_(xG in classes G) F xG = \big[op/idx]_i F (c i).

@@ -938,11 +939,11 @@ orthogonality relation.
-Let X' := \matrix_(i, j) (#|'C_G[g i]|%:R^-1 × ('chi[G]_j (g i))^*).
-Let XX'_1: X ×m X' = 1%:M.
+Let X' := \matrix_(i, j) (#|'C_G[g i]|%:R^-1 × ('chi[G]_j (g i))^*).
+Let XX'_1: X ×m X' = 1%:M.

-Lemma character_table_unit : X \in unitmx.
+Lemma character_table_unit : X \in unitmx.
Let uX := character_table_unit.

@@ -953,12 +954,12 @@
Theorem second_orthogonality_relation x y :
-    y \in G →
-  \sum_i 'chi[G]_i x × ('chi_i y)^* = #|'C_G[x]|%:R *+ (x \in y ^: G).
+    y \in G →
+  \sum_i 'chi[G]_i x × ('chi_i y)^* = #|'C_G[x]|%:R *+ (x \in y ^: G).

Lemma eq_irr_mem_classP x y :
-  y \in G → reflect (∀ i, 'chi[G]_i x = 'chi_i y) (x \in y ^: G).
+  y \in G → reflect (∀ i, 'chi[G]_i x = 'chi_i y) (x \in y ^: G).

@@ -968,10 +969,10 @@
Lemma card_afix_irr_classes (ito : action A (Iirr G)) (cto : action A _) a :
-    a \in A → [acts A, on classes G | cto] →
-    (∀ i x y, x \in G → y \in cto (x ^: G) a →
-      'chi_i x = 'chi_(ito i a) y) →
-  #|'Fix_ito[a]| = #|'Fix_(classes G | cto)[a]|.
+    a \in A → [acts A, on classes G | cto] →
+    (∀ i x y, x \in G → y \in cto (x ^: G) a →
+      'chi_i x = 'chi_(ito i a) y) →
+  #|'Fix_ito[a]| = #|'Fix_(classes G | cto)[a]|.

End OrthogonalityRelations.
@@ -982,79 +983,79 @@ Section InnerProduct.

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

-Lemma cfdot_irr i j : '['chi_i, 'chi_j]_G = (i == j)%:R.
+Lemma cfdot_irr i j : '['chi_i, 'chi_j]_G = (i == j)%:R.

-Lemma cfnorm_irr i : '['chi[G]_i] = 1.
+Lemma cfnorm_irr i : '['chi[G]_i] = 1.

Lemma irr_orthonormal : orthonormal (irr G).

-Lemma coord_cfdot phi i : coord (irr G) i phi = '[phi, 'chi_i].
+Lemma coord_cfdot phi i : coord (irr G) i phi = '[phi, 'chi_i].

-Lemma cfun_sum_cfdot phi : phi = \sum_i '[phi, 'chi_i]_G *: 'chi_i.
+Lemma cfun_sum_cfdot phi : phi = \sum_i '[phi, 'chi_i]_G *: 'chi_i.

Lemma cfdot_sum_irr phi psi :
-  '[phi, psi]_G = \sum_i '[phi, 'chi_i] × '[psi, 'chi_i]^*.
+  '[phi, psi]_G = \sum_i '[phi, 'chi_i] × '[psi, 'chi_i]^*.

Lemma Cnat_cfdot_char_irr i phi :
-  phi \is a character → '[phi, 'chi_i]_G \in Cnat.
+  phi \is a character → '[phi, 'chi_i]_G \in Cnat.

Lemma cfdot_char_r phi chi :
-  chi \is a character → '[phi, chi]_G = \sum_i '[phi, 'chi_i] × '[chi, 'chi_i].
+  chi \is a character → '[phi, chi]_G = \sum_i '[phi, 'chi_i] × '[chi, 'chi_i].

Lemma Cnat_cfdot_char chi xi :
-  chi \is a character → xi \is a character → '[chi, xi]_G \in Cnat.
+  chi \is a character → xi \is a character → '[chi, xi]_G \in Cnat.

Lemma cfdotC_char chi xi :
-  chi \is a character→ xi \is a character → '[chi, xi]_G = '[xi, chi].
+  chi \is a character→ xi \is a character → '[chi, xi]_G = '[xi, chi].

-Lemma irrEchar chi : (chi \in irr G) = (chi \is a character) && ('[chi] == 1).
+Lemma irrEchar chi : (chi \in irr G) = (chi \is a character) && ('[chi] == 1).

-Lemma irrWchar chi : chi \in irr G → chi \is a character.
+Lemma irrWchar chi : chi \in irr G → chi \is a character.

-Lemma irrWnorm chi : chi \in irr G → '[chi] = 1.
+Lemma irrWnorm chi : chi \in irr G → '[chi] = 1.

Lemma mul_lin_irr xi chi :
-  xi \is a linear_char → chi \in irr G → xi × chi \in irr G.
+  xi \is a linear_char → chi \in irr G → xi × chi \in irr G.

Lemma eq_scaled_irr a b i j :
-  (a *: 'chi[G]_i == b *: 'chi_j) = (a == b) && ((a == 0) || (i == j)).
+  (a *: 'chi[G]_i == b *: 'chi_j) = (a == b) && ((a == 0) || (i == j)).

-Lemma eq_signed_irr (s t : bool) i j :
-  ((-1) ^+ s *: 'chi[G]_i == (-1) ^+ t *: 'chi_j) = (s == t) && (i == j).
+Lemma eq_signed_irr (s t : bool) i j :
+  ((-1) ^+ s *: 'chi[G]_i == (-1) ^+ t *: 'chi_j) = (s == t) && (i == j).

Lemma eq_scale_irr a (i j : Iirr G) :
-  (a *: 'chi_i == a *: 'chi_j) = (a == 0) || (i == j).
+  (a *: 'chi_i == a *: 'chi_j) = (a == 0) || (i == j).

Lemma eq_addZ_irr a b (i j r t : Iirr G) :
-  (a *: 'chi_i + b *: 'chi_j == a *: 'chi_r + b *: 'chi_t)
-   = [|| [&& (a == 0) || (i == r) & (b == 0) || (j == t)],
-         [&& i == t, j == r & a == b] | [&& i == j, r == t & a == - b]].
+  (a *: 'chi_i + b *: 'chi_j == a *: 'chi_r + b *: 'chi_t)
+   = [|| [&& (a == 0) || (i == r) & (b == 0) || (j == t)],
+         [&& i == t, j == r & a == b] | [&& i == j, r == t & a == - b]].

-Lemma eq_subZnat_irr (a b : nat) (i j r t : Iirr G) :
-  (a%:R *: 'chi_i - b%:R *: 'chi_j == a%:R *: 'chi_r - b%:R *: 'chi_t)
-     = [|| a == 0%N | i == r] && [|| b == 0%N | j == t]
-      || [&& i == j, r == t & a == b].
+Lemma eq_subZnat_irr (a b : nat) (i j r t : Iirr G) :
+  (a%:R *: 'chi_i - b%:R *: 'chi_j == a%:R *: 'chi_r - b%:R *: 'chi_t)
+     = [|| a == 0%N | i == r] && [|| b == 0%N | j == t]
+      || [&& i == j, r == t & a == b].

End InnerProduct.
@@ -1063,53 +1064,53 @@ Section IrrConstt.

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

-Lemma char1_ge_norm (chi : 'CF(G)) x :
-  chi \is a character → `|chi x| ≤ chi 1%g.
+Lemma char1_ge_norm (chi : 'CF(G)) x :
+  chi \is a character → `|chi x| ≤ chi 1%g.

Lemma max_cfRepr_norm_scalar n (rG : mx_representation algCF G n) x :
-     x \in G → `|cfRepr rG x| = cfRepr rG 1%g →
-   exists2 c, `|c| = 1 & rG x = c%:M.
+     x \in G → `|cfRepr rG x| = cfRepr rG 1%g →
+   exists2 c, `|c| = 1 & rG x = c%:M.

Lemma max_cfRepr_mx1 n (rG : mx_representation algCF G n) x :
-   x \in G → cfRepr rG x = cfRepr rG 1%g → rG x = 1%:M.
+   x \in G → cfRepr rG x = cfRepr rG 1%g → rG x = 1%:M.

-Definition irr_constt (B : {set gT}) phi := [pred i | '[phi, 'chi_i]_B != 0].
+Definition irr_constt (B : {set gT}) phi := [pred i | '[phi, 'chi_i]_B != 0].

-Lemma irr_consttE i phi : (i \in irr_constt phi) = ('[phi, 'chi_i]_G != 0).
+Lemma irr_consttE i phi : (i \in irr_constt phi) = ('[phi, 'chi_i]_G != 0).

Lemma constt_charP (i : Iirr G) chi :
-    chi \is a character →
-  reflect (exists2 chi', chi' \is a character & chi = 'chi_i + chi')
-          (i \in irr_constt chi).
+    chi \is a character →
+  reflect (exists2 chi', chi' \is a character & chi = 'chi_i + chi')
+          (i \in irr_constt chi).

-Lemma cfun_sum_constt (phi : 'CF(G)) :
-  phi = \sum_(i in irr_constt phi) '[phi, 'chi_i] *: 'chi_i.
+Lemma cfun_sum_constt (phi : 'CF(G)) :
+  phi = \sum_(i in irr_constt phi) '[phi, 'chi_i] *: 'chi_i.

-Lemma neq0_has_constt (phi : 'CF(G)) :
-  phi != 0 → ∃ i, i \in irr_constt phi.
+Lemma neq0_has_constt (phi : 'CF(G)) :
+  phi != 0 → ∃ i, i \in irr_constt phi.

-Lemma constt_irr i : irr_constt 'chi[G]_i =i pred1 i.
+Lemma constt_irr i : irr_constt 'chi[G]_i =i pred1 i.

Lemma char1_ge_constt (i : Iirr G) chi :
-  chi \is a character → i \in irr_constt chi → 'chi_i 1%g ≤ chi 1%g.
+  chi \is a character → i \in irr_constt chi → 'chi_i 1%g ≤ chi 1%g.

-Lemma constt_ortho_char (phi psi : 'CF(G)) i j :
-     phi \is a character → psi \is a character →
-     i \in irr_constt phi → j \in irr_constt psi →
-  '[phi, psi] = 0 → '['chi_i, 'chi_j] = 0.
+Lemma constt_ortho_char (phi psi : 'CF(G)) i j :
+     phi \is a character → psi \is a character →
+     i \in irr_constt phi → j \in irr_constt psi →
+  '[phi, psi] = 0 → '['chi_i, 'chi_j] = 0.

End IrrConstt.
@@ -1120,62 +1121,62 @@ Section Kernel.

-Variable (gT : finGroupType) (G : {group gT}).
-Implicit Types (phi chi xi : 'CF(G)) (H : {group gT}).
+Variable (gT : finGroupType) (G : {group gT}).
+Implicit Types (phi chi xi : 'CF(G)) (H : {group gT}).

Lemma cfker_repr n (rG : mx_representation algCF G n) :
-  cfker (cfRepr rG) = rker rG.
+  cfker (cfRepr rG) = rker rG.

Lemma cfkerEchar chi :
-  chi \is a character → cfker chi = [set x in G | chi x == chi 1%g].
+  chi \is a character → cfker chi = [set x in G | chi x == chi 1%g].

Lemma cfker_nzcharE chi :
-  chi \is a character → chi != 0 → cfker chi = [set x | chi x == chi 1%g].
+  chi \is a character → chi != 0 → cfker chi = [set x | chi x == chi 1%g].

-Lemma cfkerEirr i : cfker 'chi[G]_i = [set x | 'chi_i x == 'chi_i 1%g].
+Lemma cfkerEirr i : cfker 'chi[G]_i = [set x | 'chi_i x == 'chi_i 1%g].

-Lemma cfker_irr0 : cfker 'chi[G]_0 = G.
+Lemma cfker_irr0 : cfker 'chi[G]_0 = G.

Lemma cfaithful_reg : cfaithful (cfReg G).

Lemma cfkerE chi :
-    chi \is a character →
-  cfker chi = G :&: \bigcap_(i in irr_constt chi) cfker 'chi_i.
+    chi \is a character →
+  cfker chi = G :&: \bigcap_(i in irr_constt chi) cfker 'chi_i.

-Lemma TI_cfker_irr : \bigcap_i cfker 'chi[G]_i = [1].
+Lemma TI_cfker_irr : \bigcap_i cfker 'chi[G]_i = [1].

Lemma cfker_constt i chi :
-    chi \is a character → i \in irr_constt chi →
-  cfker chi \subset cfker 'chi[G]_i.
+    chi \is a character → i \in irr_constt chi →
+  cfker chi \subset cfker 'chi[G]_i.

Section KerLin.

-Variable xi : 'CF(G).
-Hypothesis lin_xi : xi \is a linear_char.
-Let Nxi: xi \is a character.
+Variable xi : 'CF(G).
+Hypothesis lin_xi : xi \is a linear_char.
+Let Nxi: xi \is a character.

-Lemma lin_char_der1 : G^`(1)%g \subset cfker xi.
+Lemma lin_char_der1 : G^`(1)%g \subset cfker xi.

-Lemma cforder_lin_char : #[xi]%CF = exponent (G / cfker xi)%g.
+Lemma cforder_lin_char : #[xi]%CF = exponent (G / cfker xi)%g.

-Lemma cforder_lin_char_dvdG : #[xi]%CF %| #|G|.
+Lemma cforder_lin_char_dvdG : #[xi]%CF %| #|G|.

-Lemma cforder_lin_char_gt0 : (0 < #[xi]%CF)%N.
+Lemma cforder_lin_char_gt0 : (0 < #[xi]%CF)%N.

End KerLin.
@@ -1187,41 +1188,41 @@ Section Restrict.

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

-Lemma cfRepr_sub n (rG : mx_representation algCF G n) (sHG : H \subset G) :
-  cfRepr (subg_repr rG sHG) = 'Res[H] (cfRepr rG).
+Lemma cfRepr_sub n (rG : mx_representation algCF G n) (sHG : H \subset G) :
+  cfRepr (subg_repr rG sHG) = 'Res[H] (cfRepr rG).

-Lemma cfRes_char chi : chi \is a character → 'Res[H, G] chi \is a character.
+Lemma cfRes_char chi : chi \is a character → 'Res[H, G] chi \is a character.

-Lemma cfRes_eq0 phi : phi \is a character → ('Res[H, G] phi == 0) = (phi == 0).
+Lemma cfRes_eq0 phi : phi \is a character → ('Res[H, G] phi == 0) = (phi == 0).

Lemma cfRes_lin_char chi :
-  chi \is a linear_char → 'Res[H, G] chi \is a linear_char.
+  chi \is a linear_char → 'Res[H, G] chi \is a linear_char.

-Lemma Res_irr_neq0 i : 'Res[H, G] 'chi_i != 0.
+Lemma Res_irr_neq0 i : 'Res[H, G] 'chi_i != 0.

-Lemma cfRes_lin_lin (chi : 'CF(G)) :
-  chi \is a character → 'Res[H] chi \is a linear_char → chi \is a linear_char.
+Lemma cfRes_lin_lin (chi : 'CF(G)) :
+  chi \is a character → 'Res[H] chi \is a linear_char → chi \is a linear_char.

Lemma cfRes_irr_irr chi :
-  chi \is a character → 'Res[H] chi \in irr H → chi \in irr G.
+  chi \is a character → 'Res[H] chi \in irr H → chi \in irr G.

-Definition Res_Iirr (A B : {set gT}) i := cfIirr ('Res[B, A] 'chi_i).
+Definition Res_Iirr (A B : {set gT}) i := cfIirr ('Res[B, A] 'chi_i).

-Lemma Res_Iirr0 : Res_Iirr H (0 : Iirr G) = 0.
+Lemma Res_Iirr0 : Res_Iirr H (0 : Iirr G) = 0.

-Lemma lin_Res_IirrE i : 'chi[G]_i 1%g = 1 → 'chi_(Res_Iirr H i) = 'Res 'chi_i.
+Lemma lin_Res_IirrE i : 'chi[G]_i 1%g = 1 → 'chi_(Res_Iirr H i) = 'Res 'chi_i.

End Restrict.
@@ -1232,21 +1233,21 @@ Section MoreConstt.

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

Lemma constt_Ind_Res i j :
-  i \in irr_constt ('Ind[G] 'chi_j) = (j \in irr_constt ('Res[H] 'chi_i)).
+  i \in irr_constt ('Ind[G] 'chi_j) = (j \in irr_constt ('Res[H] 'chi_i)).

Lemma cfdot_Res_ge_constt i j psi :
-    psi \is a character → j \in irr_constt psi →
-  '['Res[H, G] 'chi_j, 'chi_i] ≤ '['Res[H] psi, 'chi_i].
+    psi \is a character → j \in irr_constt psi →
+  '['Res[H, G] 'chi_j, 'chi_i] ≤ '['Res[H] psi, 'chi_i].

Lemma constt_Res_trans j psi :
-    psi \is a character → j \in irr_constt psi →
-  {subset irr_constt ('Res[H, G] 'chi_j) ≤ irr_constt ('Res[H] psi)}.
+    psi \is a character → j \in irr_constt psi →
+  {subset irr_constt ('Res[H, G] 'chi_j) ≤ irr_constt ('Res[H] psi)}.

End MoreConstt.
@@ -1255,49 +1256,49 @@ Section Morphim.

-Variables (aT rT : finGroupType) (G D : {group aT}) (f : {morphism D >-> rT}).
-Implicit Type chi : 'CF(f @* G).
+Variables (aT rT : finGroupType) (G D : {group aT}) (f : {morphism D >-> rT}).
+Implicit Type chi : 'CF(f @* G).

-Lemma cfRepr_morphim n (rfG : mx_representation algCF (f @* G) n) sGD :
-  cfRepr (morphim_repr rfG sGD) = cfMorph (cfRepr rfG).
+Lemma cfRepr_morphim n (rfG : mx_representation algCF (f @* G) n) sGD :
+  cfRepr (morphim_repr rfG sGD) = cfMorph (cfRepr rfG).

-Lemma cfMorph_char chi : chi \is a character → cfMorph chi \is a character.
+Lemma cfMorph_char chi : chi \is a character → cfMorph chi \is a character.

Lemma cfMorph_lin_char chi :
-  chi \is a linear_char → cfMorph chi \is a linear_char.
+  chi \is a linear_char → cfMorph chi \is a linear_char.

Lemma cfMorph_charE chi :
-  G \subset D → (cfMorph chi \is a character) = (chi \is a character).
+  G \subset D → (cfMorph chi \is a character) = (chi \is a character).

Lemma cfMorph_lin_charE chi :
-  G \subset D → (cfMorph chi \is a linear_char) = (chi \is a linear_char).
+  G \subset D → (cfMorph chi \is a linear_char) = (chi \is a linear_char).

Lemma cfMorph_irr chi :
-  G \subset D → (cfMorph chi \in irr G) = (chi \in irr (f @* G)).
+  G \subset D → (cfMorph chi \in irr G) = (chi \in irr (f @* G)).

-Definition morph_Iirr i := cfIirr (cfMorph 'chi[f @* G]_i).
+Definition morph_Iirr i := cfIirr (cfMorph 'chi[f @* G]_i).

-Lemma morph_Iirr0 : morph_Iirr 0 = 0.
+Lemma morph_Iirr0 : morph_Iirr 0 = 0.

-Hypothesis sGD : G \subset D.
+Hypothesis sGD : G \subset D.

-Lemma morph_IirrE i : 'chi_(morph_Iirr i) = cfMorph 'chi_i.
+Lemma morph_IirrE i : 'chi_(morph_Iirr i) = cfMorph 'chi_i.

-Lemma morph_Iirr_inj : injective morph_Iirr.
+Lemma morph_Iirr_inj : injective morph_Iirr.

-Lemma morph_Iirr_eq0 i : (morph_Iirr i == 0) = (i == 0).
+Lemma morph_Iirr_eq0 i : (morph_Iirr i == 0) = (i == 0).

End Morphim.
@@ -1306,35 +1307,35 @@ Section Isom.

-Variables (aT rT : finGroupType) (G : {group aT}) (f : {morphism G >-> rT}).
-Variables (R : {group rT}) (isoGR : isom G R f).
-Implicit Type chi : 'CF(G).
+Variables (aT rT : finGroupType) (G : {group aT}) (f : {morphism G >-> rT}).
+Variables (R : {group rT}) (isoGR : isom G R f).
+Implicit Type chi : 'CF(G).

Lemma cfIsom_char chi :
-  (cfIsom isoGR chi \is a character) = (chi \is a character).
+  (cfIsom isoGR chi \is a character) = (chi \is a character).

Lemma cfIsom_lin_char chi :
-  (cfIsom isoGR chi \is a linear_char) = (chi \is a linear_char).
+  (cfIsom isoGR chi \is a linear_char) = (chi \is a linear_char).

-Lemma cfIsom_irr chi : (cfIsom isoGR chi \in irr R) = (chi \in irr G).
+Lemma cfIsom_irr chi : (cfIsom isoGR chi \in irr R) = (chi \in irr G).

-Definition isom_Iirr i := cfIirr (cfIsom isoGR 'chi_i).
+Definition isom_Iirr i := cfIirr (cfIsom isoGR 'chi_i).

-Lemma isom_IirrE i : 'chi_(isom_Iirr i) = cfIsom isoGR 'chi_i.
+Lemma isom_IirrE i : 'chi_(isom_Iirr i) = cfIsom isoGR 'chi_i.

-Lemma isom_Iirr_inj : injective isom_Iirr.
+Lemma isom_Iirr_inj : injective isom_Iirr.

-Lemma isom_Iirr_eq0 i : (isom_Iirr i == 0) = (i == 0).
+Lemma isom_Iirr_eq0 i : (isom_Iirr i == 0) = (i == 0).

-Lemma isom_Iirr0 : isom_Iirr 0 = 0.
+Lemma isom_Iirr0 : isom_Iirr 0 = 0.

End Isom.
@@ -1345,14 +1346,14 @@ Section IsomInv.

-Variables (aT rT : finGroupType) (G : {group aT}) (f : {morphism G >-> rT}).
-Variables (R : {group rT}) (isoGR : isom G R f).
+Variables (aT rT : finGroupType) (G : {group aT}) (f : {morphism G >-> rT}).
+Variables (R : {group rT}) (isoGR : isom G R f).

-Lemma isom_IirrK : cancel (isom_Iirr isoGR) (isom_Iirr (isom_sym isoGR)).
+Lemma isom_IirrK : cancel (isom_Iirr isoGR) (isom_Iirr (isom_sym isoGR)).

-Lemma isom_IirrKV : cancel (isom_Iirr (isom_sym isoGR)) (isom_Iirr isoGR).
+Lemma isom_IirrKV : cancel (isom_Iirr (isom_sym isoGR)) (isom_Iirr isoGR).

End IsomInv.
@@ -1361,50 +1362,50 @@ Section Sdprod.

-Variables (gT : finGroupType) (K H G : {group gT}).
-Hypothesis defG : K ><| H = G.
-Let nKG: G \subset 'N(K).
+Variables (gT : finGroupType) (K H G : {group gT}).
+Hypothesis defG : K ><| H = G.
+Let nKG: G \subset 'N(K).

Lemma cfSdprod_char chi :
- (cfSdprod defG chi \is a character) = (chi \is a character).
+ (cfSdprod defG chi \is a character) = (chi \is a character).

Lemma cfSdprod_lin_char chi :
- (cfSdprod defG chi \is a linear_char) = (chi \is a linear_char).
+ (cfSdprod defG chi \is a linear_char) = (chi \is a linear_char).

-Lemma cfSdprod_irr chi : (cfSdprod defG chi \in irr G) = (chi \in irr H).
+Lemma cfSdprod_irr chi : (cfSdprod defG chi \in irr G) = (chi \in irr H).

-Definition sdprod_Iirr j := cfIirr (cfSdprod defG 'chi_j).
+Definition sdprod_Iirr j := cfIirr (cfSdprod defG 'chi_j).

-Lemma sdprod_IirrE j : 'chi_(sdprod_Iirr j) = cfSdprod defG 'chi_j.
+Lemma sdprod_IirrE j : 'chi_(sdprod_Iirr j) = cfSdprod defG 'chi_j.

-Lemma sdprod_IirrK : cancel sdprod_Iirr (Res_Iirr H).
+Lemma sdprod_IirrK : cancel sdprod_Iirr (Res_Iirr H).

-Lemma sdprod_Iirr_inj : injective sdprod_Iirr.
+Lemma sdprod_Iirr_inj : injective sdprod_Iirr.

-Lemma sdprod_Iirr_eq0 i : (sdprod_Iirr i == 0) = (i == 0).
+Lemma sdprod_Iirr_eq0 i : (sdprod_Iirr i == 0) = (i == 0).

-Lemma sdprod_Iirr0 : sdprod_Iirr 0 = 0.
+Lemma sdprod_Iirr0 : sdprod_Iirr 0 = 0.

Lemma Res_sdprod_irr phi :
-  K \subset cfker phi → phi \in irr G → 'Res phi \in irr H.
+  K \subset cfker phi → phi \in irr G → 'Res phi \in irr H.

Lemma sdprod_Res_IirrE i :
-  K \subset cfker 'chi[G]_i → 'chi_(Res_Iirr H i) = 'Res 'chi_i.
+  K \subset cfker 'chi[G]_i → 'chi_(Res_Iirr H i) = 'Res 'chi_i.

Lemma sdprod_Res_IirrK i :
-  K \subset cfker 'chi_i → sdprod_Iirr (Res_Iirr H i) = i.
+  K \subset cfker 'chi_i → sdprod_Iirr (Res_Iirr H i) = i.

End Sdprod.
@@ -1415,119 +1416,119 @@ Section DProd.

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

-Lemma cfDprodKl_abelian j : abelian H → cancel ((cfDprod KxH)^~ 'chi_j) 'Res.
+Lemma cfDprodKl_abelian j : abelian H → cancel ((cfDprod KxH)^~ 'chi_j) 'Res.

-Lemma cfDprodKr_abelian i : abelian K → cancel (cfDprod KxH 'chi_i) 'Res.
+Lemma cfDprodKr_abelian i : abelian K → cancel (cfDprod KxH 'chi_i) 'Res.

Lemma cfDprodl_char phi :
-  (cfDprodl KxH phi \is a character) = (phi \is a character).
+  (cfDprodl KxH phi \is a character) = (phi \is a character).

Lemma cfDprodr_char psi :
-  (cfDprodr KxH psi \is a character) = (psi \is a character).
+  (cfDprodr KxH psi \is a character) = (psi \is a character).

Lemma cfDprod_char phi psi :
-     phi \is a character → psi \is a character →
-  cfDprod KxH phi psi \is a character.
+     phi \is a character → psi \is a character →
+  cfDprod KxH phi psi \is a character.

Lemma cfDprod_eq1 phi psi :
-    phi \is a character → psi \is a character →
-  (cfDprod KxH phi psi == 1) = (phi == 1) && (psi == 1).
+    phi \is a character → psi \is a character →
+  (cfDprod KxH phi psi == 1) = (phi == 1) && (psi == 1).

Lemma cfDprodl_lin_char phi :
-  (cfDprodl KxH phi \is a linear_char) = (phi \is a linear_char).
+  (cfDprodl KxH phi \is a linear_char) = (phi \is a linear_char).

Lemma cfDprodr_lin_char psi :
-  (cfDprodr KxH psi \is a linear_char) = (psi \is a linear_char).
+  (cfDprodr KxH psi \is a linear_char) = (psi \is a linear_char).

Lemma cfDprod_lin_char phi psi :
-     phi \is a linear_char → psi \is a linear_char →
-  cfDprod KxH phi psi \is a linear_char.
+     phi \is a linear_char → psi \is a linear_char →
+  cfDprod KxH phi psi \is a linear_char.

-Lemma cfDprodl_irr chi : (cfDprodl KxH chi \in irr G) = (chi \in irr K).
+Lemma cfDprodl_irr chi : (cfDprodl KxH chi \in irr G) = (chi \in irr K).

-Lemma cfDprodr_irr chi : (cfDprodr KxH chi \in irr G) = (chi \in irr H).
+Lemma cfDprodr_irr chi : (cfDprodr KxH chi \in irr G) = (chi \in irr H).

-Definition dprodl_Iirr i := cfIirr (cfDprodl KxH 'chi_i).
+Definition dprodl_Iirr i := cfIirr (cfDprodl KxH 'chi_i).

-Lemma dprodl_IirrE i : 'chi_(dprodl_Iirr i) = cfDprodl KxH 'chi_i.
- Lemma dprodl_IirrK : cancel dprodl_Iirr (Res_Iirr K).
- Lemma dprodl_Iirr_eq0 i : (dprodl_Iirr i == 0) = (i == 0).
- Lemma dprodl_Iirr0 : dprodl_Iirr 0 = 0.
+Lemma dprodl_IirrE i : 'chi_(dprodl_Iirr i) = cfDprodl KxH 'chi_i.
+ Lemma dprodl_IirrK : cancel dprodl_Iirr (Res_Iirr K).
+ Lemma dprodl_Iirr_eq0 i : (dprodl_Iirr i == 0) = (i == 0).
+ Lemma dprodl_Iirr0 : dprodl_Iirr 0 = 0.

-Definition dprodr_Iirr j := cfIirr (cfDprodr KxH 'chi_j).
+Definition dprodr_Iirr j := cfIirr (cfDprodr KxH 'chi_j).

-Lemma dprodr_IirrE j : 'chi_(dprodr_Iirr j) = cfDprodr KxH 'chi_j.
- Lemma dprodr_IirrK : cancel dprodr_Iirr (Res_Iirr H).
- Lemma dprodr_Iirr_eq0 j : (dprodr_Iirr j == 0) = (j == 0).
- Lemma dprodr_Iirr0 : dprodr_Iirr 0 = 0.
+Lemma dprodr_IirrE j : 'chi_(dprodr_Iirr j) = cfDprodr KxH 'chi_j.
+ Lemma dprodr_IirrK : cancel dprodr_Iirr (Res_Iirr H).
+ Lemma dprodr_Iirr_eq0 j : (dprodr_Iirr j == 0) = (j == 0).
+ Lemma dprodr_Iirr0 : dprodr_Iirr 0 = 0.

-Lemma cfDprod_irr i j : cfDprod KxH 'chi_i 'chi_j \in irr G.
+Lemma cfDprod_irr i j : cfDprod KxH 'chi_i 'chi_j \in irr G.

-Definition dprod_Iirr ij := cfIirr (cfDprod KxH 'chi_ij.1 'chi_ij.2).
+Definition dprod_Iirr ij := cfIirr (cfDprod KxH 'chi_ij.1 'chi_ij.2).

-Lemma dprod_IirrE i j : 'chi_(dprod_Iirr (i, j)) = cfDprod KxH 'chi_i 'chi_j.
+Lemma dprod_IirrE i j : 'chi_(dprod_Iirr (i, j)) = cfDprod KxH 'chi_i 'chi_j.

-Lemma dprod_IirrEl i : 'chi_(dprod_Iirr (i, 0)) = cfDprodl KxH 'chi_i.
+Lemma dprod_IirrEl i : 'chi_(dprod_Iirr (i, 0)) = cfDprodl KxH 'chi_i.

-Lemma dprod_IirrEr j : 'chi_(dprod_Iirr (0, j)) = cfDprodr KxH 'chi_j.
+Lemma dprod_IirrEr j : 'chi_(dprod_Iirr (0, j)) = cfDprodr KxH 'chi_j.

-Lemma dprod_Iirr_inj : injective dprod_Iirr.
+Lemma dprod_Iirr_inj : injective dprod_Iirr.

-Lemma dprod_Iirr0 : dprod_Iirr (0, 0) = 0.
+Lemma dprod_Iirr0 : dprod_Iirr (0, 0) = 0.

-Lemma dprod_Iirr0l j : dprod_Iirr (0, j) = dprodr_Iirr j.
+Lemma dprod_Iirr0l j : dprod_Iirr (0, j) = dprodr_Iirr j.

-Lemma dprod_Iirr0r i : dprod_Iirr (i, 0) = dprodl_Iirr i.
+Lemma dprod_Iirr0r i : dprod_Iirr (i, 0) = dprodl_Iirr i.

-Lemma dprod_Iirr_eq0 i j : (dprod_Iirr (i, j) == 0) = (i == 0) && (j == 0).
+Lemma dprod_Iirr_eq0 i j : (dprod_Iirr (i, j) == 0) = (i == 0) && (j == 0).

Lemma cfdot_dprod_irr i1 i2 j1 j2 :
-  '['chi_(dprod_Iirr (i1, j1)), 'chi_(dprod_Iirr (i2, j2))]
-     = ((i1 == i2) && (j1 == j2))%:R.
+  '['chi_(dprod_Iirr (i1, j1)), 'chi_(dprod_Iirr (i2, j2))]
+     = ((i1 == i2) && (j1 == j2))%:R.

-Lemma dprod_Iirr_onto k : k \in codom dprod_Iirr.
+Lemma dprod_Iirr_onto k : k \in codom dprod_Iirr.

Definition inv_dprod_Iirr i := iinv (dprod_Iirr_onto i).

-Lemma dprod_IirrK : cancel dprod_Iirr inv_dprod_Iirr.
+Lemma dprod_IirrK : cancel dprod_Iirr inv_dprod_Iirr.

-Lemma inv_dprod_IirrK : cancel inv_dprod_Iirr dprod_Iirr.
+Lemma inv_dprod_IirrK : cancel inv_dprod_Iirr dprod_Iirr.

-Lemma inv_dprod_Iirr0 : inv_dprod_Iirr 0 = (0, 0).
+Lemma inv_dprod_Iirr0 : inv_dprod_Iirr 0 = (0, 0).

End DProd.
@@ -1535,72 +1536,72 @@

-Lemma dprod_IirrC (gT : finGroupType) (G K H : {group gT})
-                  (KxH : K \x H = G) (HxK : H \x K = G) i j :
-  dprod_Iirr KxH (i, j) = dprod_Iirr HxK (j, i).
+Lemma dprod_IirrC (gT : finGroupType) (G K H : {group gT})
+                  (KxH : K \x H = G) (HxK : H \x K = G) i j :
+  dprod_Iirr KxH (i, j) = dprod_Iirr HxK (j, i).

Section BigDprod.

-Variables (gT : finGroupType) (I : finType) (P : pred I).
-Variables (A : I → {group gT}) (G : {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}).
+Hypothesis defG : \big[dprod/1%g]_(i | P i) A i = G.

-Let sAG i : P i → A i \subset G.
+Let sAG i : P i → A i \subset G.

-Lemma cfBigdprodi_char i (phi : 'CF(A i)) :
-  phi \is a character → cfBigdprodi defG phi \is a character.
+Lemma cfBigdprodi_char i (phi : 'CF(A i)) :
+  phi \is a character → cfBigdprodi defG phi \is a character.

-Lemma cfBigdprodi_charE i (phi : 'CF(A i)) :
-  P i → (cfBigdprodi defG phi \is a character) = (phi \is a character).
+Lemma cfBigdprodi_charE i (phi : 'CF(A i)) :
+  P i → (cfBigdprodi defG phi \is a character) = (phi \is a character).

Lemma cfBigdprod_char phi :
-    (∀ i, P i → phi i \is a character) →
-  cfBigdprod defG phi \is a character.
+    (∀ i, P i → phi i \is a character) →
+  cfBigdprod defG phi \is a character.

-Lemma cfBigdprodi_lin_char i (phi : 'CF(A i)) :
-  phi \is a linear_char → cfBigdprodi defG phi \is a linear_char.
+Lemma cfBigdprodi_lin_char i (phi : 'CF(A i)) :
+  phi \is a linear_char → cfBigdprodi defG phi \is a linear_char.

-Lemma cfBigdprodi_lin_charE i (phi : 'CF(A i)) :
-  P i → (cfBigdprodi defG phi \is a linear_char) = (phi \is a linear_char).
+Lemma cfBigdprodi_lin_charE i (phi : 'CF(A i)) :
+  P i → (cfBigdprodi defG phi \is a linear_char) = (phi \is a linear_char).

Lemma cfBigdprod_lin_char phi :
-    (∀ i, P i → phi i \is a linear_char) →
-  cfBigdprod defG phi \is a linear_char.
+    (∀ i, P i → phi i \is a linear_char) →
+  cfBigdprod defG phi \is a linear_char.

Lemma cfBigdprodi_irr i chi :
-  P i → (cfBigdprodi defG chi \in irr G) = (chi \in irr (A i)).
+  P i → (cfBigdprodi defG chi \in irr G) = (chi \in irr (A i)).

Lemma cfBigdprod_irr chi :
-  (∀ i, P i → chi i \in irr (A i)) → cfBigdprod defG chi \in irr G.
+  (∀ i, P i → chi i \in irr (A i)) → cfBigdprod defG chi \in irr G.

Lemma cfBigdprod_eq1 phi :
-    (∀ i, P i → phi i \is a character) →
-  (cfBigdprod defG phi == 1) = [∀ (i | P i), phi i == 1].
+    (∀ i, P i → phi i \is a character) →
+  (cfBigdprod defG phi == 1) = [∀ (i | P i), phi i == 1].

Lemma cfBigdprod_Res_lin chi :
-  chi \is a linear_char → cfBigdprod defG (fun i ⇒ 'Res[A i] chi) = chi.
+  chi \is a linear_char → cfBigdprod defG (fun i ⇒ 'Res[A i] chi) = chi.

Lemma cfBigdprodKlin phi :
-  (∀ i, P i → phi i \is a linear_char) →
-  ∀ i, P i → 'Res (cfBigdprod defG phi) = phi i.
+  (∀ i, P i → phi i \is a linear_char) →
+  ∀ i, P i → 'Res (cfBigdprod defG phi) = phi i.

-Lemma cfBigdprodKabelian Iphi (phi := fun i ⇒ 'chi_(Iphi i)) :
-  abelian G → ∀ i, P i → 'Res (cfBigdprod defG phi) = 'chi_(Iphi i).
+Lemma cfBigdprodKabelian Iphi (phi := fun i ⇒ 'chi_(Iphi i)) :
+  abelian G → ∀ i, P i → 'Res (cfBigdprod defG phi) = 'chi_(Iphi i).

End BigDprod.
@@ -1609,62 +1610,62 @@ Section Aut.

-Variables (gT : finGroupType) (G : {group gT}).
-Implicit Type u : {rmorphism algC → algC}.
+Variables (gT : finGroupType) (G : {group gT}).
+Implicit Type u : {rmorphism algC → algC}.

-Lemma conjC_charAut u (chi : 'CF(G)) x :
-  chi \is a character → (u (chi x))^* = u (chi x)^*.
+Lemma conjC_charAut u (chi : 'CF(G)) x :
+  chi \is a character → (u (chi x))^* = u (chi x)^*.

-Lemma conjC_irrAut u i x : (u ('chi[G]_i x))^* = u ('chi_i x)^*.
+Lemma conjC_irrAut u i x : (u ('chi[G]_i x))^* = u ('chi_i x)^*.

-Lemma cfdot_aut_char u (phi chi : 'CF(G)) :
-  chi \is a character → '[cfAut u phi, cfAut u chi] = u '[phi, chi].
+Lemma cfdot_aut_char u (phi chi : 'CF(G)) :
+  chi \is a character → '[cfAut u phi, cfAut u chi] = u '[phi, chi].

Lemma cfdot_aut_irr u phi i :
-  '[cfAut u phi, cfAut u 'chi[G]_i] = u '[phi, 'chi_i].
+  '[cfAut u phi, cfAut u 'chi[G]_i] = u '[phi, 'chi_i].

-Lemma cfAut_irr u chi : (cfAut u chi \in irr G) = (chi \in irr G).
+Lemma cfAut_irr u chi : (cfAut u chi \in irr G) = (chi \in irr G).

-Lemma cfConjC_irr i : (('chi_i)^*)%CF \in irr G.
+Lemma cfConjC_irr i : (('chi_i)^*)%CF \in irr G.

Lemma irr_aut_closed u : cfAut_closed u (irr G).

-Definition aut_Iirr u i := cfIirr (cfAut u 'chi[G]_i).
+Definition aut_Iirr u i := cfIirr (cfAut u 'chi[G]_i).

-Lemma aut_IirrE u i : 'chi_(aut_Iirr u i) = cfAut u 'chi_i.
+Lemma aut_IirrE u i : 'chi_(aut_Iirr u i) = cfAut u 'chi_i.

Definition conjC_Iirr := aut_Iirr conjC.

-Lemma conjC_IirrE i : 'chi[G]_(conjC_Iirr i) = ('chi_i)^*%CF.
+Lemma conjC_IirrE i : 'chi[G]_(conjC_Iirr i) = ('chi_i)^*%CF.

-Lemma conjC_IirrK : involutive conjC_Iirr.
+Lemma conjC_IirrK : involutive conjC_Iirr.

-Lemma aut_Iirr0 u : aut_Iirr u 0 = 0 :> Iirr G.
+Lemma aut_Iirr0 u : aut_Iirr u 0 = 0 :> Iirr G.

-Lemma conjC_Iirr0 : conjC_Iirr 0 = 0 :> Iirr G.
+Lemma conjC_Iirr0 : conjC_Iirr 0 = 0 :> Iirr G.

-Lemma aut_Iirr_eq0 u i : (aut_Iirr u i == 0) = (i == 0).
+Lemma aut_Iirr_eq0 u i : (aut_Iirr u i == 0) = (i == 0).

-Lemma conjC_Iirr_eq0 i : (conjC_Iirr i == 0 :> Iirr G) = (i == 0).
+Lemma conjC_Iirr_eq0 i : (conjC_Iirr i == 0 :> Iirr G) = (i == 0).

-Lemma aut_Iirr_inj u : injective (aut_Iirr u).
+Lemma aut_Iirr_inj u : injective (aut_Iirr u).

End Aut.
@@ -1678,106 +1679,106 @@ Variable (gT : finGroupType).

-Implicit Types G H : {group gT}.
+Implicit Types G H : {group gT}.

-Lemma cfQuo_char G H (chi : 'CF(G)) :
-  chi \is a character → (chi / H)%CF \is a character.
+Lemma cfQuo_char G H (chi : 'CF(G)) :
+  chi \is a character → (chi / H)%CF \is a character.

-Lemma cfQuo_lin_char G H (chi : 'CF(G)) :
-  chi \is a linear_char → (chi / H)%CF \is a linear_char.
+Lemma cfQuo_lin_char G H (chi : 'CF(G)) :
+  chi \is a linear_char → (chi / H)%CF \is a linear_char.

-Lemma cfMod_char G H (chi : 'CF(G / H)) :
-  chi \is a character → (chi %% H)%CF \is a character.
+Lemma cfMod_char G H (chi : 'CF(G / H)) :
+  chi \is a character → (chi %% H)%CF \is a character.

-Lemma cfMod_lin_char G H (chi : 'CF(G / H)) :
-  chi \is a linear_char → (chi %% H)%CF \is a linear_char.
+Lemma cfMod_lin_char G H (chi : 'CF(G / H)) :
+  chi \is a linear_char → (chi %% H)%CF \is a linear_char.

-Lemma cfMod_charE G H (chi : 'CF(G / H)) :
-  H <| G → (chi %% H \is a character)%CF = (chi \is a character).
+Lemma cfMod_charE G H (chi : 'CF(G / H)) :
+  H <| G → (chi %% H \is a character)%CF = (chi \is a character).

-Lemma cfMod_lin_charE G H (chi : 'CF(G / H)) :
-  H <| G → (chi %% H \is a linear_char)%CF = (chi \is a linear_char).
+Lemma cfMod_lin_charE G H (chi : 'CF(G / H)) :
+  H <| G → (chi %% H \is a linear_char)%CF = (chi \is a linear_char).

-Lemma cfQuo_charE G H (chi : 'CF(G)) :
-   H <| G → H \subset cfker chi →
- (chi / H \is a character)%CF = (chi \is a character).
+Lemma cfQuo_charE G H (chi : 'CF(G)) :
+   H <| G → H \subset cfker chi →
+ (chi / H \is a character)%CF = (chi \is a character).

-Lemma cfQuo_lin_charE G H (chi : 'CF(G)) :
-   H <| G → H \subset cfker chi →
- (chi / H \is a linear_char)%CF = (chi \is a linear_char).
+Lemma cfQuo_lin_charE G H (chi : 'CF(G)) :
+   H <| G → H \subset cfker chi →
+ (chi / H \is a linear_char)%CF = (chi \is a linear_char).

Lemma cfMod_irr G H chi :
-  H <| G → (chi %% H \in irr G)%CF = (chi \in irr (G / H)).
+  H <| G → (chi %% H \in irr G)%CF = (chi \in irr (G / H)).

-Definition mod_Iirr G H i := cfIirr ('chi[G / H]_i %% H)%CF.
+Definition mod_Iirr G H i := cfIirr ('chi[G / H]_i %% H)%CF.

-Lemma mod_Iirr0 G H : mod_Iirr (0 : Iirr (G / H)) = 0.
+Lemma mod_Iirr0 G H : mod_Iirr (0 : Iirr (G / H)) = 0.

-Lemma mod_IirrE G H i : H <| G → 'chi_(mod_Iirr i) = ('chi[G / H]_i %% H)%CF.
+Lemma mod_IirrE G H i : H <| G → 'chi_(mod_Iirr i) = ('chi[G / H]_i %% H)%CF.

Lemma mod_Iirr_eq0 G H i :
-  H <| G → (mod_Iirr i == 0) = (i == 0 :> Iirr (G / H)).
+  H <| G → (mod_Iirr i == 0) = (i == 0 :> Iirr (G / H)).

Lemma cfQuo_irr G H chi :
-     H <| G → H \subset cfker chi →
-  ((chi / H)%CF \in irr (G / H)) = (chi \in irr G).
+     H <| G → H \subset cfker chi →
+  ((chi / H)%CF \in irr (G / H)) = (chi \in irr G).

-Definition quo_Iirr G H i := cfIirr ('chi[G]_i / H)%CF.
+Definition quo_Iirr G H i := cfIirr ('chi[G]_i / H)%CF.

-Lemma quo_Iirr0 G H : quo_Iirr H (0 : Iirr G) = 0.
+Lemma quo_Iirr0 G H : quo_Iirr H (0 : Iirr G) = 0.

Lemma quo_IirrE G H i :
-  H <| G → H \subset cfker 'chi[G]_i → 'chi_(quo_Iirr H i) = ('chi_i / H)%CF.
+  H <| G → H \subset cfker 'chi[G]_i → 'chi_(quo_Iirr H i) = ('chi_i / H)%CF.

Lemma quo_Iirr_eq0 G H i :
-  H <| G → H \subset cfker 'chi[G]_i → (quo_Iirr H i == 0) = (i == 0).
+  H <| G → H \subset cfker 'chi[G]_i → (quo_Iirr H i == 0) = (i == 0).

-Lemma mod_IirrK G H : H <| G → cancel (@mod_Iirr G H) (@quo_Iirr G H).
+Lemma mod_IirrK G H : H <| G → cancel (@mod_Iirr G H) (@quo_Iirr G H).

Lemma quo_IirrK G H i :
-  H <| G → H \subset cfker 'chi[G]_i → mod_Iirr (quo_Iirr H i) = i.
+  H <| G → H \subset cfker 'chi[G]_i → mod_Iirr (quo_Iirr H i) = i.

Lemma quo_IirrKeq G H :
-    H <| G →
-  ∀ i, (mod_Iirr (quo_Iirr H i) == i) = (H \subset cfker 'chi[G]_i).
+    H <| G →
+  ∀ i, (mod_Iirr (quo_Iirr H i) == i) = (H \subset cfker 'chi[G]_i).

Lemma mod_Iirr_bij H G :
-  H <| G → {on [pred i | H \subset cfker 'chi_i], bijective (@mod_Iirr G H)}.
+  H <| G → {on [pred i | H \subset cfker 'chi_i], bijective (@mod_Iirr G H)}.

Lemma sum_norm_irr_quo H G x :
-    x \in G → H <| G →
-  \sum_i `|'chi[G / H]_i (coset H x)| ^+ 2
-    = \sum_(i | H \subset cfker 'chi_i) `|'chi[G]_i x| ^+ 2.
+    x \in G → H <| G →
+  \sum_i `|'chi[G / H]_i (coset H x)| ^+ 2
+    = \sum_(i | H \subset cfker 'chi_i) `|'chi[G]_i x| ^+ 2.

Lemma cap_cfker_normal G H :
-  H <| G → \bigcap_(i | H \subset cfker 'chi[G]_i) (cfker 'chi_i) = H.
+  H <| G → \bigcap_(i | H \subset cfker 'chi[G]_i) (cfker 'chi_i) = H.

-Lemma cfker_reg_quo G H : H <| G → cfker (cfReg (G / H)%g %% H) = H.
+Lemma cfker_reg_quo G H : H <| G → cfker (cfReg (G / H)%g %% H) = H.

End Coset.
@@ -1787,18 +1788,18 @@
Variable gT : finGroupType.
-Implicit Types G H : {group gT}.
+Implicit Types G H : {group gT}.

Lemma lin_irr_der1 G i :
-   ('chi_i \is a linear_char) = (G^`(1)%g \subset cfker 'chi[G]_i).
+   ('chi_i \is a linear_char) = (G^`(1)%g \subset cfker 'chi[G]_i).

-Lemma subGcfker G i : (G \subset cfker 'chi[G]_i) = (i == 0).
+Lemma subGcfker G i : (G \subset cfker 'chi[G]_i) = (i == 0).

Lemma irr_prime_injP G i :
-  prime #|G| → reflect {in G &, injective 'chi[G]_i} (i != 0).
+  prime #|G| → reflect {in G &, injective 'chi[G]_i} (i != 0).

@@ -1808,7 +1809,7 @@
Lemma cap_cfker_lin_irr G :
-  \bigcap_(i | 'chi[G]_i \is a linear_char) (cfker 'chi_i) = G^`(1)%g.
+  \bigcap_(i | 'chi[G]_i \is a linear_char) (cfker 'chi_i) = G^`(1)%g.

@@ -1818,7 +1819,7 @@
Lemma card_lin_irr G :
-  #|[pred i | 'chi[G]_i \is a linear_char]| = #|G : G^`(1)%g|.
+  #|[pred i | 'chi[G]_i \is a linear_char]| = #|G : G^`(1)%g|.
@@ -1839,8 +1840,8 @@ by apply: eq_card => i; rewrite !inE /lin_char irr_char irr1_degree -eqC_nat.
Lemma solvable_has_lin_char G :
-    G :!=: 1%g → solvable G →
-  exists2 i, 'chi[G]_i \is a linear_char & 'chi_i != 1.
+    G :!=: 1%g → solvable G →
+  exists2 i, 'chi[G]_i \is a linear_char & 'chi_i != 1.

@@ -1850,20 +1851,20 @@ by apply: eq_card => i; rewrite !inE /lin_char irr_char irr1_degree -eqC_nat.
Lemma lin_char_group G :
-  {linG : finGroupType & {cF : linG → 'CF(G) |
-         [/\ injective cF, #|linG| = #|G : G^`(1)|,
-             ∀ u, cF u \is a linear_char
-           & ∀ phi, phi \is a linear_char → ∃ u, phi = cF u]
-       & [/\ cF 1%g = 1%R,
-             {morph cF : u v / (u × v)%g >-> (u × v)%R},
-             ∀ k, {morph cF : u / (u^+ k)%g >-> u ^+ k},
-             {morph cF: u / u^-1%g >-> u^-1%CF}
-           & {mono cF: u / #[u]%g >-> #[u]%CF} ]}}.
+  {linG : finGroupType & {cF : linG → 'CF(G) |
+         [/\ injective cF, #|linG| = #|G : G^`(1)|,
+             ∀ u, cF u \is a linear_char
+           & ∀ phi, phi \is a linear_char → ∃ u, phi = cF u]
+       & [/\ cF 1%g = 1%R,
+             {morph cF : u v / (u × v)%g >-> (u × v)%R},
+             ∀ k, {morph cF : u / (u^+ k)%g >-> u ^+ k},
+             {morph cF: u / u^-1%g >-> u^-1%CF}
+           & {mono cF: u / #[u]%g >-> #[u]%CF} ]}}.

Lemma cfExp_prime_transitive G (i j : Iirr G) :
-    prime #|G| → i != 0 → j != 0 →
-  exists2 k, coprime k #['chi_i]%CF & 'chi_j = 'chi_i ^+ k.
+    prime #|G| → i != 0 → j != 0 →
+  exists2 k, coprime k #['chi_i]%CF & 'chi_j = 'chi_i ^+ k.

@@ -1873,7 +1874,7 @@ by apply: eq_card => i; rewrite !inE /lin_char irr_char irr1_degree -eqC_nat.
Lemma card_subcent1_coset G H x :
-  x \in G → H <| G → (#|'C_(G / H)[coset H x]| ≤ #|'C_G[x]|)%N.
+  x \in G → H <| G → (#|'C_(G / H)[coset H x]| ≤ #|'C_G[x]|)%N.

End DerivedGroup.
@@ -1890,16 +1891,16 @@ by apply: eq_card => i; rewrite !inE /lin_char irr_char irr1_degree -eqC_nat. Section DetOrder.

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

Section DetRepr.

-Variables (n : nat) (rG : mx_representation [fieldType of algC] G n).
+Variables (n : nat) (rG : mx_representation [fieldType of algC] G n).

-Definition det_repr_mx x : 'M_1 := (\det (rG x))%:M.
+Definition det_repr_mx x : 'M_1 := (\det (rG x))%:M.

Fact det_is_repr : mx_repr G det_repr_mx.
@@ -1909,49 +1910,49 @@ by apply: eq_card => i; rewrite !inE /lin_char irr_char irr1_degree -eqC_nat. Definition detRepr := cfRepr det_repr.

-Lemma detRepr_lin_char : detRepr \is a linear_char.
+Lemma detRepr_lin_char : detRepr \is a linear_char.

End DetRepr.

-Definition cfDet phi := \prod_i detRepr 'Chi_i ^+ truncC '[phi, 'chi[G]_i].
+Definition cfDet phi := \prod_i detRepr 'Chi_i ^+ truncC '[phi, 'chi[G]_i].

-Lemma cfDet_lin_char phi : cfDet phi \is a linear_char.
+Lemma cfDet_lin_char phi : cfDet phi \is a linear_char.

Lemma cfDetD :
-  {in character &, {morph cfDet : phi psi / phi + psi >-> phi × psi}}.
+  {in character &, {morph cfDet : phi psi / phi + psi >-> phi × psi}}.

-Lemma cfDet0 : cfDet 0 = 1.
+Lemma cfDet0 : cfDet 0 = 1.

Lemma cfDetMn k :
-  {in character, {morph cfDet : phi / phi *+ k >-> phi ^+ k}}.
+  {in character, {morph cfDet : phi / phi *+ k >-> phi ^+ k}}.

-Lemma cfDetRepr n rG : cfDet (cfRepr rG) = @detRepr n rG.
+Lemma cfDetRepr n rG : cfDet (cfRepr rG) = @detRepr n rG.

-Lemma cfDet_id xi : xi \is a linear_char → cfDet xi = xi.
+Lemma cfDet_id xi : xi \is a linear_char → cfDet xi = xi.

-Definition cfDet_order phi := #[cfDet phi]%CF.
+Definition cfDet_order phi := #[cfDet phi]%CF.

Definition cfDet_order_lin xi :
-  xi \is a linear_char → cfDet_order xi = #[xi]%CF.
+  xi \is a linear_char → cfDet_order xi = #[xi]%CF.

-Definition cfDet_order_dvdG phi : cfDet_order phi %| #|G|.
+Definition cfDet_order_dvdG phi : cfDet_order phi %| #|G|.

End DetOrder.

-Notation "''o' ( phi )" := (cfDet_order phi)
+Notation "''o' ( phi )" := (cfDet_order phi)
  (at level 8, format "''o' ( phi )") : cfun_scope.

@@ -1961,40 +1962,40 @@ by apply: eq_card => i; rewrite !inE /lin_char irr_char irr1_degree -eqC_nat. Implicit Types gT aT rT : finGroupType.

-Lemma cfDetRes gT (G H : {group gT}) phi :
-  phi \is a character → cfDet ('Res[H, G] phi) = 'Res (cfDet phi).
+Lemma cfDetRes gT (G H : {group gT}) phi :
+  phi \is a character → cfDet ('Res[H, G] phi) = 'Res (cfDet phi).

-Lemma cfDetMorph aT rT (D G : {group aT}) (f : {morphism D >-> rT})
-                (phi : 'CF(f @* G)) :
-  phi \is a character → cfDet (cfMorph phi) = cfMorph (cfDet phi).
+Lemma cfDetMorph aT rT (D G : {group aT}) (f : {morphism D >-> rT})
+                (phi : 'CF(f @* G)) :
+  phi \is a character → cfDet (cfMorph phi) = cfMorph (cfDet phi).

-Lemma cfDetIsom aT rT (G : {group aT}) (R : {group rT})
-                (f : {morphism G >-> rT}) (isoGR : isom G R f) phi :
-  cfDet (cfIsom isoGR phi) = cfIsom isoGR (cfDet phi).
+Lemma cfDetIsom aT rT (G : {group aT}) (R : {group rT})
+                (f : {morphism G >-> rT}) (isoGR : isom G R f) phi :
+  cfDet (cfIsom isoGR phi) = cfIsom isoGR (cfDet phi).

-Lemma cfDet_mul_lin gT (G : {group gT}) (lambda phi : 'CF(G)) :
-    lambda \is a linear_char → phi \is a character →
-  cfDet (lambda × phi) = lambda ^+ truncC (phi 1%g) × cfDet phi.
+Lemma cfDet_mul_lin gT (G : {group gT}) (lambda phi : 'CF(G)) :
+    lambda \is a linear_char → phi \is a character →
+  cfDet (lambda × phi) = lambda ^+ truncC (phi 1%g) × cfDet phi.

End CfDetOps.

-Definition cfcenter (gT : finGroupType) (G : {set gT}) (phi : 'CF(G)) :=
-  if phi \is a character then [set g in G | `|phi g| == phi 1%g] else cfker phi.
+Definition cfcenter (gT : finGroupType) (G : {set gT}) (phi : 'CF(G)) :=
+  if phi \is a character then [set g in G | `|phi g| == phi 1%g] else cfker phi.

-Notation "''Z' ( phi )" := (cfcenter phi) : cfun_scope.
+Notation "''Z' ( phi )" := (cfcenter phi) : cfun_scope.

Section Center.

-Variable (gT : finGroupType) (G : {group gT}).
-Implicit Types (phi chi : 'CF(G)) (H : {group gT}).
+Variable (gT : finGroupType) (G : {group gT}).
+Implicit Types (phi chi : 'CF(G)) (H : {group gT}).

@@ -2004,7 +2005,7 @@ by apply: eq_card => i; rewrite !inE /lin_char irr_char irr1_degree -eqC_nat.
Lemma cfcenter_repr n (rG : mx_representation algCF G n) :
-  'Z(cfRepr rG)%CF = rcenter rG.
+  'Z(cfRepr rG)%CF = rcenter rG.

@@ -2013,17 +2014,17 @@ by apply: eq_card => i; rewrite !inE /lin_char irr_char irr1_degree -eqC_nat. This is part of Isaacs (2.27)(b).
-Fact cfcenter_group_set phi : group_set ('Z(phi))%CF.
+Fact cfcenter_group_set phi : group_set ('Z(phi))%CF.
Canonical cfcenter_group f := Group (cfcenter_group_set f).

Lemma char_cfcenterE chi x :
-    chi \is a character → x \in G →
-  (x \in ('Z(chi))%CF) = (`|chi x| == chi 1%g).
+    chi \is a character → x \in G →
+  (x \in ('Z(chi))%CF) = (`|chi x| == chi 1%g).

Lemma irr_cfcenterE i x :
-  x \in G → (x \in 'Z('chi[G]_i)%CF) = (`|'chi_i x| == 'chi_i 1%g).
+  x \in G → (x \in 'Z('chi[G]_i)%CF) = (`|'chi_i x| == 'chi_i 1%g).

@@ -2032,13 +2033,13 @@ by apply: eq_card => i; rewrite !inE /lin_char irr_char irr1_degree -eqC_nat. This is also Isaacs (2.27)(b).
-Lemma cfcenter_sub phi : ('Z(phi))%CF \subset G.
+Lemma cfcenter_sub phi : ('Z(phi))%CF \subset G.

-Lemma cfker_center_normal phi : cfker phi <| 'Z(phi)%CF.
+Lemma cfker_center_normal phi : cfker phi <| 'Z(phi)%CF.

-Lemma cfcenter_normal phi : 'Z(phi)%CF <| G.
+Lemma cfcenter_normal phi : 'Z(phi)%CF <| G.

@@ -2048,7 +2049,7 @@ by apply: eq_card => i; rewrite !inE /lin_char irr_char irr1_degree -eqC_nat.
Lemma cfcenter_Res chi :
-  exists2 chi1, chi1 \is a linear_char & 'Res['Z(chi)%CF] chi = chi 1%g *: chi1.
+  exists2 chi1, chi1 \is a linear_char & 'Res['Z(chi)%CF] chi = chi 1%g *: chi1.

@@ -2057,7 +2058,7 @@ by apply: eq_card => i; rewrite !inE /lin_char irr_char irr1_degree -eqC_nat. This is Isaacs (2.27)(d).
-Lemma cfcenter_cyclic chi : cyclic ('Z(chi)%CF / cfker chi)%g.
+Lemma cfcenter_cyclic chi : cyclic ('Z(chi)%CF / cfker chi)%g.

@@ -2067,7 +2068,7 @@ by apply: eq_card => i; rewrite !inE /lin_char irr_char irr1_degree -eqC_nat.
Lemma cfcenter_subset_center chi :
-  ('Z(chi)%CF / cfker chi)%g \subset 'Z(G / cfker chi)%g.
+  ('Z(chi)%CF / cfker chi)%g \subset 'Z(G / cfker chi)%g.

@@ -2077,7 +2078,7 @@ by apply: eq_card => i; rewrite !inE /lin_char irr_char irr1_degree -eqC_nat.
Lemma cfcenter_eq_center (i : Iirr G) :
-  ('Z('chi_i)%CF / cfker 'chi_i)%g = 'Z(G / cfker 'chi_i)%g.
+  ('Z('chi_i)%CF / cfker 'chi_i)%g = 'Z(G / cfker 'chi_i)%g.

@@ -2086,7 +2087,7 @@ by apply: eq_card => i; rewrite !inE /lin_char irr_char irr1_degree -eqC_nat. This is Isaacs (2.28).
-Lemma cap_cfcenter_irr : \bigcap_i 'Z('chi[G]_i)%CF = 'Z(G).
+Lemma cap_cfcenter_irr : \bigcap_i 'Z('chi[G]_i)%CF = 'Z(G).

@@ -2096,8 +2097,8 @@ by apply: eq_card => i; rewrite !inE /lin_char irr_char irr1_degree -eqC_nat.
Lemma cfnorm_Res_lerif H phi :
-    H \subset G →
-  '['Res[H] phi] ≤ #|G : H|%:R × '[phi] ?= iff (phi \in 'CF(G, H)).
+    H \subset G →
+  '['Res[H] phi] ≤ #|G : H|%:R × '[phi] ?= iff (phi \in 'CF(G, H)).

@@ -2107,8 +2108,8 @@ by apply: eq_card => i; rewrite !inE /lin_char irr_char irr1_degree -eqC_nat.
Lemma irr1_bound (i : Iirr G) :
-  ('chi_i 1%g) ^+ 2 ≤ #|G : 'Z('chi_i)%CF|%:R
-                    ?= iff ('chi_i \in 'CF(G, 'Z('chi_i)%CF)).
+  ('chi_i 1%g) ^+ 2 ≤ #|G : 'Z('chi_i)%CF|%:R
+                    ?= iff ('chi_i \in 'CF(G, 'Z('chi_i)%CF)).

@@ -2118,7 +2119,7 @@ by apply: eq_card => i; rewrite !inE /lin_char irr_char irr1_degree -eqC_nat.
Lemma irr1_abelian_bound (i : Iirr G) :
-  abelian (G / 'Z('chi_i)%CF) → ('chi_i 1%g) ^+ 2 = #|G : 'Z('chi_i)%CF|%:R.
+  abelian (G / 'Z('chi_i)%CF) → ('chi_i 1%g) ^+ 2 = #|G : 'Z('chi_i)%CF|%:R.

@@ -2127,10 +2128,10 @@ by apply: eq_card => i; rewrite !inE /lin_char irr_char irr1_degree -eqC_nat. This is Isaacs (2.32)(a).
-Lemma irr_faithful_center i : cfaithful 'chi[G]_i → cyclic 'Z(G).
+Lemma irr_faithful_center i : cfaithful 'chi[G]_i → cyclic 'Z(G).

-Lemma cfcenter_fful_irr i : cfaithful 'chi[G]_i → 'Z('chi_i)%CF = 'Z(G).
+Lemma cfcenter_fful_irr i : cfaithful 'chi[G]_i → 'Z('chi_i)%CF = 'Z(G).

@@ -2139,8 +2140,8 @@ by apply: eq_card => i; rewrite !inE /lin_char irr_char irr1_degree -eqC_nat. This is Isaacs (2.32)(b).
-Lemma pgroup_cyclic_faithful (p : nat) :
-  p.-group G → cyclic 'Z(G) → ∃ i, cfaithful 'chi[G]_i.
+Lemma pgroup_cyclic_faithful (p : nat) :
+  p.-group G → cyclic 'Z(G) → ∃ i, cfaithful 'chi[G]_i.

End Center.
@@ -2149,32 +2150,32 @@ by apply: eq_card => i; rewrite !inE /lin_char irr_char irr1_degree -eqC_nat. Section Induced.

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

-Lemma cfInd_char chi : chi \is a character → 'Ind[G] chi \is a character.
+Lemma cfInd_char chi : chi \is a character → 'Ind[G] chi \is a character.

Lemma cfInd_eq0 chi :
-  H \subset G → chi \is a character → ('Ind[G] chi == 0) = (chi == 0).
+  H \subset G → chi \is a character → ('Ind[G] chi == 0) = (chi == 0).

-Lemma Ind_irr_neq0 i : H \subset G → 'Ind[G, H] 'chi_i != 0.
+Lemma Ind_irr_neq0 i : H \subset G → 'Ind[G, H] 'chi_i != 0.

-Definition Ind_Iirr (A B : {set gT}) i := cfIirr ('Ind[B, A] 'chi_i).
+Definition Ind_Iirr (A B : {set gT}) i := cfIirr ('Ind[B, A] 'chi_i).

-Lemma constt_cfRes_irr i : {j | j \in irr_constt ('Res[H, G] 'chi_i)}.
+Lemma constt_cfRes_irr i : {j | j \in irr_constt ('Res[H, G] 'chi_i)}.

Lemma constt_cfInd_irr i :
-  H \subset G → {j | j \in irr_constt ('Ind[G, H] 'chi_i)}.
+  H \subset G → {j | j \in irr_constt ('Ind[G, H] 'chi_i)}.

Lemma cfker_Res phi :
-  H \subset G → phi \is a character → cfker ('Res[H] phi) = H :&: cfker phi.
+  H \subset G → phi \is a character → cfker ('Res[H] phi) = H :&: cfker phi.

@@ -2184,12 +2185,12 @@ by apply: eq_card => i; rewrite !inE /lin_char irr_char irr1_degree -eqC_nat.
Lemma cfker_Ind chi :
-    H \subset G → chi \is a character → chi != 0 →
-  cfker ('Ind[G, H] chi) = gcore (cfker chi) G.
+    H \subset G → chi \is a character → chi != 0 →
+  cfker ('Ind[G, H] chi) = gcore (cfker chi) G.

Lemma cfker_Ind_irr i :
-  H \subset G → cfker ('Ind[G, H] 'chi_i) = gcore (cfker 'chi_i) G.
+  H \subset G → cfker ('Ind[G, H] 'chi_i) = gcore (cfker 'chi_i) G.

End Induced.
-- cgit v1.2.3