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.integral_char.html | 133 ++++++++++----------- 1 file changed, 66 insertions(+), 67 deletions(-) (limited to 'docs/htmldoc/mathcomp.character.integral_char.html') diff --git a/docs/htmldoc/mathcomp.character.integral_char.html b/docs/htmldoc/mathcomp.character.integral_char.html index 749c078..322b5ac 100644 --- a/docs/htmldoc/mathcomp.character.integral_char.html +++ b/docs/htmldoc/mathcomp.character.integral_char.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.

@@ -55,16 +54,16 @@ Local Open Scope ring_scope.

-Lemma group_num_field_exists (gT : finGroupType) (G : {group gT}) :
-  {Qn : splittingFieldType rat & galois 1 {:Qn} &
-    {QnC : {rmorphism Qn → algC}
-         & ∀ nuQn : argumentType (mem ('Gal({:Qn}%VS / 1%VS))),
-              {nu : {rmorphism algC → algC} |
-                 {morph QnC: a / nuQn a >-> nu a}}
-         & {w : Qn & #|G|.-primitive_root w ∧ <<1; w>>%VS = fullv
-              & ∀ (hT : finGroupType) (H : {group hT}) (phi : 'CF(H)),
-                       phi \is a character →
-                       ∀ x, (#[x] %| #|G|)%N → {a | QnC a = phi x}}}}.
+Lemma group_num_field_exists (gT : finGroupType) (G : {group gT}) :
+  {Qn : splittingFieldType rat & galois 1 {:Qn} &
+    {QnC : {rmorphism Qn → algC}
+         & ∀ nuQn : argumentType (mem ('Gal({:Qn}%VS / 1%VS))),
+              {nu : {rmorphism algC → algC} |
+                 {morph QnC: a / nuQn a >-> nu a}}
+         & {w : Qn & #|G|.-primitive_root w ∧ <<1; w>>%VS = fullv
+              & ∀ (hT : finGroupType) (H : {group hT}) (phi : 'CF(H)),
+                       phi \is a character →
+                       ∀ x, (#[x] %| #|G|)%N → {a | QnC a = phi x}}}}.

Section GenericClassSums.
@@ -80,37 +79,37 @@

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

-Definition gring_classM_coef_set (Ki Kj : {set gT}) g :=
-  [set xy in [predX Ki & Kj] | let: (x, y) := xy in x × y == g]%g.
+Definition gring_classM_coef_set (Ki Kj : {set gT}) g :=
+  [set xy in [predX Ki & Kj] | let: (x, y) := xy in x × y == g]%g.

-Definition gring_classM_coef (i j k : 'I_#|classes G|) :=
-  #|gring_classM_coef_set (enum_val i) (enum_val j) (repr (enum_val k))|.
+Definition gring_classM_coef (i j k : 'I_#|classes G|) :=
+  #|gring_classM_coef_set (enum_val i) (enum_val j) (repr (enum_val k))|.

-Definition gring_class_sum (i : 'I_#|classes G|) := gset_mx F G (enum_val i).
+Definition gring_class_sum (i : 'I_#|classes G|) := gset_mx F G (enum_val i).


-Lemma gring_class_sum_central i : ('K_i \in 'Z(group_ring F G))%MS.
+Lemma gring_class_sum_central i : ('K_i \in 'Z(group_ring F G))%MS.

-Lemma set_gring_classM_coef (i j k : 'I_#|classes G|) g :
-    g \in enum_val k →
-  a i j k = #|gring_classM_coef_set (enum_val i) (enum_val j) g|.
+Lemma set_gring_classM_coef (i j k : 'I_#|classes G|) g :
+    g \in enum_val k →
+  a i j k = #|gring_classM_coef_set (enum_val i) (enum_val j) g|.

-Theorem gring_classM_expansion i j : 'K_i ×m 'K_j = \sum_k (a i j k)%:R *: 'K_k.
+Theorem gring_classM_expansion i j : 'K_i ×m 'K_j = \sum_k (a i j k)%:R *: 'K_k.

-Fact gring_irr_mode_key : unit.
-Definition gring_irr_mode_def (i : Iirr G) := ('chi_i 1%g)^-1 *: 'chi_i.
-Definition gring_irr_mode := locked_with gring_irr_mode_key gring_irr_mode_def.
-Canonical gring_irr_mode_unlockable := [unlockable fun gring_irr_mode].
+Fact gring_irr_mode_key : unit.
+Definition gring_irr_mode_def (i : Iirr G) := ('chi_i 1%g)^-1 *: 'chi_i.
+Definition gring_irr_mode := locked_with gring_irr_mode_key gring_irr_mode_def.
+Canonical gring_irr_mode_unlockable := [unlockable fun gring_irr_mode].

End GenericClassSums.
@@ -118,18 +117,18 @@

-Notation "''K_' i" := (gring_class_sum _ i)
+Notation "''K_' i" := (gring_class_sum _ i)
  (at level 8, i at level 2, format "''K_' i") : ring_scope.

-Notation "''omega_' i [ A ]" := (xcfun (gring_irr_mode i) A)
+Notation "''omega_' i [ A ]" := (xcfun (gring_irr_mode i) A)
   (at level 8, i at level 2, format "''omega_' i [ A ]") : ring_scope.

Section IntegralChar.

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

@@ -138,10 +137,10 @@ This is Isaacs, Corollary (3.6).
-Lemma Aint_char (chi : 'CF(G)) x : chi \is a character → chi x \in Aint.
+Lemma Aint_char (chi : 'CF(G)) x : chi \is a character → chi x \in Aint.

-Lemma Aint_irr i x : 'chi[G]_i x \in Aint.
+Lemma Aint_irr i x : 'chi[G]_i x \in Aint.

@@ -153,7 +152,7 @@
Lemma mx_irr_gring_op_center_scalar n (rG : mx_representation algCfield G n) A :
-  mx_irreducible rG → (A \in 'Z(R_G))%MS → is_scalar_mx (gring_op rG A).
+  mx_irreducible rG → (A \in 'Z(R_G))%MS → is_scalar_mx (gring_op rG A).

Section GringIrrMode.
@@ -163,24 +162,24 @@
Let n := irr_degree (socle_of_Iirr i).
-Let mxZn_inj: injective (@scalar_mx algCfield n).
+Let mxZn_inj: injective (@scalar_mx algCfield n).

Lemma cfRepr_gring_center n1 (rG : mx_representation algCfield G n1) A :
-  cfRepr rG = 'chi_i → (A \in 'Z(R_G))%MS → gring_op rG A = 'omega_i[A]%:M.
+  cfRepr rG = 'chi_i → (A \in 'Z(R_G))%MS → gring_op rG A = 'omega_i[A]%:M.

Lemma irr_gring_center A :
-  (A \in 'Z(R_G))%MS → gring_op 'Chi_i A = 'omega_i[A]%:M.
+  (A \in 'Z(R_G))%MS → gring_op 'Chi_i A = 'omega_i[A]%:M.

Lemma gring_irr_modeM A B :
-    (A \in 'Z(R_G))%MS → (B \in 'Z(R_G))%MS →
-  'omega_i[A ×m B] = 'omega_i[A] × 'omega_i[B].
+    (A \in 'Z(R_G))%MS → (B \in 'Z(R_G))%MS →
+  'omega_i[A ×m B] = 'omega_i[A] × 'omega_i[B].

-Lemma gring_mode_class_sum_eq (k : 'I_#|classes G|) g :
-  g \in enum_val k → 'omega_i['K_k] = #|g ^: G|%:R × 'chi_i g / 'chi_i 1%g.
+Lemma gring_mode_class_sum_eq (k : 'I_#|classes G|) g :
+  g \in enum_val k → 'omega_i['K_k] = #|g ^: G|%:R × 'chi_i g / 'chi_i 1%g.

@@ -189,7 +188,7 @@ This is Isaacs, Theorem (3.7).
-Lemma Aint_gring_mode_class_sum k : 'omega_i['K_k] \in Aint.
+Lemma Aint_gring_mode_class_sum k : 'omega_i['K_k] \in Aint.

@@ -199,7 +198,7 @@
Corollary Aint_class_div_irr1 x :
-  x \in G → #|x ^: G|%:R × 'chi_i x / 'chi_i 1%g \in Aint.
+  x \in G → #|x ^: G|%:R × 'chi_i x / 'chi_i 1%g \in Aint.

@@ -209,8 +208,8 @@
Theorem coprime_degree_support_cfcenter g :
-    coprime (truncC ('chi_i 1%g)) #|g ^: G| → g \notin ('Z('chi_i))%CF →
-  'chi_i g = 0.
+    coprime (truncC ('chi_i 1%g)) #|g ^: G| → g \notin ('Z('chi_i))%CF →
+  'chi_i g = 0.

End GringIrrMode.
@@ -223,7 +222,7 @@
Theorem primes_class_simple_gt1 C :
-  simple G → ~~ abelian G → C \in (classes G)^# → (size (primes #|C|) > 1)%N.
+  simple G → ~~ abelian G → C \in (classes G)^# → (size (primes #|C|) > 1)%N.

End IntegralChar.
@@ -241,8 +240,8 @@ This is Burnside's famous p^a.q^b theorem (Isaacs, Theorem (3.10)).
-Theorem Burnside_p_a_q_b gT (G : {group gT}) :
-  (size (primes #|G|) ≤ 2)%N → solvable G.
+Theorem Burnside_p_a_q_b gT (G : {group gT}) :
+  (size (primes #|G|) ≤ 2)%N → solvable G.

@@ -251,7 +250,7 @@ This is Isaacs, Theorem (3.11).
-Theorem dvd_irr1_cardG gT (G : {group gT}) i : ('chi[G]_i 1%g %| #|G|)%C.
+Theorem dvd_irr1_cardG gT (G : {group gT}) i : ('chi[G]_i 1%g %| #|G|)%C.

@@ -260,8 +259,8 @@ This is Isaacs, Theorem (3.12).
-Theorem dvd_irr1_index_center gT (G : {group gT}) i :
-  ('chi[G]_i 1%g %| #|G : 'Z('chi_i)%CF|)%C.
+Theorem dvd_irr1_index_center gT (G : {group gT}) i :
+  ('chi[G]_i 1%g %| #|G : 'Z('chi_i)%CF|)%C.

@@ -270,11 +269,11 @@ This is Isaacs, Problem (3.7).
-Lemma gring_classM_coef_sum_eq gT (G : {group gT}) j1 j2 k g1 g2 g :
+Lemma gring_classM_coef_sum_eq gT (G : {group gT}) j1 j2 k g1 g2 g :
   let a := @gring_classM_coef gT G j1 j2 in let a_k := a k in
-   g1 \in enum_val j1 → g2 \in enum_val j2 → g \in enum_val k →
-   let sum12g := \sum_i 'chi[G]_i g1 × 'chi_i g2 × ('chi_i g)^* / 'chi_i 1%g in
-  a_k%:R = (#|enum_val j1| × #|enum_val j2|)%:R / #|G|%:R × sum12g.
+   g1 \in enum_val j1 → g2 \in enum_val j2 → g \in enum_val k →
+   let sum12g := \sum_i 'chi[G]_i g1 × 'chi_i g2 × ('chi_i g)^* / 'chi_i 1%g in
+  a_k%:R = (#|enum_val j1| × #|enum_val j2|)%:R / #|G|%:R × sum12g.

@@ -283,10 +282,10 @@ This is Isaacs, Problem (2.16).
-Lemma index_support_dvd_degree gT (G H : {group gT}) chi :
-    H \subset G → chi \is a character → chi \in 'CF(G, H) →
-    (H :==: 1%g) || abelian G →
-  (#|G : H| %| chi 1%g)%C.
+Lemma index_support_dvd_degree gT (G H : {group gT}) chi :
+    H \subset G → chi \is a character → chi \in 'CF(G, H) →
+    (H :==: 1%g) || abelian G →
+  (#|G : H| %| chi 1%g)%C.

@@ -295,10 +294,10 @@ This is Isaacs, Theorem (3.13).
-Theorem faithful_degree_p_part gT (p : nat) (G P : {group gT}) i :
-    cfaithful 'chi[G]_i → p.-nat (truncC ('chi_i 1%g)) →
-    p.-Sylow(G) P → abelian P →
-  'chi_i 1%g = (#|G : 'Z(G)|`_p)%:R.
+Theorem faithful_degree_p_part gT (p : nat) (G P : {group gT}) i :
+    cfaithful 'chi[G]_i → p.-nat (truncC ('chi_i 1%g)) →
+    p.-Sylow(G) P → abelian P →
+  'chi_i 1%g = (#|G : 'Z(G)|`_p)%:R.

@@ -309,10 +308,10 @@ empty if this is not the case.
-Lemma sum_norm2_char_generators gT (G : {group gT}) (chi : 'CF(G)) :
-    let S := [pred s | generator G s] in
-    chi \is a character → {in S, ∀ s, chi s != 0} →
-  \sum_(s in S) `|chi s| ^+ 2 ≥ #|S|%:R.
+Lemma sum_norm2_char_generators gT (G : {group gT}) (chi : 'CF(G)) :
+    let S := [pred s | generator G s] in
+    chi \is a character → {in S, ∀ s, chi s != 0} →
+  \sum_(s in S) `|chi s| ^+ 2 ≥ #|S|%:R.

@@ -321,8 +320,8 @@ This is Burnside's vanishing theorem (Isaacs, Theorem (3.15)).
-Theorem nonlinear_irr_vanish gT (G : {group gT}) i :
-  'chi[G]_i 1%g > 1 → exists2 x, x \in G & 'chi_i x = 0.
+Theorem nonlinear_irr_vanish gT (G : {group gT}) i :
+  'chi[G]_i 1%g > 1 → exists2 x, x \in G & 'chi_i x = 0.

End MoreIntegralChar.
-- cgit v1.2.3