diff options
Diffstat (limited to 'docs/htmldoc/mathcomp.solvable.alt.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.solvable.alt.html | 199 |
1 files changed, 199 insertions, 0 deletions
diff --git a/docs/htmldoc/mathcomp.solvable.alt.html b/docs/htmldoc/mathcomp.solvable.alt.html new file mode 100644 index 0000000..dd87d49 --- /dev/null +++ b/docs/htmldoc/mathcomp.solvable.alt.html @@ -0,0 +1,199 @@ +<!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.solvable.alt</title> +</head> + +<body> + +<div id="page"> + +<div id="header"> +</div> + +<div id="main"> + +<h1 class="libtitle">Library mathcomp.solvable.alt</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"> + Definitions of the symmetric and alternate groups, and some properties. + 'Sym_T == The symmetric group over type T (which must have a finType + structure). + := [set: {perm T} ] + 'Alt_T == The alternating group over type T. +</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>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="bool_groupMixin"><span class="id" title="definition">bool_groupMixin</span></a> := <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Mixin"><span class="id" title="definition">FinGroup.Mixin</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#addbA"><span class="id" title="lemma">addbA</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#addFb"><span class="id" title="lemma">addFb</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#addbb"><span class="id" title="lemma">addbb</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">bool_baseGroup</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.BaseFinGroupType"><span class="id" title="abbreviation">BaseFinGroupType</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a> <a class="idref" href="mathcomp.solvable.alt.html#bool_groupMixin"><span class="id" title="definition">bool_groupMixin</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">boolGroup</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.FinGroupType"><span class="id" title="abbreviation">FinGroupType</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#addbb"><span class="id" title="lemma">addbb</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="SymAltDef"><span class="id" title="section">SymAltDef</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variable</span> <a name="SymAltDef.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>.<br/> +<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">s</span> : <a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span> : <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.T"><span class="id" title="variable">T</span></a>).<br/> + +<br/> +</div> + +<div class="doc"> + Definitions of the alternate groups and some Properties * +</div> +<div class="code"> +<span class="id" title="keyword">Definition</span> <a name="Sym"><span class="id" title="definition">Sym</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#phant"><span class="id" title="inductive">phant</span></a> <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.T"><span class="id" title="variable">T</span></a> : <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.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a> := <a class="idref" href="mathcomp.ssreflect.finset.html#setT"><span class="id" title="abbreviation">setT</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Sym_group</span> <span class="id" title="var">phT</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#ccb763a84253e971fd106aeeb9cd3cb0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ccb763a84253e971fd106aeeb9cd3cb0"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#ccb763a84253e971fd106aeeb9cd3cb0"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.alt.html#Sym"><span class="id" title="definition">Sym</span></a> <a class="idref" href="mathcomp.solvable.alt.html#phT"><span class="id" title="variable">phT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ccb763a84253e971fd106aeeb9cd3cb0"><span class="id" title="notation">]</span></a>.<br/> + +<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">sign_morph</span> := @<a class="idref" href="mathcomp.fingroup.morphism.html#Morphism"><span class="id" title="constructor">Morphism</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="mathcomp.solvable.alt.html#f32935784d160bf8a9cbdbd987859003"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#f32935784d160bf8a9cbdbd987859003"><span class="id" title="notation">Sym_T</span></a> <span class="id" title="var">_</span> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#in2W"><span class="id" title="lemma">in2W</span></a> (@<a class="idref" href="mathcomp.fingroup.perm.html#odd_permM"><span class="id" title="lemma">odd_permM</span></a> <span class="id" title="var">_</span>)).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="Alt"><span class="id" title="definition">Alt</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#phant"><span class="id" title="inductive">phant</span></a> <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.T"><span class="id" title="variable">T</span></a> := <a class="idref" href="mathcomp.fingroup.morphism.html#034cc0eb573e9a86d9574eaed7b27a13"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#034cc0eb573e9a86d9574eaed7b27a13"><span class="id" title="notation">ker</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#034cc0eb573e9a86d9574eaed7b27a13"><span class="id" title="notation">(</span></a>@<a class="idref" href="mathcomp.fingroup.perm.html#odd_perm"><span class="id" title="definition">odd_perm</span></a> <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#034cc0eb573e9a86d9574eaed7b27a13"><span class="id" title="notation">)</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Alt_group</span> <span class="id" title="var">phT</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#ccb763a84253e971fd106aeeb9cd3cb0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ccb763a84253e971fd106aeeb9cd3cb0"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#ccb763a84253e971fd106aeeb9cd3cb0"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.alt.html#Alt"><span class="id" title="definition">Alt</span></a> <a class="idref" href="mathcomp.solvable.alt.html#phT"><span class="id" title="variable">phT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ccb763a84253e971fd106aeeb9cd3cb0"><span class="id" title="notation">]</span></a>.<br/> + +<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Alt_even"><span class="id" title="lemma">Alt_even</span></a> <span class="id" title="var">p</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.solvable.alt.html#p"><span class="id" title="variable">p</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.solvable.alt.html#406b51dfa4fc877443129b4a51a66748"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#406b51dfa4fc877443129b4a51a66748"><span class="id" title="notation">Alt_T</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="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="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.solvable.alt.html#p"><span class="id" title="variable">p</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Alt_subset"><span class="id" title="lemma">Alt_subset</span></a> : <a class="idref" href="mathcomp.solvable.alt.html#406b51dfa4fc877443129b4a51a66748"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#406b51dfa4fc877443129b4a51a66748"><span class="id" title="notation">Alt_T</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.solvable.alt.html#f32935784d160bf8a9cbdbd987859003"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#f32935784d160bf8a9cbdbd987859003"><span class="id" title="notation">Sym_T</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Alt_normal"><span class="id" title="lemma">Alt_normal</span></a> : <a class="idref" href="mathcomp.solvable.alt.html#406b51dfa4fc877443129b4a51a66748"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#406b51dfa4fc877443129b4a51a66748"><span class="id" title="notation">Alt_T</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#c27c638e534bbb5b7de2d4b4aa0a3e82"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.solvable.alt.html#f32935784d160bf8a9cbdbd987859003"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#f32935784d160bf8a9cbdbd987859003"><span class="id" title="notation">Sym_T</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Alt_norm"><span class="id" title="lemma">Alt_norm</span></a> : <a class="idref" href="mathcomp.solvable.alt.html#f32935784d160bf8a9cbdbd987859003"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#f32935784d160bf8a9cbdbd987859003"><span class="id" title="notation">Sym_T</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.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.alt.html#406b51dfa4fc877443129b4a51a66748"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#406b51dfa4fc877443129b4a51a66748"><span class="id" title="notation">Alt_T</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">)</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Let</span> <a name="SymAltDef.n"><span class="id" title="variable">n</span></a> := <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.T"><span class="id" title="variable">T</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">Lemma</span> <a name="Alt_index"><span class="id" title="lemma">Alt_index</span></a> : 1 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation"><</span></a> <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.n"><span class="id" title="variable">n</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#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.alt.html#f32935784d160bf8a9cbdbd987859003"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#f32935784d160bf8a9cbdbd987859003"><span class="id" title="notation">Sym_T</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.alt.html#406b51dfa4fc877443129b4a51a66748"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#406b51dfa4fc877443129b4a51a66748"><span class="id" title="notation">Alt_T</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><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> 2.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="card_Sym"><span class="id" title="lemma">card_Sym</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.alt.html#f32935784d160bf8a9cbdbd987859003"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#f32935784d160bf8a9cbdbd987859003"><span class="id" title="notation">Sym_T</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#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f2f331192ff43772ca561a371dde9740"><span class="id" title="notation">`!</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="card_Alt"><span class="id" title="lemma">card_Alt</span></a> : 1 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation"><</span></a> <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.n"><span class="id" title="variable">n</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> (2 <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.solvable.alt.html#406b51dfa4fc877443129b4a51a66748"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#406b51dfa4fc877443129b4a51a66748"><span class="id" title="notation">Alt_T</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#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f2f331192ff43772ca561a371dde9740"><span class="id" title="notation">`!</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Sym_trans"><span class="id" title="lemma">Sym_trans</span></a> : <a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">transitive</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.solvable.alt.html#f32935784d160bf8a9cbdbd987859003"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#f32935784d160bf8a9cbdbd987859003"><span class="id" title="notation">Sym_T</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#setT"><span class="id" title="abbreviation">setT</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.action.html#6e357cd64401db5e610bc455a18fd25f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#6e357cd64401db5e610bc455a18fd25f"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Alt_trans"><span class="id" title="lemma">Alt_trans</span></a> : <a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">transitive</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#b870774a3786e6850cf468108b4e1ee5"><span class="id" title="notation">.-2</span></a> <a class="idref" href="mathcomp.solvable.alt.html#406b51dfa4fc877443129b4a51a66748"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#406b51dfa4fc877443129b4a51a66748"><span class="id" title="notation">Alt_T</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#setT"><span class="id" title="abbreviation">setT</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.action.html#6e357cd64401db5e610bc455a18fd25f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#6e357cd64401db5e610bc455a18fd25f"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="aperm_faithful"><span class="id" title="lemma">aperm_faithful</span></a> (<span class="id" title="var">A</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.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) : <a class="idref" href="mathcomp.fingroup.action.html#6e1bf5287bfc6397badc2a71c227e8d0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#6e1bf5287bfc6397badc2a71c227e8d0"><span class="id" title="notation">faithful</span></a> <a class="idref" href="mathcomp.solvable.alt.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#6e1bf5287bfc6397badc2a71c227e8d0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#6e1bf5287bfc6397badc2a71c227e8d0"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#setT"><span class="id" title="abbreviation">setT</span></a> <a class="idref" href="mathcomp.fingroup.action.html#6e1bf5287bfc6397badc2a71c227e8d0"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.action.html#6e357cd64401db5e610bc455a18fd25f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#6e357cd64401db5e610bc455a18fd25f"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.fingroup.action.html#6e1bf5287bfc6397badc2a71c227e8d0"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.alt.html#SymAltDef"><span class="id" title="section">SymAltDef</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="aaf7cf9086a45aa8e70b0083fabd82dd"><span class="id" title="notation">"</span></a>''Sym_' T" := (<a class="idref" href="mathcomp.solvable.alt.html#Sym"><span class="id" title="definition">Sym</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">T</span>))<br/> + (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8, <span class="id" title="var">T</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">format</span> "''Sym_' T") : <span class="id" title="var">group_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="0af815391ca483d74a2e8bf97e897bcd"><span class="id" title="notation">"</span></a>''Sym_' T" := (<a class="idref" href="mathcomp.solvable.alt.html#Sym_group"><span class="id" title="definition">Sym_group</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">T</span>)) : <span class="id" title="var">Group_scope</span>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="083c0e28f35f28a3c1e1db2408b44720"><span class="id" title="notation">"</span></a>''Alt_' T" := (<a class="idref" href="mathcomp.solvable.alt.html#Alt"><span class="id" title="definition">Alt</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">T</span>))<br/> + (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8, <span class="id" title="var">T</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">format</span> "''Alt_' T") : <span class="id" title="var">group_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="692a66efc3505aab1e6d19a56b8b0139"><span class="id" title="notation">"</span></a>''Alt_' T" := (<a class="idref" href="mathcomp.solvable.alt.html#Alt_group"><span class="id" title="definition">Alt_group</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">T</span>)) : <span class="id" title="var">Group_scope</span>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="trivial_Alt_2"><span class="id" title="lemma">trivial_Alt_2</span></a> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.alt.html#T"><span class="id" title="variable">T</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 <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.alt.html#083c0e28f35f28a3c1e1db2408b44720"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#083c0e28f35f28a3c1e1db2408b44720"><span class="id" title="notation">Alt_T</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> 1.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="simple_Alt_3"><span class="id" title="lemma">simple_Alt_3</span></a> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.alt.html#T"><span class="id" title="variable">T</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#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 3 <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.gseries.html#simple"><span class="id" title="definition">simple</span></a> <a class="idref" href="mathcomp.solvable.alt.html#083c0e28f35f28a3c1e1db2408b44720"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#083c0e28f35f28a3c1e1db2408b44720"><span class="id" title="notation">Alt_T</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="not_simple_Alt_4"><span class="id" title="lemma">not_simple_Alt_4</span></a> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.alt.html#T"><span class="id" title="variable">T</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#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 4 <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.solvable.gseries.html#simple"><span class="id" title="definition">simple</span></a> <a class="idref" href="mathcomp.solvable.alt.html#083c0e28f35f28a3c1e1db2408b44720"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#083c0e28f35f28a3c1e1db2408b44720"><span class="id" title="notation">Alt_T</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="simple_Alt5_base"><span class="id" title="lemma">simple_Alt5_base</span></a> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.alt.html#T"><span class="id" title="variable">T</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#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 5 <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.gseries.html#simple"><span class="id" title="definition">simple</span></a> <a class="idref" href="mathcomp.solvable.alt.html#083c0e28f35f28a3c1e1db2408b44720"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#083c0e28f35f28a3c1e1db2408b44720"><span class="id" title="notation">Alt_T</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="Restrict"><span class="id" title="section">Restrict</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="Restrict.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) (<a name="Restrict.x"><span class="id" title="variable">x</span></a> : <a class="idref" href="mathcomp.solvable.alt.html#T"><span class="id" title="variable">T</span></a>).<br/> +<span class="id" title="keyword">Notation</span> <a name="T'"><span class="id" title="abbreviation">T'</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">y</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.solvable.alt.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.solvable.alt.html#Restrict.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>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="rfd_funP"><span class="id" title="lemma">rfd_funP</span></a> (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.solvable.alt.html#Restrict.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">u</span> : <a class="idref" href="mathcomp.solvable.alt.html#T'"><span class="id" title="abbreviation">T'</span></a>) :<br/> + <span class="id" title="keyword">let</span> <span class="id" title="var">p1</span> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.solvable.alt.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.solvable.alt.html#Restrict.x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.solvable.alt.html#Restrict.x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">then</span></a> <a class="idref" href="mathcomp.solvable.alt.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">else</span></a> 1 <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.solvable.alt.html#p1"><span class="id" title="variable">p1</span></a> (<a class="idref" href="mathcomp.ssreflect.eqtype.html#val"><span class="id" title="projection">val</span></a> <a class="idref" href="mathcomp.solvable.alt.html#u"><span class="id" title="variable">u</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.solvable.alt.html#Restrict.x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="rfd_fun"><span class="id" title="definition">rfd_fun</span></a> <span class="id" title="var">p</span> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#0bba0687209e799f52ace6d4b2c6d64a"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#0bba0687209e799f52ace6d4b2c6d64a"><span class="id" title="notation">fun</span></a> <span class="id" title="var">u</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#0bba0687209e799f52ace6d4b2c6d64a"><span class="id" title="notation">⇒</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#Sub"><span class="id" title="projection">Sub</span></a> ((<span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#4509b22bf26e3d6d771897e22bd8bc8f"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.solvable.alt.html#Restrict.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">}</span></a>) <span class="id" title="var">_</span>) (<a class="idref" href="mathcomp.solvable.alt.html#rfd_funP"><span class="id" title="lemma">rfd_funP</span></a> <a class="idref" href="mathcomp.solvable.alt.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.solvable.alt.html#u"><span class="id" title="variable">u</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#4509b22bf26e3d6d771897e22bd8bc8f"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.alt.html#T'"><span class="id" title="abbreviation">T'</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#0bba0687209e799f52ace6d4b2c6d64a"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="rfdP"><span class="id" title="lemma">rfdP</span></a> <span class="id" title="var">p</span> : <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.solvable.alt.html#rfd_fun"><span class="id" title="definition">rfd_fun</span></a> <a class="idref" href="mathcomp.solvable.alt.html#p"><span class="id" title="variable">p</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="rfd"><span class="id" title="definition">rfd</span></a> <span class="id" title="var">p</span> := <a class="idref" href="mathcomp.fingroup.perm.html#perm"><span class="id" title="abbreviation">perm</span></a> (@<a class="idref" href="mathcomp.solvable.alt.html#rfdP"><span class="id" title="lemma">rfdP</span></a> <a class="idref" href="mathcomp.solvable.alt.html#p"><span class="id" title="variable">p</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Hypothesis</span> <a name="Restrict.card_T"><span class="id" title="variable">card_T</span></a> : 2 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><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.solvable.alt.html#Restrict.T"><span class="id" title="variable">T</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">Lemma</span> <a name="rfd_morph"><span class="id" title="lemma">rfd_morph</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.action.html#1fb3703b929cf964cd25eac50eea7151"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#1fb3703b929cf964cd25eac50eea7151"><span class="id" title="notation">C_</span></a><a class="idref" href="mathcomp.fingroup.action.html#1fb3703b929cf964cd25eac50eea7151"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.alt.html#aaf7cf9086a45aa8e70b0083fabd82dd"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#aaf7cf9086a45aa8e70b0083fabd82dd"><span class="id" title="notation">Sym_T</span></a><a class="idref" href="mathcomp.fingroup.action.html#1fb3703b929cf964cd25eac50eea7151"><span class="id" title="notation">)[</span></a><a class="idref" href="mathcomp.solvable.alt.html#Restrict.x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.action.html#1fb3703b929cf964cd25eac50eea7151"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.action.html#6e357cd64401db5e610bc455a18fd25f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#6e357cd64401db5e610bc455a18fd25f"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.fingroup.action.html#1fb3703b929cf964cd25eac50eea7151"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">&,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.solvable.alt.html#rfd"><span class="id" title="definition">rfd</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">:</span></a> <span class="id" title="var">y</span> <span class="id" title="var">z</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.alt.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.solvable.alt.html#z"><span class="id" title="variable">z</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">rfd_morphism</span> := <a class="idref" href="mathcomp.fingroup.morphism.html#Morphism"><span class="id" title="constructor">Morphism</span></a> <a class="idref" href="mathcomp.solvable.alt.html#rfd_morph"><span class="id" title="lemma">rfd_morph</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="rgd_fun"><span class="id" title="definition">rgd_fun</span></a> (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.solvable.alt.html#T'"><span class="id" title="abbreviation">T'</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><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#0bba0687209e799f52ace6d4b2c6d64a"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#0bba0687209e799f52ace6d4b2c6d64a"><span class="id" title="notation">fun</span></a> <span class="id" title="var">x1</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#0bba0687209e799f52ace6d4b2c6d64a"><span class="id" title="notation">⇒</span></a> <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#insub"><span class="id" title="definition">insub</span></a> <a class="idref" href="mathcomp.solvable.alt.html#x1"><span class="id" title="variable">x1</span></a> <span class="id" title="keyword">is</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">u</span> <span class="id" title="keyword">then</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#sval"><span class="id" title="abbreviation">sval</span></a> (<a class="idref" href="mathcomp.solvable.alt.html#p"><span class="id" title="variable">p</span></a> <span class="id" title="var">u</span>) <span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.solvable.alt.html#Restrict.x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#0bba0687209e799f52ace6d4b2c6d64a"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="rgdP"><span class="id" title="lemma">rgdP</span></a> <span class="id" title="var">p</span> : <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.solvable.alt.html#rgd_fun"><span class="id" title="definition">rgd_fun</span></a> <a class="idref" href="mathcomp.solvable.alt.html#p"><span class="id" title="variable">p</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="rgd"><span class="id" title="definition">rgd</span></a> <span class="id" title="var">p</span> := <a class="idref" href="mathcomp.fingroup.perm.html#perm"><span class="id" title="abbreviation">perm</span></a> (@<a class="idref" href="mathcomp.solvable.alt.html#rgdP"><span class="id" title="lemma">rgdP</span></a> <a class="idref" href="mathcomp.solvable.alt.html#p"><span class="id" title="variable">p</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="rfd_odd"><span class="id" title="lemma">rfd_odd</span></a> (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.solvable.alt.html#Restrict.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.perm.html#8787ba8c1ae558dde17e1bdb8427679e"><span class="id" title="notation">}</span></a>) : <a class="idref" href="mathcomp.solvable.alt.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.solvable.alt.html#Restrict.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> <a class="idref" href="mathcomp.solvable.alt.html#Restrict.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#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.alt.html#rfd"><span class="id" title="definition">rfd</span></a> <a class="idref" href="mathcomp.solvable.alt.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#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.alt.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#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:></span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="rfd_iso"><span class="id" title="lemma">rfd_iso</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#1fb3703b929cf964cd25eac50eea7151"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#1fb3703b929cf964cd25eac50eea7151"><span class="id" title="notation">C_</span></a><a class="idref" href="mathcomp.fingroup.action.html#1fb3703b929cf964cd25eac50eea7151"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.alt.html#083c0e28f35f28a3c1e1db2408b44720"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#083c0e28f35f28a3c1e1db2408b44720"><span class="id" title="notation">Alt_T</span></a><a class="idref" href="mathcomp.fingroup.action.html#1fb3703b929cf964cd25eac50eea7151"><span class="id" title="notation">)[</span></a><a class="idref" href="mathcomp.solvable.alt.html#Restrict.x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.action.html#1fb3703b929cf964cd25eac50eea7151"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.action.html#6e357cd64401db5e610bc455a18fd25f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#6e357cd64401db5e610bc455a18fd25f"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.fingroup.action.html#1fb3703b929cf964cd25eac50eea7151"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.alt.html#083c0e28f35f28a3c1e1db2408b44720"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#083c0e28f35f28a3c1e1db2408b44720"><span class="id" title="notation">Alt_T'</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.alt.html#Restrict"><span class="id" title="section">Restrict</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="simple_Alt5"><span class="id" title="lemma">simple_Alt5</span></a> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.alt.html#T"><span class="id" title="variable">T</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#08fe8636f4b45ae6787c490d19de1366"><span class="id" title="notation">≥</span></a> 5 <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.gseries.html#simple"><span class="id" title="definition">simple</span></a> <a class="idref" href="mathcomp.solvable.alt.html#083c0e28f35f28a3c1e1db2408b44720"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#083c0e28f35f28a3c1e1db2408b44720"><span class="id" title="notation">Alt_T</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 |