diff options
Diffstat (limited to 'docs/htmldoc/mathcomp.character.integral_char.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.character.integral_char.html | 339 |
1 files changed, 339 insertions, 0 deletions
diff --git a/docs/htmldoc/mathcomp.character.integral_char.html b/docs/htmldoc/mathcomp.character.integral_char.html new file mode 100644 index 0000000..749c078 --- /dev/null +++ b/docs/htmldoc/mathcomp.character.integral_char.html @@ -0,0 +1,339 @@ +<!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/> +<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#"><span class="id" title="library">mathcomp.ssreflect.ssreflect</span></a>.<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#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><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#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) :<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#e4098fb21bb0cc5ef8d3e3bf7391b88b"><span class="id" title="notation">{</span></a><span class="id" title="var">Qn</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#e4098fb21bb0cc5ef8d3e3bf7391b88b"><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/8.8.0/stdlib//Coq.Init.Specif.html#e4098fb21bb0cc5ef8d3e3bf7391b88b"><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#899a5fd19c4f3564d9757a9ac446b1dc"><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#899a5fd19c4f3564d9757a9ac446b1dc"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#e4098fb21bb0cc5ef8d3e3bf7391b88b"><span class="id" title="notation">&</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#e4098fb21bb0cc5ef8d3e3bf7391b88b"><span class="id" title="notation">{</span></a><span class="id" title="var">QnC</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#e4098fb21bb0cc5ef8d3e3bf7391b88b"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">}</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#e4098fb21bb0cc5ef8d3e3bf7391b88b"><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/8.8.0/stdlib//Coq.ssr.ssreflect.html#argumentType"><span class="id" title="definition">argumentType</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#mem"><span class="id" title="definition">mem</span></a> (<a class="idref" href="mathcomp.field.galois.html#7f39fd713ca3f00fbfda8b71eae7e2e1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.field.galois.html#7f39fd713ca3f00fbfda8b71eae7e2e1"><span class="id" title="notation">Gal</span></a><a class="idref" href="mathcomp.field.galois.html#7f39fd713ca3f00fbfda8b71eae7e2e1"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.vector.html#899a5fd19c4f3564d9757a9ac446b1dc"><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#899a5fd19c4f3564d9757a9ac446b1dc"><span class="id" title="notation">}</span></a>%<span class="id" title="var">VS</span> <a class="idref" href="mathcomp.field.galois.html#7f39fd713ca3f00fbfda8b71eae7e2e1"><span class="id" title="notation">/</span></a> 1%<span class="id" title="var">VS</span><a class="idref" href="mathcomp.field.galois.html#7f39fd713ca3f00fbfda8b71eae7e2e1"><span class="id" title="notation">)</span></a>)),<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">{</span></a><span class="id" title="var">nu</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">|</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><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/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">:</span></a> <span class="id" title="var">a</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><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/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><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/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">}</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#e4098fb21bb0cc5ef8d3e3bf7391b88b"><span class="id" title="notation">&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#e4098fb21bb0cc5ef8d3e3bf7391b88b"><span class="id" title="notation">{</span></a><span class="id" title="var">w</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#e4098fb21bb0cc5ef8d3e3bf7391b88b"><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/8.8.0/stdlib//Coq.Init.Specif.html#e4098fb21bb0cc5ef8d3e3bf7391b88b"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><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#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.algebra.poly.html#92efb5ea268b6e2f9a125afe76aecbba"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.algebra.poly.html#92efb5ea268b6e2f9a125afe76aecbba"><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/8.8.0/stdlib//Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation"><<</span></a>1<a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><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#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">>></span></a>%<span class="id" title="var">VS</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><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/8.8.0/stdlib//Coq.Init.Specif.html#e4098fb21bb0cc5ef8d3e3bf7391b88b"><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#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><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#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">phi</span> : <a class="idref" href="mathcomp.character.classfun.html#d35bff44a2e44c0688f93d605f17e822"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.classfun.html#d35bff44a2e44c0688f93d605f17e822"><span class="id" title="notation">CF</span></a><a class="idref" href="mathcomp.character.classfun.html#d35bff44a2e44c0688f93d605f17e822"><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#d35bff44a2e44c0688f93d605f17e822"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#1e40fee506a85b20590ef299005b003d"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#1e40fee506a85b20590ef299005b003d"><span class="id" title="notation">is</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#1e40fee506a85b20590ef299005b003d"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#89402f0d9375903caa99ad84144160d5"><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#89402f0d9375903caa99ad84144160d5"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#aa34fd1c61c5cf0a3356b624a5d2afed"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><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#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a>)%<span class="id" title="var">N</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">{</span></a><span class="id" title="var">a</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><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/8.8.0/stdlib//Coq.Init.Specif.html#5b63cb9ed0fed82566685c66e56592e4"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#e4098fb21bb0cc5ef8d3e3bf7391b88b"><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#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><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#ab072eb546972c7e5cdaf33b8a35ce6b"><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#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><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#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a>) <span class="id" title="var">g</span> :=<br/> + <a class="idref" href="mathcomp.ssreflect.finset.html#11a9aebd9632a5968df4f5811663355a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#11a9aebd9632a5968df4f5811663355a"><span class="id" title="notation">set</span></a> <span class="id" title="var">xy</span> <a class="idref" href="mathcomp.ssreflect.finset.html#11a9aebd9632a5968df4f5811663355a"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#a4c99a0dbc2a758b24afbd951fc3a580"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#a4c99a0dbc2a758b24afbd951fc3a580"><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#a4c99a0dbc2a758b24afbd951fc3a580"><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#a4c99a0dbc2a758b24afbd951fc3a580"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#11a9aebd9632a5968df4f5811663355a"><span class="id" title="notation">|</span></a> <span class="id" title="keyword">let</span>: <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <span class="id" title="var">y</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><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#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><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#11a9aebd9632a5968df4f5811663355a"><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#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">I_</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><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#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a>) :=<br/> + <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><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#f01714bb99e6c7abc6cfb2e43eff7f6e"><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#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">I_</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><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#f01714bb99e6c7abc6cfb2e43eff7f6e"><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#afc4c4affce3b8ef6e9f442c1d91639c"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.integral_char.html#afc4c4affce3b8ef6e9f442c1d91639c"><span class="id" title="notation">K_i</span></a> <a class="idref" href="mathcomp.algebra.mxalgebra.html#bfc118b745d1a8ee504472dad1db645c"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#bfc118b745d1a8ee504472dad1db645c"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.mxalgebra.html#972f5ef28830d59d0a4b5dfdfda2843a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#972f5ef28830d59d0a4b5dfdfda2843a"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#972f5ef28830d59d0a4b5dfdfda2843a"><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#972f5ef28830d59d0a4b5dfdfda2843a"><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#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">I_</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><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#f01714bb99e6c7abc6cfb2e43eff7f6e"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><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#f01714bb99e6c7abc6cfb2e43eff7f6e"><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#afc4c4affce3b8ef6e9f442c1d91639c"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.integral_char.html#afc4c4affce3b8ef6e9f442c1d91639c"><span class="id" title="notation">K_i</span></a> <a class="idref" href="mathcomp.algebra.matrix.html#9c6b777e699b0b93592b907e7450465e"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.algebra.matrix.html#9c6b777e699b0b93592b907e7450465e"><span class="id" title="notation">m</span></a> <a class="idref" href="mathcomp.character.integral_char.html#afc4c4affce3b8ef6e9f442c1d91639c"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.integral_char.html#afc4c4affce3b8ef6e9f442c1d91639c"><span class="id" title="notation">K_j</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#640778742e86daa97d31c9911c679af3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#640778742e86daa97d31c9911c679af3"><span class="id" title="notation">sum_k</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#af5c1d7e13410a0a6c3dff5441ac8477"><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#af5c1d7e13410a0a6c3dff5441ac8477"><span class="id" title="notation">)%:</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#af5c1d7e13410a0a6c3dff5441ac8477"><span class="id" title="notation">R</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#81f8078534dcbb7e13a32d292f766525"><span class="id" title="notation">*:</span></a> <a class="idref" href="mathcomp.character.integral_char.html#afc4c4affce3b8ef6e9f442c1d91639c"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.integral_char.html#afc4c4affce3b8ef6e9f442c1d91639c"><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/8.8.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#f3016d4e55aa553d3e912592ec65e342"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.character.character.html#04ab09ba1579a4628398b1ac594f25e6"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#04ab09ba1579a4628398b1ac594f25e6"><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#f3016d4e55aa553d3e912592ec65e342"><span class="id" title="notation">)^-1</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#81f8078534dcbb7e13a32d292f766525"><span class="id" title="notation">*:</span></a> <a class="idref" href="mathcomp.character.character.html#04ab09ba1579a4628398b1ac594f25e6"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#04ab09ba1579a4628398b1ac594f25e6"><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/8.8.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/8.8.0/stdlib//Coq.ssr.ssreflect.html#58f94351327943cd874eb55da8e0ca14"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#58f94351327943cd874eb55da8e0ca14"><span class="id" title="notation">unlockable</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#58f94351327943cd874eb55da8e0ca14"><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/8.8.0/stdlib//Coq.ssr.ssreflect.html#58f94351327943cd874eb55da8e0ca14"><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="c1170e3ef8cfb8250158dd746fcfbce5"><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="47d30fc39d66fa0fa54b1639ab583368"><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#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><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#ab072eb546972c7e5cdaf33b8a35ce6b"><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#d35bff44a2e44c0688f93d605f17e822"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.classfun.html#d35bff44a2e44c0688f93d605f17e822"><span class="id" title="notation">CF</span></a><a class="idref" href="mathcomp.character.classfun.html#d35bff44a2e44c0688f93d605f17e822"><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#d35bff44a2e44c0688f93d605f17e822"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#1e40fee506a85b20590ef299005b003d"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#1e40fee506a85b20590ef299005b003d"><span class="id" title="notation">is</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#1e40fee506a85b20590ef299005b003d"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><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#18b59bdb60cfba8ef35899cef605f5f1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#18b59bdb60cfba8ef35899cef605f5f1"><span class="id" title="notation">chi</span></a><a class="idref" href="mathcomp.character.character.html#18b59bdb60cfba8ef35899cef605f5f1"><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#18b59bdb60cfba8ef35899cef605f5f1"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.character.character.html#18b59bdb60cfba8ef35899cef605f5f1"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#bfc118b745d1a8ee504472dad1db645c"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#bfc118b745d1a8ee504472dad1db645c"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.mxalgebra.html#972f5ef28830d59d0a4b5dfdfda2843a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#972f5ef28830d59d0a4b5dfdfda2843a"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#972f5ef28830d59d0a4b5dfdfda2843a"><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#972f5ef28830d59d0a4b5dfdfda2843a"><span class="id" title="notation">)</span></a>)%<span class="id" title="var">MS</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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/8.8.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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.character.character.html#04ab09ba1579a4628398b1ac594f25e6"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#04ab09ba1579a4628398b1ac594f25e6"><span class="id" title="notation">chi_i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#bfc118b745d1a8ee504472dad1db645c"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#bfc118b745d1a8ee504472dad1db645c"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.mxalgebra.html#972f5ef28830d59d0a4b5dfdfda2843a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#972f5ef28830d59d0a4b5dfdfda2843a"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#972f5ef28830d59d0a4b5dfdfda2843a"><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#972f5ef28830d59d0a4b5dfdfda2843a"><span class="id" title="notation">)</span></a>)%<span class="id" title="var">MS</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.character.integral_char.html#47d30fc39d66fa0fa54b1639ab583368"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.integral_char.html#47d30fc39d66fa0fa54b1639ab583368"><span class="id" title="notation">omega_i</span></a><a class="idref" href="mathcomp.character.integral_char.html#47d30fc39d66fa0fa54b1639ab583368"><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#47d30fc39d66fa0fa54b1639ab583368"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.algebra.matrix.html#6bc5aad53caab585f4bb088e10501342"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.matrix.html#6bc5aad53caab585f4bb088e10501342"><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#bfc118b745d1a8ee504472dad1db645c"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#bfc118b745d1a8ee504472dad1db645c"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.mxalgebra.html#972f5ef28830d59d0a4b5dfdfda2843a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#972f5ef28830d59d0a4b5dfdfda2843a"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#972f5ef28830d59d0a4b5dfdfda2843a"><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#972f5ef28830d59d0a4b5dfdfda2843a"><span class="id" title="notation">)</span></a>)%<span class="id" title="var">MS</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#e5b0c5fb6feae803158d92833c2cdc72"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#e5b0c5fb6feae803158d92833c2cdc72"><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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.character.integral_char.html#47d30fc39d66fa0fa54b1639ab583368"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.integral_char.html#47d30fc39d66fa0fa54b1639ab583368"><span class="id" title="notation">omega_i</span></a><a class="idref" href="mathcomp.character.integral_char.html#47d30fc39d66fa0fa54b1639ab583368"><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#47d30fc39d66fa0fa54b1639ab583368"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.algebra.matrix.html#6bc5aad53caab585f4bb088e10501342"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.matrix.html#6bc5aad53caab585f4bb088e10501342"><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#bfc118b745d1a8ee504472dad1db645c"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#bfc118b745d1a8ee504472dad1db645c"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.mxalgebra.html#972f5ef28830d59d0a4b5dfdfda2843a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#972f5ef28830d59d0a4b5dfdfda2843a"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#972f5ef28830d59d0a4b5dfdfda2843a"><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#972f5ef28830d59d0a4b5dfdfda2843a"><span class="id" title="notation">)</span></a>)%<span class="id" title="var">MS</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#bfc118b745d1a8ee504472dad1db645c"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#bfc118b745d1a8ee504472dad1db645c"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.mxalgebra.html#972f5ef28830d59d0a4b5dfdfda2843a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#972f5ef28830d59d0a4b5dfdfda2843a"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.algebra.mxalgebra.html#972f5ef28830d59d0a4b5dfdfda2843a"><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#972f5ef28830d59d0a4b5dfdfda2843a"><span class="id" title="notation">)</span></a>)%<span class="id" title="var">MS</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.character.integral_char.html#47d30fc39d66fa0fa54b1639ab583368"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.integral_char.html#47d30fc39d66fa0fa54b1639ab583368"><span class="id" title="notation">omega_i</span></a><a class="idref" href="mathcomp.character.integral_char.html#47d30fc39d66fa0fa54b1639ab583368"><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#9c6b777e699b0b93592b907e7450465e"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.algebra.matrix.html#9c6b777e699b0b93592b907e7450465e"><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#47d30fc39d66fa0fa54b1639ab583368"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.character.integral_char.html#47d30fc39d66fa0fa54b1639ab583368"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.integral_char.html#47d30fc39d66fa0fa54b1639ab583368"><span class="id" title="notation">omega_i</span></a><a class="idref" href="mathcomp.character.integral_char.html#47d30fc39d66fa0fa54b1639ab583368"><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#47d30fc39d66fa0fa54b1639ab583368"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.character.integral_char.html#47d30fc39d66fa0fa54b1639ab583368"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.integral_char.html#47d30fc39d66fa0fa54b1639ab583368"><span class="id" title="notation">omega_i</span></a><a class="idref" href="mathcomp.character.integral_char.html#47d30fc39d66fa0fa54b1639ab583368"><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#47d30fc39d66fa0fa54b1639ab583368"><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#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#9de6d53cccc27f521f3ab56b38159140"><span class="id" title="notation">I_</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><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#f01714bb99e6c7abc6cfb2e43eff7f6e"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.character.integral_char.html#47d30fc39d66fa0fa54b1639ab583368"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.integral_char.html#47d30fc39d66fa0fa54b1639ab583368"><span class="id" title="notation">omega_i</span></a><a class="idref" href="mathcomp.character.integral_char.html#47d30fc39d66fa0fa54b1639ab583368"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.character.integral_char.html#c1170e3ef8cfb8250158dd746fcfbce5"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.integral_char.html#c1170e3ef8cfb8250158dd746fcfbce5"><span class="id" title="notation">K_k</span></a><a class="idref" href="mathcomp.character.integral_char.html#47d30fc39d66fa0fa54b1639ab583368"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><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#30988ee242f08216f4b40cf90b42b816"><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#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#af5c1d7e13410a0a6c3dff5441ac8477"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#af5c1d7e13410a0a6c3dff5441ac8477"><span class="id" title="notation">R</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.character.character.html#04ab09ba1579a4628398b1ac594f25e6"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#04ab09ba1579a4628398b1ac594f25e6"><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#4fa85b0aa898c2a7e18c3b076438c2e7"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.character.character.html#04ab09ba1579a4628398b1ac594f25e6"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#04ab09ba1579a4628398b1ac594f25e6"><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#47d30fc39d66fa0fa54b1639ab583368"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.integral_char.html#47d30fc39d66fa0fa54b1639ab583368"><span class="id" title="notation">omega_i</span></a><a class="idref" href="mathcomp.character.integral_char.html#47d30fc39d66fa0fa54b1639ab583368"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.character.integral_char.html#c1170e3ef8cfb8250158dd746fcfbce5"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.integral_char.html#c1170e3ef8cfb8250158dd746fcfbce5"><span class="id" title="notation">K_k</span></a><a class="idref" href="mathcomp.character.integral_char.html#47d30fc39d66fa0fa54b1639ab583368"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><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#30988ee242f08216f4b40cf90b42b816"><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#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#af5c1d7e13410a0a6c3dff5441ac8477"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#af5c1d7e13410a0a6c3dff5441ac8477"><span class="id" title="notation">R</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.character.character.html#04ab09ba1579a4628398b1ac594f25e6"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#04ab09ba1579a4628398b1ac594f25e6"><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#4fa85b0aa898c2a7e18c3b076438c2e7"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.character.character.html#04ab09ba1579a4628398b1ac594f25e6"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#04ab09ba1579a4628398b1ac594f25e6"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><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#04ab09ba1579a4628398b1ac594f25e6"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#04ab09ba1579a4628398b1ac594f25e6"><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#f01714bb99e6c7abc6cfb2e43eff7f6e"><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#30988ee242f08216f4b40cf90b42b816"><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#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#ad6d23746eb1a3b62e52010d3945a1db"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ad6d23746eb1a3b62e52010d3945a1db"><span class="id" title="notation">notin</span></a> (<a class="idref" href="mathcomp.character.character.html#cfab1161405ba806c35c4f37c62102ab"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#cfab1161405ba806c35c4f37c62102ab"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.character.character.html#cfab1161405ba806c35c4f37c62102ab"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.character.character.html#04ab09ba1579a4628398b1ac594f25e6"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#04ab09ba1579a4628398b1ac594f25e6"><span class="id" title="notation">chi_i</span></a><a class="idref" href="mathcomp.character.character.html#cfab1161405ba806c35c4f37c62102ab"><span class="id" title="notation">)</span></a>)%<span class="id" title="var">CF</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.character.character.html#04ab09ba1579a4628398b1ac594f25e6"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#04ab09ba1579a4628398b1ac594f25e6"><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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#adb8044960c962a921cca1bd48aae97d"><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#adb8044960c962a921cca1bd48aae97d"><span class="id" title="notation">)^#</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#f01714bb99e6c7abc6cfb2e43eff7f6e"><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#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a>) <a class="idref" href="mathcomp.ssreflect.ssrnat.html#19ab5cfd7e4f60fa14f22b576013bd96"><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#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><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#ab072eb546972c7e5cdaf33b8a35ce6b"><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#f01714bb99e6c7abc6cfb2e43eff7f6e"><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#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a>) <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9b077c369e19739ef880736ba34623ff"><span class="id" title="notation">≤</span></a> 2)%<span class="id" title="var">N</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><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#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) <span class="id" title="var">i</span> : (<a class="idref" href="mathcomp.character.character.html#18b59bdb60cfba8ef35899cef605f5f1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#18b59bdb60cfba8ef35899cef605f5f1"><span class="id" title="notation">chi</span></a><a class="idref" href="mathcomp.character.character.html#18b59bdb60cfba8ef35899cef605f5f1"><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#18b59bdb60cfba8ef35899cef605f5f1"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.character.character.html#18b59bdb60cfba8ef35899cef605f5f1"><span class="id" title="notation">_i</span></a> 1%<span class="id" title="var">g</span> <a class="idref" href="mathcomp.field.algC.html#9a2f23320469c9d2a314bb86625d5b32"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><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#f01714bb99e6c7abc6cfb2e43eff7f6e"><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#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><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#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) <span class="id" title="var">i</span> :<br/> + (<a class="idref" href="mathcomp.character.character.html#18b59bdb60cfba8ef35899cef605f5f1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#18b59bdb60cfba8ef35899cef605f5f1"><span class="id" title="notation">chi</span></a><a class="idref" href="mathcomp.character.character.html#18b59bdb60cfba8ef35899cef605f5f1"><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#18b59bdb60cfba8ef35899cef605f5f1"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.character.character.html#18b59bdb60cfba8ef35899cef605f5f1"><span class="id" title="notation">_i</span></a> 1%<span class="id" title="var">g</span> <a class="idref" href="mathcomp.field.algC.html#9a2f23320469c9d2a314bb86625d5b32"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><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#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.character.character.html#cfab1161405ba806c35c4f37c62102ab"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#cfab1161405ba806c35c4f37c62102ab"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.character.character.html#cfab1161405ba806c35c4f37c62102ab"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.character.character.html#04ab09ba1579a4628398b1ac594f25e6"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#04ab09ba1579a4628398b1ac594f25e6"><span class="id" title="notation">chi_i</span></a><a class="idref" href="mathcomp.character.character.html#cfab1161405ba806c35c4f37c62102ab"><span class="id" title="notation">)</span></a>%<span class="id" title="var">CF</span><a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><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#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><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#ab072eb546972c7e5cdaf33b8a35ce6b"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#640778742e86daa97d31c9911c679af3"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#640778742e86daa97d31c9911c679af3"><span class="id" title="notation">sum_i</span></a> <a class="idref" href="mathcomp.character.character.html#18b59bdb60cfba8ef35899cef605f5f1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#18b59bdb60cfba8ef35899cef605f5f1"><span class="id" title="notation">chi</span></a><a class="idref" href="mathcomp.character.character.html#18b59bdb60cfba8ef35899cef605f5f1"><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#18b59bdb60cfba8ef35899cef605f5f1"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.character.character.html#18b59bdb60cfba8ef35899cef605f5f1"><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#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.character.character.html#04ab09ba1579a4628398b1ac594f25e6"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#04ab09ba1579a4628398b1ac594f25e6"><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#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.ssrnum.html#b07d6e6599ef6e468ce182ffe6029532"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.character.character.html#04ab09ba1579a4628398b1ac594f25e6"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#04ab09ba1579a4628398b1ac594f25e6"><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#b07d6e6599ef6e468ce182ffe6029532"><span class="id" title="notation">)^*</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#4fa85b0aa898c2a7e18c3b076438c2e7"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.character.character.html#04ab09ba1579a4628398b1ac594f25e6"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#04ab09ba1579a4628398b1ac594f25e6"><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#af5c1d7e13410a0a6c3dff5441ac8477"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#af5c1d7e13410a0a6c3dff5441ac8477"><span class="id" title="notation">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#af5c1d7e13410a0a6c3dff5441ac8477"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><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#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><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#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#af5c1d7e13410a0a6c3dff5441ac8477"><span class="id" title="notation">)%:</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#af5c1d7e13410a0a6c3dff5441ac8477"><span class="id" title="notation">R</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#4fa85b0aa898c2a7e18c3b076438c2e7"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><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#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#af5c1d7e13410a0a6c3dff5441ac8477"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#af5c1d7e13410a0a6c3dff5441ac8477"><span class="id" title="notation">R</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><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#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><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#ab072eb546972c7e5cdaf33b8a35ce6b"><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#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#1e40fee506a85b20590ef299005b003d"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#1e40fee506a85b20590ef299005b003d"><span class="id" title="notation">is</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#1e40fee506a85b20590ef299005b003d"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.character.classfun.html#98d2bf34d82aa4f9a1163621bbcbea56"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.classfun.html#98d2bf34d82aa4f9a1163621bbcbea56"><span class="id" title="notation">CF</span></a><a class="idref" href="mathcomp.character.classfun.html#98d2bf34d82aa4f9a1163621bbcbea56"><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#98d2bf34d82aa4f9a1163621bbcbea56"><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#98d2bf34d82aa4f9a1163621bbcbea56"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><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#24f47bb7b1a372904563d2bdb8a213a4"><span class="id" title="notation">:==:</span></a> 1%<span class="id" title="var">g</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + (<a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><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#f65ecb5148d1ef5a9c551827b20e9bfa"><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#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.field.algC.html#9a2f23320469c9d2a314bb86625d5b32"><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/8.8.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#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><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#ab072eb546972c7e5cdaf33b8a35ce6b"><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#18b59bdb60cfba8ef35899cef605f5f1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#18b59bdb60cfba8ef35899cef605f5f1"><span class="id" title="notation">chi</span></a><a class="idref" href="mathcomp.character.character.html#18b59bdb60cfba8ef35899cef605f5f1"><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#18b59bdb60cfba8ef35899cef605f5f1"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.character.character.html#18b59bdb60cfba8ef35899cef605f5f1"><span class="id" title="notation">_i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#8663a77d1d910826e10ba42d1e8d2a02"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#8663a77d1d910826e10ba42d1e8d2a02"><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#04ab09ba1579a4628398b1ac594f25e6"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#04ab09ba1579a4628398b1ac594f25e6"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">Sylow</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><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#43f075314fcfccdaa8a5813debe2d9ed"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.character.character.html#04ab09ba1579a4628398b1ac594f25e6"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#04ab09ba1579a4628398b1ac594f25e6"><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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#af5c1d7e13410a0a6c3dff5441ac8477"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><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#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><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#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#fdd58465d6c6ade4406f2c94baecf8f8"><span class="id" title="notation">`</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#fdd58465d6c6ade4406f2c94baecf8f8"><span class="id" title="notation">_p</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#af5c1d7e13410a0a6c3dff5441ac8477"><span class="id" title="notation">)%:</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#af5c1d7e13410a0a6c3dff5441ac8477"><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#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><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#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">chi</span> : <a class="idref" href="mathcomp.character.classfun.html#d35bff44a2e44c0688f93d605f17e822"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.classfun.html#d35bff44a2e44c0688f93d605f17e822"><span class="id" title="notation">CF</span></a><a class="idref" href="mathcomp.character.classfun.html#d35bff44a2e44c0688f93d605f17e822"><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#d35bff44a2e44c0688f93d605f17e822"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#880a9790dece461a678db8aa0c091f63"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#880a9790dece461a678db8aa0c091f63"><span class="id" title="notation">pred</span></a> <span class="id" title="var">s</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#880a9790dece461a678db8aa0c091f63"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#880a9790dece461a678db8aa0c091f63"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#1e40fee506a85b20590ef299005b003d"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#1e40fee506a85b20590ef299005b003d"><span class="id" title="notation">is</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#1e40fee506a85b20590ef299005b003d"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><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#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.algebra.ssralg.html#0c791dbdc1655ae690f0a6c159a384c0"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0c791dbdc1655ae690f0a6c159a384c0"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0c791dbdc1655ae690f0a6c159a384c0"><span class="id" title="notation">(</span></a><span class="id" title="var">s</span> <a class="idref" href="mathcomp.algebra.ssralg.html#0c791dbdc1655ae690f0a6c159a384c0"><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#0c791dbdc1655ae690f0a6c159a384c0"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.algebra.ssrnum.html#c536f9a86d3c053391521360ac3f5a61"><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#c536f9a86d3c053391521360ac3f5a61"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#fb22424322c3d7eb9b837dfca65ce21e"><span class="id" title="notation">^+</span></a> 2 <a class="idref" href="mathcomp.algebra.ssrnum.html#4a55c8439dfd5912be472b2910ab4015"><span class="id" title="notation">≥</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><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#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#af5c1d7e13410a0a6c3dff5441ac8477"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#af5c1d7e13410a0a6c3dff5441ac8477"><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#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><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#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) <span class="id" title="var">i</span> :<br/> + <a class="idref" href="mathcomp.character.character.html#18b59bdb60cfba8ef35899cef605f5f1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#18b59bdb60cfba8ef35899cef605f5f1"><span class="id" title="notation">chi</span></a><a class="idref" href="mathcomp.character.character.html#18b59bdb60cfba8ef35899cef605f5f1"><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#18b59bdb60cfba8ef35899cef605f5f1"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.character.character.html#18b59bdb60cfba8ef35899cef605f5f1"><span class="id" title="notation">_i</span></a> 1%<span class="id" title="var">g</span> <a class="idref" href="mathcomp.algebra.ssrnum.html#07bcd9d86ae6b6828fbc17b15193853f"><span class="id" title="notation">></span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><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/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.character.character.html#04ab09ba1579a4628398b1ac594f25e6"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.character.character.html#04ab09ba1579a4628398b1ac594f25e6"><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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><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 |