diff options
Diffstat (limited to 'docs/htmldoc/mathcomp.character.integral_char.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.character.integral_char.html | 338 |
1 files changed, 0 insertions, 338 deletions
diff --git a/docs/htmldoc/mathcomp.character.integral_char.html b/docs/htmldoc/mathcomp.character.integral_char.html deleted file mode 100644 index 322b5ac..0000000 --- a/docs/htmldoc/mathcomp.character.integral_char.html +++ /dev/null @@ -1,338 +0,0 @@ -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" -"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> -<html xmlns="http://www.w3.org/1999/xhtml"> -<head> -<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> -<link href="coqdoc.css" rel="stylesheet" type="text/css" /> -<title>mathcomp.character.integral_char</title> -</head> - -<body> - -<div id="page"> - -<div id="header"> -</div> - -<div id="main"> - -<h1 class="libtitle">Library mathcomp.character.integral_char</h1> - -<div class="code"> -<span class="comment">(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. <br/> - Distributed under the terms of CeCILL-B. *)</span><br/> - -<br/> -</div> - -<div class="doc"> - This file provides some standard results based on integrality properties - of characters, such as theorem asserting that the degree of an irreducible - character of G divides the order of G (Isaacs 3.11), or the famous p^a.q^b - solvability theorem of Burnside. - Defined here: - 'K_k == the kth class sum in gring F G, where k : 'I#|classes G|, and - F is inferred from the context. - := gset_mx F G (enum_val k) (see mxrepresentation.v). - --> The 'K_k form a basis of 'Z(group_ring F G)%%MS. - gring_classM_coef i j k == the coordinate of 'K_i *m 'K_j on 'K_k; this - is usually abbreviated as a i j k. - gring_classM_coef_set A B z == the set of all (x, y) in setX A B such - that x * y = z; if A and B are respectively the ith and jth - conjugacy class of G, and z is in the kth conjugacy class, then - gring_classM_coef i j k is exactly the cardinal of this set. - 'omega_i<span class="inlinecode">#<span class="id" title="var">A</span>#</span> == the mode of 'chi<span class="inlinecode">#<span class="id" title="var">G</span>#</span>#<i>i on (A \in 'Z(group_ring algC G))%MS, - i.e., the z such that gring_op 'Chi_i A = z%:M. -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Set Implicit Arguments</span>.<br/> - -<br/> -<span class="id" title="keyword">Import</span> <span class="id" title="var">GroupScope</span> <span class="id" title="var">GRing.Theory</span> <span class="id" title="var">Num.Theory</span>.<br/> -<span class="id" title="keyword">Local Open</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">ring_scope</span>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="group_num_field_exists"><span class="id" title="lemma">group_num_field_exists</span></a> (<span class="id" title="var">gT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.character.integral_char.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) :<br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#2d3f7aca3c5e595bced87000c0854440"><span class="id" title="notation">{</span></a><span class="id" title="var">Qn</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#2d3f7aca3c5e595bced87000c0854440"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.field.galois.html#SplittingField.Exports.splittingFieldType"><span class="id" title="abbreviation">splittingFieldType</span></a> <a class="idref" href="mathcomp.algebra.rat.html#rat"><span class="id" title="record">rat</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#2d3f7aca3c5e595bced87000c0854440"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.field.galois.html#galois"><span class="id" title="definition">galois</span></a> 1 <a class="idref" href="mathcomp.algebra.vector.html#6a45c77a68f1019c1f3b35b71c415ac8"><span class="id" title="notation">{:</span></a><a class="idref" href="mathcomp.character.integral_char.html#Qn"><span class="id" title="variable">Qn</span></a><a class="idref" href="mathcomp.algebra.vector.html#6a45c77a68f1019c1f3b35b71c415ac8"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#2d3f7aca3c5e595bced87000c0854440"><span class="id" title="notation">&</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#2d3f7aca3c5e595bced87000c0854440"><span class="id" title="notation">{</span></a><span class="id" title="var">QnC</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#2d3f7aca3c5e595bced87000c0854440"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">rmorphism</span></a> <a class="idref" href="mathcomp.character.integral_char.html#Qn"><span class="id" title="variable">Qn</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">}</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#2d3f7aca3c5e595bced87000c0854440"><span class="id" title="notation">&</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">nuQn</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#argumentType"><span class="id" title="definition">argumentType</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> (<a class="idref" href="mathcomp.field.galois.html#1f007a2c34bca981c8e1e44634ce1d47"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.field.galois.html#1f007a2c34bca981c8e1e44634ce1d47"><span class="id" title="notation">Gal</span></a><a class="idref" href="mathcomp.field.galois.html#1f007a2c34bca981c8e1e44634ce1d47"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.vector.html#6a45c77a68f1019c1f3b35b71c415ac8"><span class="id" title="notation">{:</span></a><a class="idref" href="mathcomp.character.integral_char.html#Qn"><span class="id" title="variable">Qn</span></a><a class="idref" href="mathcomp.algebra.vector.html#6a45c77a68f1019c1f3b35b71c415ac8"><span class="id" title="notation">}</span></a>%<span class="id" title="var">VS</span> <a class="idref" href="mathcomp.field.galois.html#1f007a2c34bca981c8e1e44634ce1d47"><span class="id" title="notation">/</span></a> 1%<span class="id" title="var">VS</span><a class="idref" href="mathcomp.field.galois.html#1f007a2c34bca981c8e1e44634ce1d47"><span class="id" title="notation">)</span></a>)),<br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#6556914db359db999889decec6a4a562"><span class="id" title="notation">{</span></a><span class="id" title="var">nu</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#6556914db359db999889decec6a4a562"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">rmorphism</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algC"><span class="id" title="abbreviation">algC</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#6556914db359db999889decec6a4a562"><span class="id" title="notation">|</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.character.integral_char.html#QnC"><span class="id" title="variable">QnC</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">:</span></a> <span class="id" title="var">a</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.character.integral_char.html#nuQn"><span class="id" title="variable">nuQn</span></a> <a class="idref" href="mathcomp.character.integral_char.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.character.integral_char.html#nu"><span class="id" title="variable">nu</span></a> <a class="idref" href="mathcomp.character.integral_char.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8bf6fdbe8b0c22b67e58fa5cd9937190"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#6556914db359db999889decec6a4a562"><span class="id" title="notation">}</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#2d3f7aca3c5e595bced87000c0854440"><span class="id" title="notation">&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#2d3f7aca3c5e595bced87000c0854440"><span class="id" title="notation">{</span></a><span class="id" title="var">w</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#2d3f7aca3c5e595bced87000c0854440"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.character.integral_char.html#Qn"><span class="id" title="variable">Qn</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#2d3f7aca3c5e595bced87000c0854440"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.character.integral_char.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.algebra.poly.html#ad6a7217bc47606779ec5b6d2378a1dd"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.algebra.poly.html#ad6a7217bc47606779ec5b6d2378a1dd"><span class="id" title="notation">primitive_root</span></a> <a class="idref" href="mathcomp.character.integral_char.html#w"><span class="id" title="variable">w</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#ba2b0e492d2b4675a0acf3ea92aabadd"><span class="id" title="notation">∧</span></a> <a class="idref" href="mathcomp.field.falgebra.html#faad1af6363310d507c72eed3dbfbc17"><span class="id" title="notation"><<</span></a>1<a class="idref" href="mathcomp.field.falgebra.html#faad1af6363310d507c72eed3dbfbc17"><span class="id" title="notation">;</span></a> <a class="idref" href="mathcomp.character.integral_char.html#w"><span class="id" title="variable">w</span></a><a class="idref" href="mathcomp.field.falgebra.html#faad1af6363310d507c72eed3dbfbc17"><span class="id" title="notation">>></span></a>%<span class="id" title="var">VS</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.vector.html#fullv"><span class="id" title="definition">fullv</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#2d3f7aca3c5e595bced87000c0854440"><span class="id" title="notation">&</span></a> <span class="id" title="keyword">∀</span> (<span class="id" title="var">hT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<span class="id" title="var">H</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.character.integral_char.html#hT"><span class="id" title="variable">hT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">phi</span> : <a class="idref" href="mathcomp.character.classfun.html#5112e587c59fdaca05e10d1764f09c4c"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.classfun.html#5112e587c59fdaca05e10d1764f09c4c"><span class="id" title="notation">CF</span></a><a class="idref" href="mathcomp.character.classfun.html#5112e587c59fdaca05e10d1764f09c4c"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.character.integral_char.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.character.classfun.html#5112e587c59fdaca05e10d1764f09c4c"><span class="id" title="notation">)</span></a>),<br/> - <a class="idref" href="mathcomp.character.integral_char.html#phi"><span class="id" title="variable">phi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">is</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">a</span></a> <a class="idref" href="mathcomp.character.character.html#character"><span class="id" title="definition">character</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, (<a class="idref" href="mathcomp.fingroup.fingroup.html#09508509373ff3217fbbadb14d25dc5c"><span class="id" title="notation">#[</span></a><a class="idref" href="mathcomp.character.integral_char.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#09508509373ff3217fbbadb14d25dc5c"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#bde82eab2fe4a0799bc2419e587505d4"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.character.integral_char.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a>)%<span class="id" title="var">N</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><span class="id" title="notation">{</span></a><span class="id" title="var">a</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.character.integral_char.html#QnC"><span class="id" title="variable">QnC</span></a> <a class="idref" href="mathcomp.character.integral_char.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.character.integral_char.html#phi"><span class="id" title="variable">phi</span></a> <a class="idref" href="mathcomp.character.integral_char.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#2d3f7aca3c5e595bced87000c0854440"><span class="id" title="notation">}}}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="GenericClassSums"><span class="id" title="section">GenericClassSums</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - This is Isaacs, Theorem (2.4), generalized to an arbitrary field, and with - the combinatorial definition of the coeficients exposed. - This part could move to mxrepresentation. -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Variable</span> (<a name="GenericClassSums.gT"><span class="id" title="variable">gT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<a name="GenericClassSums.G"><span class="id" title="variable">G</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.character.integral_char.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) (<a name="GenericClassSums.F"><span class="id" title="variable">F</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Field.Exports.fieldType"><span class="id" title="abbreviation">fieldType</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="gring_classM_coef_set"><span class="id" title="definition">gring_classM_coef_set</span></a> (<span class="id" title="var">Ki</span> <span class="id" title="var">Kj</span> : <a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.character.integral_char.html#GenericClassSums.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>) <span class="id" title="var">g</span> :=<br/> - <a class="idref" href="mathcomp.ssreflect.finset.html#91816551bcea1b6f359ecf76f3595e38"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#91816551bcea1b6f359ecf76f3595e38"><span class="id" title="notation">set</span></a> <span class="id" title="var">xy</span> <a class="idref" href="mathcomp.ssreflect.finset.html#91816551bcea1b6f359ecf76f3595e38"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#a3b642bc5072eac3f8d0c73615125d00"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#a3b642bc5072eac3f8d0c73615125d00"><span class="id" title="notation">predX</span></a> <a class="idref" href="mathcomp.character.integral_char.html#Ki"><span class="id" title="variable">Ki</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#a3b642bc5072eac3f8d0c73615125d00"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.character.integral_char.html#Kj"><span class="id" title="variable">Kj</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#a3b642bc5072eac3f8d0c73615125d00"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#91816551bcea1b6f359ecf76f3595e38"><span class="id" title="notation">|</span></a> <span class="id" title="keyword">let</span>: <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <span class="id" title="var">y</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> := <a class="idref" href="mathcomp.character.integral_char.html#xy"><span class="id" title="variable">xy</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">x</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#8b8794efbfbae1b793d9cb62ce802285"><span class="id" title="notation">×</span></a> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.character.integral_char.html#g"><span class="id" title="variable">g</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#91816551bcea1b6f359ecf76f3595e38"><span class="id" title="notation">]</span></a>%<span class="id" title="var">g</span>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="gring_classM_coef"><span class="id" title="definition">gring_classM_coef</span></a> (<span class="id" title="var">i</span> <span class="id" title="var">j</span> <span class="id" title="var">k</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#classes"><span class="id" title="definition">classes</span></a> <a class="idref" href="mathcomp.character.integral_char.html#GenericClassSums.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a>) :=<br/> - <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.character.integral_char.html#gring_classM_coef_set"><span class="id" title="definition">gring_classM_coef_set</span></a> (<a class="idref" href="mathcomp.ssreflect.fintype.html#enum_val"><span class="id" title="definition">enum_val</span></a> <a class="idref" href="mathcomp.character.integral_char.html#i"><span class="id" title="variable">i</span></a>) (<a class="idref" href="mathcomp.ssreflect.fintype.html#enum_val"><span class="id" title="definition">enum_val</span></a> <a class="idref" href="mathcomp.character.integral_char.html#j"><span class="id" title="variable">j</span></a>) (<a class="idref" href="mathcomp.fingroup.fingroup.html#repr"><span class="id" title="definition">repr</span></a> (<a class="idref" href="mathcomp.ssreflect.fintype.html#enum_val"><span class="id" title="definition">enum_val</span></a> <a class="idref" href="mathcomp.character.integral_char.html#k"><span class="id" title="variable">k</span></a>))<a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="gring_class_sum"><span class="id" title="definition">gring_class_sum</span></a> (<span class="id" title="var">i</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#classes"><span class="id" title="definition">classes</span></a> <a class="idref" href="mathcomp.character.integral_char.html#GenericClassSums.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a>) := <a class="idref" href="mathcomp.character.mxrepresentation.html#gset_mx"><span class="id" title="definition">gset_mx</span></a> <a class="idref" href="mathcomp.character.integral_char.html#GenericClassSums.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.character.integral_char.html#GenericClassSums.G"><span class="id" title="variable">G</span></a> (<a class="idref" href="mathcomp.ssreflect.fintype.html#enum_val"><span class="id" title="definition">enum_val</span></a> <a class="idref" href="mathcomp.character.integral_char.html#i"><span class="id" title="variable">i</span></a>).<br/> - -<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="gring_class_sum_central"><span class="id" title="lemma">gring_class_sum_central</span></a> <span class="id" title="var">i</span> : (<a class="idref" href="mathcomp.character.integral_char.html#f80e99a2407abb4198f6e6b914561060"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.integral_char.html#f80e99a2407abb4198f6e6b914561060"><span class="id" title="notation">K_i</span></a> <a class="idref" href="mathcomp.algebra.mxalgebra.html#b07e6617bc8db0b83b350e09f8851b51"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#b07e6617bc8db0b83b350e09f8851b51"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.mxalgebra.html#c6c995a25415413a47df0a8d4a5b9d94"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#c6c995a25415413a47df0a8d4a5b9d94"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#c6c995a25415413a47df0a8d4a5b9d94"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.character.mxrepresentation.html#group_ring"><span class="id" title="definition">group_ring</span></a> <a class="idref" href="mathcomp.character.integral_char.html#GenericClassSums.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.character.integral_char.html#GenericClassSums.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#c6c995a25415413a47df0a8d4a5b9d94"><span class="id" title="notation">)</span></a>)%<span class="id" title="var">MS</span>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="set_gring_classM_coef"><span class="id" title="lemma">set_gring_classM_coef</span></a> (<span class="id" title="var">i</span> <span class="id" title="var">j</span> <span class="id" title="var">k</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#classes"><span class="id" title="definition">classes</span></a> <a class="idref" href="mathcomp.character.integral_char.html#GenericClassSums.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a>) <span class="id" title="var">g</span> :<br/> - <a class="idref" href="mathcomp.character.integral_char.html#g"><span class="id" title="variable">g</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#enum_val"><span class="id" title="definition">enum_val</span></a> <a class="idref" href="mathcomp.character.integral_char.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.character.integral_char.html#a"><span class="id" title="abbreviation">a</span></a> <a class="idref" href="mathcomp.character.integral_char.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.character.integral_char.html#j"><span class="id" title="variable">j</span></a> <a class="idref" href="mathcomp.character.integral_char.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.character.integral_char.html#gring_classM_coef_set"><span class="id" title="definition">gring_classM_coef_set</span></a> (<a class="idref" href="mathcomp.ssreflect.fintype.html#enum_val"><span class="id" title="definition">enum_val</span></a> <a class="idref" href="mathcomp.character.integral_char.html#i"><span class="id" title="variable">i</span></a>) (<a class="idref" href="mathcomp.ssreflect.fintype.html#enum_val"><span class="id" title="definition">enum_val</span></a> <a class="idref" href="mathcomp.character.integral_char.html#j"><span class="id" title="variable">j</span></a>) <a class="idref" href="mathcomp.character.integral_char.html#g"><span class="id" title="variable">g</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Theorem</span> <a name="gring_classM_expansion"><span class="id" title="lemma">gring_classM_expansion</span></a> <span class="id" title="var">i</span> <span class="id" title="var">j</span> : <a class="idref" href="mathcomp.character.integral_char.html#f80e99a2407abb4198f6e6b914561060"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.integral_char.html#f80e99a2407abb4198f6e6b914561060"><span class="id" title="notation">K_i</span></a> <a class="idref" href="mathcomp.algebra.matrix.html#b2b431de65e6c1e23c1ae3a60262ea15"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.algebra.matrix.html#b2b431de65e6c1e23c1ae3a60262ea15"><span class="id" title="notation">m</span></a> <a class="idref" href="mathcomp.character.integral_char.html#f80e99a2407abb4198f6e6b914561060"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.integral_char.html#f80e99a2407abb4198f6e6b914561060"><span class="id" title="notation">K_j</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#de3e30c288f66ee879ea2b40e81e186c"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#de3e30c288f66ee879ea2b40e81e186c"><span class="id" title="notation">sum_k</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#6411ed08724033ae48d2865f0380d533"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.character.integral_char.html#a"><span class="id" title="abbreviation">a</span></a> <a class="idref" href="mathcomp.character.integral_char.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.character.integral_char.html#j"><span class="id" title="variable">j</span></a> <a class="idref" href="mathcomp.character.integral_char.html#k"><span class="id" title="variable">k</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#6411ed08724033ae48d2865f0380d533"><span class="id" title="notation">)%:</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#6411ed08724033ae48d2865f0380d533"><span class="id" title="notation">R</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#3b05480e39db306e67fadbc79d394529"><span class="id" title="notation">*:</span></a> <a class="idref" href="mathcomp.character.integral_char.html#f80e99a2407abb4198f6e6b914561060"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.integral_char.html#f80e99a2407abb4198f6e6b914561060"><span class="id" title="notation">K_k</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Fact</span> <a name="gring_irr_mode_key"><span class="id" title="lemma">gring_irr_mode_key</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a>. <br/> -<span class="id" title="keyword">Definition</span> <a name="gring_irr_mode_def"><span class="id" title="definition">gring_irr_mode_def</span></a> (<span class="id" title="var">i</span> : <a class="idref" href="mathcomp.character.character.html#Iirr"><span class="id" title="abbreviation">Iirr</span></a> <a class="idref" href="mathcomp.character.integral_char.html#GenericClassSums.G"><span class="id" title="variable">G</span></a>) := <a class="idref" href="mathcomp.algebra.ssralg.html#4e5a4c91ec0aa12de06dfe1cc07ea126"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">chi_i</span></a> 1%<span class="id" title="var">g</span><a class="idref" href="mathcomp.algebra.ssralg.html#4e5a4c91ec0aa12de06dfe1cc07ea126"><span class="id" title="notation">)^-1</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#3b05480e39db306e67fadbc79d394529"><span class="id" title="notation">*:</span></a> <a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">chi_i</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="gring_irr_mode"><span class="id" title="definition">gring_irr_mode</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#locked_with"><span class="id" title="definition">locked_with</span></a> <a class="idref" href="mathcomp.character.integral_char.html#gring_irr_mode_key"><span class="id" title="lemma">gring_irr_mode_key</span></a> <a class="idref" href="mathcomp.character.integral_char.html#gring_irr_mode_def"><span class="id" title="definition">gring_irr_mode_def</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">gring_irr_mode_unlockable</span> := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#84464b412faf5a30a7c5c6423d9b3956"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#84464b412faf5a30a7c5c6423d9b3956"><span class="id" title="notation">unlockable</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#84464b412faf5a30a7c5c6423d9b3956"><span class="id" title="notation">fun</span></a> <a class="idref" href="mathcomp.character.integral_char.html#gring_irr_mode"><span class="id" title="definition">gring_irr_mode</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#84464b412faf5a30a7c5c6423d9b3956"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.character.integral_char.html#GenericClassSums"><span class="id" title="section">GenericClassSums</span></a>.<br/> - -<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="c1b1dbde1d9ee51a0617fc81ec28c4a8"><span class="id" title="notation">"</span></a>''K_' i" := (<a class="idref" href="mathcomp.character.integral_char.html#gring_class_sum"><span class="id" title="definition">gring_class_sum</span></a> <span class="id" title="var">_</span> <span class="id" title="var">i</span>)<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8, <span class="id" title="var">i</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">format</span> "''K_' i") : <span class="id" title="var">ring_scope</span>.<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="2d1412558d708665ab38bdd05f3b1341"><span class="id" title="notation">"</span></a>''omega_' i [ A ]" := (<a class="idref" href="mathcomp.character.character.html#xcfun"><span class="id" title="definition">xcfun</span></a> (<a class="idref" href="mathcomp.character.integral_char.html#gring_irr_mode"><span class="id" title="definition">gring_irr_mode</span></a> <span class="id" title="var">i</span>) <span class="id" title="var">A</span>)<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8, <span class="id" title="var">i</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">format</span> "''omega_' i [ A ]") : <span class="id" title="var">ring_scope</span>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="IntegralChar"><span class="id" title="section">IntegralChar</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="IntegralChar.gT"><span class="id" title="variable">gT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<a name="IntegralChar.G"><span class="id" title="variable">G</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.character.integral_char.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>).<br/> - -<br/> -</div> - -<div class="doc"> - This is Isaacs, Corollary (3.6). -</div> -<div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="Aint_char"><span class="id" title="lemma">Aint_char</span></a> (<span class="id" title="var">chi</span> : <a class="idref" href="mathcomp.character.classfun.html#5112e587c59fdaca05e10d1764f09c4c"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.classfun.html#5112e587c59fdaca05e10d1764f09c4c"><span class="id" title="notation">CF</span></a><a class="idref" href="mathcomp.character.classfun.html#5112e587c59fdaca05e10d1764f09c4c"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.character.integral_char.html#IntegralChar.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.character.classfun.html#5112e587c59fdaca05e10d1764f09c4c"><span class="id" title="notation">)</span></a>) <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.character.integral_char.html#chi"><span class="id" title="variable">chi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">is</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">a</span></a> <a class="idref" href="mathcomp.character.character.html#character"><span class="id" title="definition">character</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.character.integral_char.html#chi"><span class="id" title="variable">chi</span></a> <a class="idref" href="mathcomp.character.integral_char.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.algnum.html#Aint"><span class="id" title="definition">Aint</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Aint_irr"><span class="id" title="lemma">Aint_irr</span></a> <span class="id" title="var">i</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.character.character.html#7d5ba9be6923d4bf4a568a8a939b7ab0"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#7d5ba9be6923d4bf4a568a8a939b7ab0"><span class="id" title="notation">chi</span></a><a class="idref" href="mathcomp.character.character.html#7d5ba9be6923d4bf4a568a8a939b7ab0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.character.integral_char.html#IntegralChar.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.character.character.html#7d5ba9be6923d4bf4a568a8a939b7ab0"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.character.character.html#7d5ba9be6923d4bf4a568a8a939b7ab0"><span class="id" title="notation">_i</span></a> <a class="idref" href="mathcomp.character.integral_char.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.algnum.html#Aint"><span class="id" title="definition">Aint</span></a>.<br/> - -<br/> - -<br/> -</div> - -<div class="doc"> - This is Isaacs (2.25). -</div> -<div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="mx_irr_gring_op_center_scalar"><span class="id" title="lemma">mx_irr_gring_op_center_scalar</span></a> <span class="id" title="var">n</span> (<span class="id" title="var">rG</span> : <a class="idref" href="mathcomp.character.mxrepresentation.html#mx_representation"><span class="id" title="record">mx_representation</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algCfield"><span class="id" title="abbreviation">algCfield</span></a> <a class="idref" href="mathcomp.character.integral_char.html#IntegralChar.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.character.integral_char.html#n"><span class="id" title="variable">n</span></a>) <span class="id" title="var">A</span> :<br/> - <a class="idref" href="mathcomp.character.mxrepresentation.html#mx_irreducible"><span class="id" title="definition">mx_irreducible</span></a> <a class="idref" href="mathcomp.character.integral_char.html#rG"><span class="id" title="variable">rG</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> (<a class="idref" href="mathcomp.character.integral_char.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.algebra.mxalgebra.html#b07e6617bc8db0b83b350e09f8851b51"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#b07e6617bc8db0b83b350e09f8851b51"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.mxalgebra.html#c6c995a25415413a47df0a8d4a5b9d94"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#c6c995a25415413a47df0a8d4a5b9d94"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#c6c995a25415413a47df0a8d4a5b9d94"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.character.integral_char.html#R_G"><span class="id" title="abbreviation">R_G</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#c6c995a25415413a47df0a8d4a5b9d94"><span class="id" title="notation">)</span></a>)%<span class="id" title="var">MS</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.matrix.html#is_scalar_mx"><span class="id" title="definition">is_scalar_mx</span></a> (<a class="idref" href="mathcomp.character.mxrepresentation.html#gring_op"><span class="id" title="definition">gring_op</span></a> <a class="idref" href="mathcomp.character.integral_char.html#rG"><span class="id" title="variable">rG</span></a> <a class="idref" href="mathcomp.character.integral_char.html#A"><span class="id" title="variable">A</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="IntegralChar.GringIrrMode"><span class="id" title="section">GringIrrMode</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="IntegralChar.GringIrrMode.i"><span class="id" title="variable">i</span></a> : <a class="idref" href="mathcomp.character.character.html#Iirr"><span class="id" title="abbreviation">Iirr</span></a> <a class="idref" href="mathcomp.character.integral_char.html#IntegralChar.G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Let</span> <a name="IntegralChar.GringIrrMode.n"><span class="id" title="variable">n</span></a> := <a class="idref" href="mathcomp.character.mxrepresentation.html#irr_degree"><span class="id" title="definition">irr_degree</span></a> (<a class="idref" href="mathcomp.character.character.html#socle_of_Iirr"><span class="id" title="definition">socle_of_Iirr</span></a> <a class="idref" href="mathcomp.character.integral_char.html#IntegralChar.GringIrrMode.i"><span class="id" title="variable">i</span></a>).<br/> -<span class="id" title="keyword">Let</span> <a name="IntegralChar.GringIrrMode.mxZn_inj"><span class="id" title="variable">mxZn_inj</span></a>: <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#injective"><span class="id" title="definition">injective</span></a> (@<a class="idref" href="mathcomp.algebra.matrix.html#scalar_mx"><span class="id" title="definition">scalar_mx</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algCfield"><span class="id" title="abbreviation">algCfield</span></a> <a class="idref" href="mathcomp.character.integral_char.html#IntegralChar.GringIrrMode.n"><span class="id" title="variable">n</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="cfRepr_gring_center"><span class="id" title="lemma">cfRepr_gring_center</span></a> <span class="id" title="var">n1</span> (<span class="id" title="var">rG</span> : <a class="idref" href="mathcomp.character.mxrepresentation.html#mx_representation"><span class="id" title="record">mx_representation</span></a> <a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.algCfield"><span class="id" title="abbreviation">algCfield</span></a> <a class="idref" href="mathcomp.character.integral_char.html#IntegralChar.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.character.integral_char.html#n1"><span class="id" title="variable">n1</span></a>) <span class="id" title="var">A</span> :<br/> - <a class="idref" href="mathcomp.character.character.html#cfRepr"><span class="id" title="definition">cfRepr</span></a> <a class="idref" href="mathcomp.character.integral_char.html#rG"><span class="id" title="variable">rG</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">chi_i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> (<a class="idref" href="mathcomp.character.integral_char.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.algebra.mxalgebra.html#b07e6617bc8db0b83b350e09f8851b51"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#b07e6617bc8db0b83b350e09f8851b51"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.mxalgebra.html#c6c995a25415413a47df0a8d4a5b9d94"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#c6c995a25415413a47df0a8d4a5b9d94"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#c6c995a25415413a47df0a8d4a5b9d94"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.character.integral_char.html#R_G"><span class="id" title="abbreviation">R_G</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#c6c995a25415413a47df0a8d4a5b9d94"><span class="id" title="notation">)</span></a>)%<span class="id" title="var">MS</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.character.mxrepresentation.html#gring_op"><span class="id" title="definition">gring_op</span></a> <a class="idref" href="mathcomp.character.integral_char.html#rG"><span class="id" title="variable">rG</span></a> <a class="idref" href="mathcomp.character.integral_char.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.character.integral_char.html#2d1412558d708665ab38bdd05f3b1341"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.integral_char.html#2d1412558d708665ab38bdd05f3b1341"><span class="id" title="notation">omega_i</span></a><a class="idref" href="mathcomp.character.integral_char.html#2d1412558d708665ab38bdd05f3b1341"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.character.integral_char.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.character.integral_char.html#2d1412558d708665ab38bdd05f3b1341"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.algebra.matrix.html#850c060d75891e97ece38bfec139b8ea"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.matrix.html#850c060d75891e97ece38bfec139b8ea"><span class="id" title="notation">M</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="irr_gring_center"><span class="id" title="lemma">irr_gring_center</span></a> <span class="id" title="var">A</span> :<br/> - (<a class="idref" href="mathcomp.character.integral_char.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.algebra.mxalgebra.html#b07e6617bc8db0b83b350e09f8851b51"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#b07e6617bc8db0b83b350e09f8851b51"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.mxalgebra.html#c6c995a25415413a47df0a8d4a5b9d94"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#c6c995a25415413a47df0a8d4a5b9d94"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#c6c995a25415413a47df0a8d4a5b9d94"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.character.integral_char.html#R_G"><span class="id" title="abbreviation">R_G</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#c6c995a25415413a47df0a8d4a5b9d94"><span class="id" title="notation">)</span></a>)%<span class="id" title="var">MS</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.character.mxrepresentation.html#gring_op"><span class="id" title="definition">gring_op</span></a> <a class="idref" href="mathcomp.character.character.html#862ee9dddb7503f68e86ae1b7d9d8242"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#862ee9dddb7503f68e86ae1b7d9d8242"><span class="id" title="notation">Chi_i</span></a> <a class="idref" href="mathcomp.character.integral_char.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.character.integral_char.html#2d1412558d708665ab38bdd05f3b1341"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.integral_char.html#2d1412558d708665ab38bdd05f3b1341"><span class="id" title="notation">omega_i</span></a><a class="idref" href="mathcomp.character.integral_char.html#2d1412558d708665ab38bdd05f3b1341"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.character.integral_char.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.character.integral_char.html#2d1412558d708665ab38bdd05f3b1341"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.algebra.matrix.html#850c060d75891e97ece38bfec139b8ea"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.matrix.html#850c060d75891e97ece38bfec139b8ea"><span class="id" title="notation">M</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="gring_irr_modeM"><span class="id" title="lemma">gring_irr_modeM</span></a> <span class="id" title="var">A</span> <span class="id" title="var">B</span> :<br/> - (<a class="idref" href="mathcomp.character.integral_char.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.algebra.mxalgebra.html#b07e6617bc8db0b83b350e09f8851b51"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#b07e6617bc8db0b83b350e09f8851b51"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.mxalgebra.html#c6c995a25415413a47df0a8d4a5b9d94"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#c6c995a25415413a47df0a8d4a5b9d94"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#c6c995a25415413a47df0a8d4a5b9d94"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.character.integral_char.html#R_G"><span class="id" title="abbreviation">R_G</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#c6c995a25415413a47df0a8d4a5b9d94"><span class="id" title="notation">)</span></a>)%<span class="id" title="var">MS</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> (<a class="idref" href="mathcomp.character.integral_char.html#B"><span class="id" title="variable">B</span></a> <a class="idref" href="mathcomp.algebra.mxalgebra.html#b07e6617bc8db0b83b350e09f8851b51"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#b07e6617bc8db0b83b350e09f8851b51"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.mxalgebra.html#c6c995a25415413a47df0a8d4a5b9d94"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#c6c995a25415413a47df0a8d4a5b9d94"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#c6c995a25415413a47df0a8d4a5b9d94"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.character.integral_char.html#R_G"><span class="id" title="abbreviation">R_G</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#c6c995a25415413a47df0a8d4a5b9d94"><span class="id" title="notation">)</span></a>)%<span class="id" title="var">MS</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.character.integral_char.html#2d1412558d708665ab38bdd05f3b1341"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.integral_char.html#2d1412558d708665ab38bdd05f3b1341"><span class="id" title="notation">omega_i</span></a><a class="idref" href="mathcomp.character.integral_char.html#2d1412558d708665ab38bdd05f3b1341"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.character.integral_char.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.algebra.matrix.html#b2b431de65e6c1e23c1ae3a60262ea15"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.algebra.matrix.html#b2b431de65e6c1e23c1ae3a60262ea15"><span class="id" title="notation">m</span></a> <a class="idref" href="mathcomp.character.integral_char.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="mathcomp.character.integral_char.html#2d1412558d708665ab38bdd05f3b1341"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.character.integral_char.html#2d1412558d708665ab38bdd05f3b1341"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.integral_char.html#2d1412558d708665ab38bdd05f3b1341"><span class="id" title="notation">omega_i</span></a><a class="idref" href="mathcomp.character.integral_char.html#2d1412558d708665ab38bdd05f3b1341"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.character.integral_char.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.character.integral_char.html#2d1412558d708665ab38bdd05f3b1341"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.character.integral_char.html#2d1412558d708665ab38bdd05f3b1341"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.integral_char.html#2d1412558d708665ab38bdd05f3b1341"><span class="id" title="notation">omega_i</span></a><a class="idref" href="mathcomp.character.integral_char.html#2d1412558d708665ab38bdd05f3b1341"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.character.integral_char.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="mathcomp.character.integral_char.html#2d1412558d708665ab38bdd05f3b1341"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="gring_mode_class_sum_eq"><span class="id" title="lemma">gring_mode_class_sum_eq</span></a> (<span class="id" title="var">k</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#classes"><span class="id" title="definition">classes</span></a> <a class="idref" href="mathcomp.character.integral_char.html#IntegralChar.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a>) <span class="id" title="var">g</span> :<br/> - <a class="idref" href="mathcomp.character.integral_char.html#g"><span class="id" title="variable">g</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#enum_val"><span class="id" title="definition">enum_val</span></a> <a class="idref" href="mathcomp.character.integral_char.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.character.integral_char.html#2d1412558d708665ab38bdd05f3b1341"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.integral_char.html#2d1412558d708665ab38bdd05f3b1341"><span class="id" title="notation">omega_i</span></a><a class="idref" href="mathcomp.character.integral_char.html#2d1412558d708665ab38bdd05f3b1341"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.character.integral_char.html#c1b1dbde1d9ee51a0617fc81ec28c4a8"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.integral_char.html#c1b1dbde1d9ee51a0617fc81ec28c4a8"><span class="id" title="notation">K_k</span></a><a class="idref" href="mathcomp.character.integral_char.html#2d1412558d708665ab38bdd05f3b1341"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.character.integral_char.html#g"><span class="id" title="variable">g</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#38a288b01c62a2a6a720c34fc1fffe2c"><span class="id" title="notation">^:</span></a> <a class="idref" href="mathcomp.character.integral_char.html#IntegralChar.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#6411ed08724033ae48d2865f0380d533"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#6411ed08724033ae48d2865f0380d533"><span class="id" title="notation">R</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">chi_i</span></a> <a class="idref" href="mathcomp.character.integral_char.html#g"><span class="id" title="variable">g</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#69c431a9c94f6f30a655bd7ddb59037b"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">chi_i</span></a> 1%<span class="id" title="var">g</span>.<br/> - -<br/> -</div> - -<div class="doc"> - This is Isaacs, Theorem (3.7). -</div> -<div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="Aint_gring_mode_class_sum"><span class="id" title="lemma">Aint_gring_mode_class_sum</span></a> <span class="id" title="var">k</span> : <a class="idref" href="mathcomp.character.integral_char.html#2d1412558d708665ab38bdd05f3b1341"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.integral_char.html#2d1412558d708665ab38bdd05f3b1341"><span class="id" title="notation">omega_i</span></a><a class="idref" href="mathcomp.character.integral_char.html#2d1412558d708665ab38bdd05f3b1341"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.character.integral_char.html#c1b1dbde1d9ee51a0617fc81ec28c4a8"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.integral_char.html#c1b1dbde1d9ee51a0617fc81ec28c4a8"><span class="id" title="notation">K_k</span></a><a class="idref" href="mathcomp.character.integral_char.html#2d1412558d708665ab38bdd05f3b1341"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.algnum.html#Aint"><span class="id" title="definition">Aint</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - A more usable reformulation that does not involve the class sums. -</div> -<div class="code"> -<span class="id" title="keyword">Corollary</span> <a name="Aint_class_div_irr1"><span class="id" title="lemma">Aint_class_div_irr1</span></a> <span class="id" title="var">x</span> :<br/> - <a class="idref" href="mathcomp.character.integral_char.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.character.integral_char.html#IntegralChar.G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.character.integral_char.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#38a288b01c62a2a6a720c34fc1fffe2c"><span class="id" title="notation">^:</span></a> <a class="idref" href="mathcomp.character.integral_char.html#IntegralChar.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#6411ed08724033ae48d2865f0380d533"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#6411ed08724033ae48d2865f0380d533"><span class="id" title="notation">R</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">chi_i</span></a> <a class="idref" href="mathcomp.character.integral_char.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#69c431a9c94f6f30a655bd7ddb59037b"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">chi_i</span></a> 1%<span class="id" title="var">g</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.algnum.html#Aint"><span class="id" title="definition">Aint</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - This is Isaacs, Theorem (3.8). -</div> -<div class="code"> -<span class="id" title="keyword">Theorem</span> <a name="coprime_degree_support_cfcenter"><span class="id" title="lemma">coprime_degree_support_cfcenter</span></a> <span class="id" title="var">g</span> :<br/> - <a class="idref" href="mathcomp.ssreflect.div.html#coprime"><span class="id" title="definition">coprime</span></a> (<a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.truncC"><span class="id" title="definition">truncC</span></a> (<a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">chi_i</span></a> 1%<span class="id" title="var">g</span>)) <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.character.integral_char.html#g"><span class="id" title="variable">g</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#38a288b01c62a2a6a720c34fc1fffe2c"><span class="id" title="notation">^:</span></a> <a class="idref" href="mathcomp.character.integral_char.html#IntegralChar.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.character.integral_char.html#g"><span class="id" title="variable">g</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#c1ad6bcc76a6221225111f87bc3b0c3d"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#c1ad6bcc76a6221225111f87bc3b0c3d"><span class="id" title="notation">notin</span></a> (<a class="idref" href="mathcomp.character.character.html#ae199d7c7d964620f7672d2c74e0edb0"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#ae199d7c7d964620f7672d2c74e0edb0"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.character.character.html#ae199d7c7d964620f7672d2c74e0edb0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">chi_i</span></a><a class="idref" href="mathcomp.character.character.html#ae199d7c7d964620f7672d2c74e0edb0"><span class="id" title="notation">)</span></a>)%<span class="id" title="var">CF</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">chi_i</span></a> <a class="idref" href="mathcomp.character.integral_char.html#g"><span class="id" title="variable">g</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.character.integral_char.html#IntegralChar.GringIrrMode"><span class="id" title="section">GringIrrMode</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - This is Isaacs, Theorem (3.9). -</div> -<div class="code"> -<span class="id" title="keyword">Theorem</span> <a name="primes_class_simple_gt1"><span class="id" title="lemma">primes_class_simple_gt1</span></a> <span class="id" title="var">C</span> :<br/> - <a class="idref" href="mathcomp.solvable.gseries.html#simple"><span class="id" title="definition">simple</span></a> <a class="idref" href="mathcomp.character.integral_char.html#IntegralChar.G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b3ebd0deddd84fd60e149cb5ef719351"><span class="id" title="notation">~~</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#abelian"><span class="id" title="definition">abelian</span></a> <a class="idref" href="mathcomp.character.integral_char.html#IntegralChar.G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.character.integral_char.html#C"><span class="id" title="variable">C</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#ca7f9c8131cd704a6703ad86f415c132"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#classes"><span class="id" title="definition">classes</span></a> <a class="idref" href="mathcomp.character.integral_char.html#IntegralChar.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ca7f9c8131cd704a6703ad86f415c132"><span class="id" title="notation">)^#</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> (<a class="idref" href="mathcomp.ssreflect.prime.html#primes"><span class="id" title="definition">primes</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.character.integral_char.html#C"><span class="id" title="variable">C</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a>) <a class="idref" href="mathcomp.ssreflect.ssrnat.html#7f2a7ef2c63af7359b22787a9daf336e"><span class="id" title="notation">></span></a> 1)%<span class="id" title="var">N</span>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.character.integral_char.html#IntegralChar"><span class="id" title="section">IntegralChar</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="MoreIntegralChar"><span class="id" title="section">MoreIntegralChar</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Type</span> <span class="id" title="var">gT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - This is Burnside's famous p^a.q^b theorem (Isaacs, Theorem (3.10)). -</div> -<div class="code"> -<span class="id" title="keyword">Theorem</span> <a name="Burnside_p_a_q_b"><span class="id" title="lemma">Burnside_p_a_q_b</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.character.integral_char.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) :<br/> - (<a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> (<a class="idref" href="mathcomp.ssreflect.prime.html#primes"><span class="id" title="definition">primes</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.character.integral_char.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a>) <a class="idref" href="mathcomp.ssreflect.ssrnat.html#cb53cf0ee22c036a03b4a9281c68b5a3"><span class="id" title="notation">≤</span></a> 2)%<span class="id" title="var">N</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.nilpotent.html#solvable"><span class="id" title="definition">solvable</span></a> <a class="idref" href="mathcomp.character.integral_char.html#G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - This is Isaacs, Theorem (3.11). -</div> -<div class="code"> -<span class="id" title="keyword">Theorem</span> <a name="dvd_irr1_cardG"><span class="id" title="lemma">dvd_irr1_cardG</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.character.integral_char.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) <span class="id" title="var">i</span> : (<a class="idref" href="mathcomp.character.character.html#7d5ba9be6923d4bf4a568a8a939b7ab0"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#7d5ba9be6923d4bf4a568a8a939b7ab0"><span class="id" title="notation">chi</span></a><a class="idref" href="mathcomp.character.character.html#7d5ba9be6923d4bf4a568a8a939b7ab0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.character.integral_char.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.character.character.html#7d5ba9be6923d4bf4a568a8a939b7ab0"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.character.character.html#7d5ba9be6923d4bf4a568a8a939b7ab0"><span class="id" title="notation">_i</span></a> 1%<span class="id" title="var">g</span> <a class="idref" href="mathcomp.field.algC.html#a8acd6561c48edf701c07f3c736659e7"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.character.integral_char.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a>)%<span class="id" title="var">C</span>.<br/> - -<br/> -</div> - -<div class="doc"> - This is Isaacs, Theorem (3.12). -</div> -<div class="code"> -<span class="id" title="keyword">Theorem</span> <a name="dvd_irr1_index_center"><span class="id" title="lemma">dvd_irr1_index_center</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.character.integral_char.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) <span class="id" title="var">i</span> :<br/> - (<a class="idref" href="mathcomp.character.character.html#7d5ba9be6923d4bf4a568a8a939b7ab0"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#7d5ba9be6923d4bf4a568a8a939b7ab0"><span class="id" title="notation">chi</span></a><a class="idref" href="mathcomp.character.character.html#7d5ba9be6923d4bf4a568a8a939b7ab0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.character.integral_char.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.character.character.html#7d5ba9be6923d4bf4a568a8a939b7ab0"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.character.character.html#7d5ba9be6923d4bf4a568a8a939b7ab0"><span class="id" title="notation">_i</span></a> 1%<span class="id" title="var">g</span> <a class="idref" href="mathcomp.field.algC.html#a8acd6561c48edf701c07f3c736659e7"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.character.integral_char.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.character.character.html#ae199d7c7d964620f7672d2c74e0edb0"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#ae199d7c7d964620f7672d2c74e0edb0"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.character.character.html#ae199d7c7d964620f7672d2c74e0edb0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">chi_i</span></a><a class="idref" href="mathcomp.character.character.html#ae199d7c7d964620f7672d2c74e0edb0"><span class="id" title="notation">)</span></a>%<span class="id" title="var">CF</span><a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">|</span></a>)%<span class="id" title="var">C</span>.<br/> - -<br/> -</div> - -<div class="doc"> - This is Isaacs, Problem (3.7). -</div> -<div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="gring_classM_coef_sum_eq"><span class="id" title="lemma">gring_classM_coef_sum_eq</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.character.integral_char.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) <span class="id" title="var">j1</span> <span class="id" title="var">j2</span> <span class="id" title="var">k</span> <span class="id" title="var">g1</span> <span class="id" title="var">g2</span> <span class="id" title="var">g</span> :<br/> - <span class="id" title="keyword">let</span> <span class="id" title="var">a</span> := @<a class="idref" href="mathcomp.character.integral_char.html#gring_classM_coef"><span class="id" title="definition">gring_classM_coef</span></a> <a class="idref" href="mathcomp.character.integral_char.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.character.integral_char.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.character.integral_char.html#j1"><span class="id" title="variable">j1</span></a> <a class="idref" href="mathcomp.character.integral_char.html#j2"><span class="id" title="variable">j2</span></a> <span class="id" title="tactic">in</span> <span class="id" title="keyword">let</span> <span class="id" title="var">a_k</span> := <a class="idref" href="mathcomp.character.integral_char.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.character.integral_char.html#k"><span class="id" title="variable">k</span></a> <span class="id" title="tactic">in</span><br/> - <a class="idref" href="mathcomp.character.integral_char.html#g1"><span class="id" title="variable">g1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#enum_val"><span class="id" title="definition">enum_val</span></a> <a class="idref" href="mathcomp.character.integral_char.html#j1"><span class="id" title="variable">j1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.character.integral_char.html#g2"><span class="id" title="variable">g2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#enum_val"><span class="id" title="definition">enum_val</span></a> <a class="idref" href="mathcomp.character.integral_char.html#j2"><span class="id" title="variable">j2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.character.integral_char.html#g"><span class="id" title="variable">g</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#enum_val"><span class="id" title="definition">enum_val</span></a> <a class="idref" href="mathcomp.character.integral_char.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <span class="id" title="keyword">let</span> <span class="id" title="var">sum12g</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#de3e30c288f66ee879ea2b40e81e186c"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#de3e30c288f66ee879ea2b40e81e186c"><span class="id" title="notation">sum_i</span></a> <a class="idref" href="mathcomp.character.character.html#7d5ba9be6923d4bf4a568a8a939b7ab0"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#7d5ba9be6923d4bf4a568a8a939b7ab0"><span class="id" title="notation">chi</span></a><a class="idref" href="mathcomp.character.character.html#7d5ba9be6923d4bf4a568a8a939b7ab0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.character.integral_char.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.character.character.html#7d5ba9be6923d4bf4a568a8a939b7ab0"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.character.character.html#7d5ba9be6923d4bf4a568a8a939b7ab0"><span class="id" title="notation">_i</span></a> <a class="idref" href="mathcomp.character.integral_char.html#g1"><span class="id" title="variable">g1</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">chi_i</span></a> <a class="idref" href="mathcomp.character.integral_char.html#g2"><span class="id" title="variable">g2</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.ssrnum.html#651a776cde67abfb8f7231c08f29d878"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">chi_i</span></a> <a class="idref" href="mathcomp.character.integral_char.html#g"><span class="id" title="variable">g</span></a><a class="idref" href="mathcomp.algebra.ssrnum.html#651a776cde67abfb8f7231c08f29d878"><span class="id" title="notation">)^*</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#69c431a9c94f6f30a655bd7ddb59037b"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">chi_i</span></a> 1%<span class="id" title="var">g</span> <span class="id" title="tactic">in</span><br/> - <a class="idref" href="mathcomp.character.integral_char.html#a_k"><span class="id" title="variable">a_k</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#6411ed08724033ae48d2865f0380d533"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#6411ed08724033ae48d2865f0380d533"><span class="id" title="notation">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#6411ed08724033ae48d2865f0380d533"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#enum_val"><span class="id" title="definition">enum_val</span></a> <a class="idref" href="mathcomp.character.integral_char.html#j1"><span class="id" title="variable">j1</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#enum_val"><span class="id" title="definition">enum_val</span></a> <a class="idref" href="mathcomp.character.integral_char.html#j2"><span class="id" title="variable">j2</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#6411ed08724033ae48d2865f0380d533"><span class="id" title="notation">)%:</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#6411ed08724033ae48d2865f0380d533"><span class="id" title="notation">R</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#69c431a9c94f6f30a655bd7ddb59037b"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.character.integral_char.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#6411ed08724033ae48d2865f0380d533"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#6411ed08724033ae48d2865f0380d533"><span class="id" title="notation">R</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.character.integral_char.html#sum12g"><span class="id" title="variable">sum12g</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - This is Isaacs, Problem (2.16). -</div> -<div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="index_support_dvd_degree"><span class="id" title="lemma">index_support_dvd_degree</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.character.integral_char.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) <span class="id" title="var">chi</span> :<br/> - <a class="idref" href="mathcomp.character.integral_char.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.character.integral_char.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.character.integral_char.html#chi"><span class="id" title="variable">chi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">is</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">a</span></a> <a class="idref" href="mathcomp.character.character.html#character"><span class="id" title="definition">character</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.character.integral_char.html#chi"><span class="id" title="variable">chi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.character.classfun.html#62c6c4bf7772487a11a35ed29aee9fc7"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.classfun.html#62c6c4bf7772487a11a35ed29aee9fc7"><span class="id" title="notation">CF</span></a><a class="idref" href="mathcomp.character.classfun.html#62c6c4bf7772487a11a35ed29aee9fc7"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.character.integral_char.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.character.classfun.html#62c6c4bf7772487a11a35ed29aee9fc7"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.character.integral_char.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.character.classfun.html#62c6c4bf7772487a11a35ed29aee9fc7"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#081ff67d3116402bb680e8692aa39185"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.character.integral_char.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#b91223a7636398c530555b2312d1e79b"><span class="id" title="notation">:==:</span></a> 1%<span class="id" title="var">g</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#081ff67d3116402bb680e8692aa39185"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#081ff67d3116402bb680e8692aa39185"><span class="id" title="notation">||</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#abelian"><span class="id" title="definition">abelian</span></a> <a class="idref" href="mathcomp.character.integral_char.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - (<a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.character.integral_char.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.character.integral_char.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.field.algC.html#a8acd6561c48edf701c07f3c736659e7"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.character.integral_char.html#chi"><span class="id" title="variable">chi</span></a> 1%<span class="id" title="var">g</span>)%<span class="id" title="var">C</span>.<br/> - -<br/> -</div> - -<div class="doc"> - This is Isaacs, Theorem (3.13). -</div> -<div class="code"> -<span class="id" title="keyword">Theorem</span> <a name="faithful_degree_p_part"><span class="id" title="lemma">faithful_degree_p_part</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">p</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<span class="id" title="var">G</span> <span class="id" title="var">P</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.character.integral_char.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) <span class="id" title="var">i</span> :<br/> - <a class="idref" href="mathcomp.character.classfun.html#cfaithful"><span class="id" title="definition">cfaithful</span></a> <a class="idref" href="mathcomp.character.character.html#7d5ba9be6923d4bf4a568a8a939b7ab0"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#7d5ba9be6923d4bf4a568a8a939b7ab0"><span class="id" title="notation">chi</span></a><a class="idref" href="mathcomp.character.character.html#7d5ba9be6923d4bf4a568a8a939b7ab0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.character.integral_char.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.character.character.html#7d5ba9be6923d4bf4a568a8a939b7ab0"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.character.character.html#7d5ba9be6923d4bf4a568a8a939b7ab0"><span class="id" title="notation">_i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.character.integral_char.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#31aa0776b2fdb88da5b5ba70544862a1"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#31aa0776b2fdb88da5b5ba70544862a1"><span class="id" title="notation">nat</span></a> (<a class="idref" href="mathcomp.field.algC.html#Algebraics.Exports.truncC"><span class="id" title="definition">truncC</span></a> (<a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">chi_i</span></a> 1%<span class="id" title="var">g</span>)) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.character.integral_char.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#081d3e80d093e95dd63e6bafc24fef78"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#081d3e80d093e95dd63e6bafc24fef78"><span class="id" title="notation">Sylow</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#081d3e80d093e95dd63e6bafc24fef78"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.character.integral_char.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#081d3e80d093e95dd63e6bafc24fef78"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.character.integral_char.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#abelian"><span class="id" title="definition">abelian</span></a> <a class="idref" href="mathcomp.character.integral_char.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">chi_i</span></a> 1%<span class="id" title="var">g</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#6411ed08724033ae48d2865f0380d533"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.character.integral_char.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.character.integral_char.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#e157af410f295c13bf15c0e174d5741f"><span class="id" title="notation">`</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#e157af410f295c13bf15c0e174d5741f"><span class="id" title="notation">_p</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#6411ed08724033ae48d2865f0380d533"><span class="id" title="notation">)%:</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#6411ed08724033ae48d2865f0380d533"><span class="id" title="notation">R</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - This is Isaacs, Lemma (3.14). - Note that the assumption that G be cyclic is unnecessary, as S will be - empty if this is not the case. -</div> -<div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="sum_norm2_char_generators"><span class="id" title="lemma">sum_norm2_char_generators</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.character.integral_char.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">chi</span> : <a class="idref" href="mathcomp.character.classfun.html#5112e587c59fdaca05e10d1764f09c4c"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.classfun.html#5112e587c59fdaca05e10d1764f09c4c"><span class="id" title="notation">CF</span></a><a class="idref" href="mathcomp.character.classfun.html#5112e587c59fdaca05e10d1764f09c4c"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.character.integral_char.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.character.classfun.html#5112e587c59fdaca05e10d1764f09c4c"><span class="id" title="notation">)</span></a>) :<br/> - <span class="id" title="keyword">let</span> <span class="id" title="var">S</span> := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#27dabc72ea2c2c768f2db80a79f42524"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#27dabc72ea2c2c768f2db80a79f42524"><span class="id" title="notation">pred</span></a> <span class="id" title="var">s</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#27dabc72ea2c2c768f2db80a79f42524"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.cyclic.html#generator"><span class="id" title="definition">generator</span></a> <a class="idref" href="mathcomp.character.integral_char.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.character.integral_char.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#27dabc72ea2c2c768f2db80a79f42524"><span class="id" title="notation">]</span></a> <span class="id" title="tactic">in</span><br/> - <a class="idref" href="mathcomp.character.integral_char.html#chi"><span class="id" title="variable">chi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">is</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">a</span></a> <a class="idref" href="mathcomp.character.character.html#character"><span class="id" title="definition">character</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.character.integral_char.html#S"><span class="id" title="variable">S</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">s</span>, <a class="idref" href="mathcomp.character.integral_char.html#chi"><span class="id" title="variable">chi</span></a> <a class="idref" href="mathcomp.character.integral_char.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.algebra.ssralg.html#b4ba9f64661118f4ed0bad900f98d2a2"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b4ba9f64661118f4ed0bad900f98d2a2"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b4ba9f64661118f4ed0bad900f98d2a2"><span class="id" title="notation">(</span></a><span class="id" title="var">s</span> <a class="idref" href="mathcomp.algebra.ssralg.html#b4ba9f64661118f4ed0bad900f98d2a2"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.character.integral_char.html#S"><span class="id" title="variable">S</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b4ba9f64661118f4ed0bad900f98d2a2"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.algebra.ssrnum.html#55297ec87c6b3f98c14c99daeafb55d3"><span class="id" title="notation">`|</span></a><a class="idref" href="mathcomp.character.integral_char.html#chi"><span class="id" title="variable">chi</span></a> <a class="idref" href="mathcomp.character.integral_char.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="mathcomp.algebra.ssrnum.html#55297ec87c6b3f98c14c99daeafb55d3"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#663140372ac3b275aae871b74b140513"><span class="id" title="notation">^+</span></a> 2 <a class="idref" href="mathcomp.algebra.ssrnum.html#a3446a989be902579d41cbac1597f4cf"><span class="id" title="notation">≥</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.character.integral_char.html#S"><span class="id" title="variable">S</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#6411ed08724033ae48d2865f0380d533"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#6411ed08724033ae48d2865f0380d533"><span class="id" title="notation">R</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - This is Burnside's vanishing theorem (Isaacs, Theorem (3.15)). -</div> -<div class="code"> -<span class="id" title="keyword">Theorem</span> <a name="nonlinear_irr_vanish"><span class="id" title="lemma">nonlinear_irr_vanish</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.character.integral_char.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) <span class="id" title="var">i</span> :<br/> - <a class="idref" href="mathcomp.character.character.html#7d5ba9be6923d4bf4a568a8a939b7ab0"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#7d5ba9be6923d4bf4a568a8a939b7ab0"><span class="id" title="notation">chi</span></a><a class="idref" href="mathcomp.character.character.html#7d5ba9be6923d4bf4a568a8a939b7ab0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.character.integral_char.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.character.character.html#7d5ba9be6923d4bf4a568a8a939b7ab0"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.character.character.html#7d5ba9be6923d4bf4a568a8a939b7ab0"><span class="id" title="notation">_i</span></a> 1%<span class="id" title="var">g</span> <a class="idref" href="mathcomp.algebra.ssrnum.html#1f96a77ded31d6d5fa0c8fe9a087652a"><span class="id" title="notation">></span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.character.integral_char.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.character.integral_char.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#fc972dbc606652894cd5958d13eb0ca3"><span class="id" title="notation">chi_i</span></a> <a class="idref" href="mathcomp.character.integral_char.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 0.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.character.integral_char.html#MoreIntegralChar"><span class="id" title="section">MoreIntegralChar</span></a>.<br/> -</div> -</div> - -<div id="footer"> -<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a> -</div> - -</div> - -</body> -</html>
\ No newline at end of file |