diff options
Diffstat (limited to 'docs/htmldoc/mathcomp.solvable.alt.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.solvable.alt.html | 198 |
1 files changed, 0 insertions, 198 deletions
diff --git a/docs/htmldoc/mathcomp.solvable.alt.html b/docs/htmldoc/mathcomp.solvable.alt.html deleted file mode 100644 index f94a27f..0000000 --- a/docs/htmldoc/mathcomp.solvable.alt.html +++ /dev/null @@ -1,198 +0,0 @@ -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" -"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> -<html xmlns="http://www.w3.org/1999/xhtml"> -<head> -<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> -<link href="coqdoc.css" rel="stylesheet" type="text/css" /> -<title>mathcomp.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/> - -<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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#addbA"><span class="id" title="lemma">addbA</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#addFb"><span class="id" title="lemma">addFb</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.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/V8.9.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/V8.9.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#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><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#683bed2e43e8b9b52492c89e618e34b6"><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/V8.9.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#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><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#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><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#f6996ff347e6cf832aa130837b06a848"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#f6996ff347e6cf832aa130837b06a848"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f6996ff347e6cf832aa130837b06a848"><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#f6996ff347e6cf832aa130837b06a848"><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#8862e848ccf2a2502b30843c5961bc5d"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#8862e848ccf2a2502b30843c5961bc5d"><span class="id" title="notation">Sym_T</span></a> <span class="id" title="var">_</span> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.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/V8.9.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#7ef99623452370540bbc44fd30b0bc94"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#7ef99623452370540bbc44fd30b0bc94"><span class="id" title="notation">ker</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#7ef99623452370540bbc44fd30b0bc94"><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#7ef99623452370540bbc44fd30b0bc94"><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#f6996ff347e6cf832aa130837b06a848"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#f6996ff347e6cf832aa130837b06a848"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f6996ff347e6cf832aa130837b06a848"><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#f6996ff347e6cf832aa130837b06a848"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.alt.html#f2ad636ea36e028382f20273ca6ed6f8"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#f2ad636ea36e028382f20273ca6ed6f8"><span class="id" title="notation">Alt_T</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b3ebd0deddd84fd60e149cb5ef719351"><span class="id" title="notation">~~</span></a> <a class="idref" href="mathcomp.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#f2ad636ea36e028382f20273ca6ed6f8"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#f2ad636ea36e028382f20273ca6ed6f8"><span class="id" title="notation">Alt_T</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.alt.html#8862e848ccf2a2502b30843c5961bc5d"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#8862e848ccf2a2502b30843c5961bc5d"><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#f2ad636ea36e028382f20273ca6ed6f8"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#f2ad636ea36e028382f20273ca6ed6f8"><span class="id" title="notation">Alt_T</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7e8095b432e7aa5c3c22bb87584658b7"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.solvable.alt.html#8862e848ccf2a2502b30843c5961bc5d"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#8862e848ccf2a2502b30843c5961bc5d"><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#8862e848ccf2a2502b30843c5961bc5d"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#8862e848ccf2a2502b30843c5961bc5d"><span class="id" title="notation">Sym_T</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.alt.html#f2ad636ea36e028382f20273ca6ed6f8"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#f2ad636ea36e028382f20273ca6ed6f8"><span class="id" title="notation">Alt_T</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><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#234f50e13366f794cd6877cf832a5935"><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#234f50e13366f794cd6877cf832a5935"><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#00fe0eaf5e6949f0a31725357afa4bba"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.alt.html#8862e848ccf2a2502b30843c5961bc5d"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#8862e848ccf2a2502b30843c5961bc5d"><span class="id" title="notation">Sym_T</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.alt.html#f2ad636ea36e028382f20273ca6ed6f8"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#f2ad636ea36e028382f20273ca6ed6f8"><span class="id" title="notation">Alt_T</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 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#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.alt.html#8862e848ccf2a2502b30843c5961bc5d"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#8862e848ccf2a2502b30843c5961bc5d"><span class="id" title="notation">Sym_T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#fb85b56582e20c3ab47a4e55b1f6f111"><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#00fe0eaf5e6949f0a31725357afa4bba"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> (2 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.alt.html#f2ad636ea36e028382f20273ca6ed6f8"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#f2ad636ea36e028382f20273ca6ed6f8"><span class="id" title="notation">Alt_T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a>)%<span class="id" title="var">N</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#fb85b56582e20c3ab47a4e55b1f6f111"><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#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">transitive</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><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#8862e848ccf2a2502b30843c5961bc5d"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#8862e848ccf2a2502b30843c5961bc5d"><span class="id" title="notation">Sym_T</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><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#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.action.html#3eb38e105ce23aabcb8ebe6af6d1b8af"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#3eb38e105ce23aabcb8ebe6af6d1b8af"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><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#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">transitive</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><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#b9f3db5365f11e72cad3907646ac5a3a"><span class="id" title="notation">.-2</span></a> <a class="idref" href="mathcomp.solvable.alt.html#f2ad636ea36e028382f20273ca6ed6f8"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#f2ad636ea36e028382f20273ca6ed6f8"><span class="id" title="notation">Alt_T</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><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#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.action.html#3eb38e105ce23aabcb8ebe6af6d1b8af"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#3eb38e105ce23aabcb8ebe6af6d1b8af"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><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#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) : <a class="idref" href="mathcomp.fingroup.action.html#b33bbd7f4609361a5f6c220c33141a0c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#b33bbd7f4609361a5f6c220c33141a0c"><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#b33bbd7f4609361a5f6c220c33141a0c"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#b33bbd7f4609361a5f6c220c33141a0c"><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#b33bbd7f4609361a5f6c220c33141a0c"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.action.html#3eb38e105ce23aabcb8ebe6af6d1b8af"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#3eb38e105ce23aabcb8ebe6af6d1b8af"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.fingroup.action.html#b33bbd7f4609361a5f6c220c33141a0c"><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="5639f842b98f65df33b56e1d8d4a2946"><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/V8.9.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="fc8e40fe0cb216ea2f594c2c63586038"><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/V8.9.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="c6380dd602db0fe4c329837012a38954"><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/V8.9.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="988d46c711db28d95b743bfa12c213c4"><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/V8.9.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#234f50e13366f794cd6877cf832a5935"><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#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#cb53cf0ee22c036a03b4a9281c68b5a3"><span class="id" title="notation">≤</span></a> 2 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.alt.html#c6380dd602db0fe4c329837012a38954"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#c6380dd602db0fe4c329837012a38954"><span class="id" title="notation">Alt_T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 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#234f50e13366f794cd6877cf832a5935"><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#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 3 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#simple"><span class="id" title="definition">simple</span></a> <a class="idref" href="mathcomp.solvable.alt.html#c6380dd602db0fe4c329837012a38954"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#c6380dd602db0fe4c329837012a38954"><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#234f50e13366f794cd6877cf832a5935"><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#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 4 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b3ebd0deddd84fd60e149cb5ef719351"><span class="id" title="notation">~~</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#simple"><span class="id" title="definition">simple</span></a> <a class="idref" href="mathcomp.solvable.alt.html#c6380dd602db0fe4c329837012a38954"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#c6380dd602db0fe4c329837012a38954"><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#234f50e13366f794cd6877cf832a5935"><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#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 5 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#simple"><span class="id" title="definition">simple</span></a> <a class="idref" href="mathcomp.solvable.alt.html#c6380dd602db0fe4c329837012a38954"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#c6380dd602db0fe4c329837012a38954"><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/V8.9.0/stdlib//Coq.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><span class="id" title="notation">{</span></a><span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><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#c385a484ee9d1b4e0615924561a9b75e"><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/V8.9.0/stdlib//Coq.Init.Specif.html#bc4528e836ab0e91ea7e942fb09e898f"><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#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><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#683bed2e43e8b9b52492c89e618e34b6"><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/V8.9.0/stdlib//Coq.ssr.ssreflect.html#00a1a5b58aac8f1e3f1abff064a39f9d"><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#df45e8c2e8370fd4f0f7c4fdaf208180"><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/V8.9.0/stdlib//Coq.ssr.ssreflect.html#00a1a5b58aac8f1e3f1abff064a39f9d"><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/V8.9.0/stdlib//Coq.ssr.ssreflect.html#00a1a5b58aac8f1e3f1abff064a39f9d"><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#c385a484ee9d1b4e0615924561a9b75e"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8486b0ff5bfed6f6875afb7a9befbceb"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8486b0ff5bfed6f6875afb7a9befbceb"><span class="id" title="notation">fun</span></a> <span class="id" title="var">u</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8486b0ff5bfed6f6875afb7a9befbceb"><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/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><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#683bed2e43e8b9b52492c89e618e34b6"><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/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8486b0ff5bfed6f6875afb7a9befbceb"><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/V8.9.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#00fe0eaf5e6949f0a31725357afa4bba"><span class="id" title="notation"><</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.alt.html#Restrict.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="rfd_morph"><span class="id" title="lemma">rfd_morph</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.action.html#24b4379335336f15427bd11e0177a7fb"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#24b4379335336f15427bd11e0177a7fb"><span class="id" title="notation">C_</span></a><a class="idref" href="mathcomp.fingroup.action.html#24b4379335336f15427bd11e0177a7fb"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.alt.html#5639f842b98f65df33b56e1d8d4a2946"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#5639f842b98f65df33b56e1d8d4a2946"><span class="id" title="notation">Sym_T</span></a><a class="idref" href="mathcomp.fingroup.action.html#24b4379335336f15427bd11e0177a7fb"><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#24b4379335336f15427bd11e0177a7fb"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.action.html#3eb38e105ce23aabcb8ebe6af6d1b8af"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#3eb38e105ce23aabcb8ebe6af6d1b8af"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.fingroup.action.html#24b4379335336f15427bd11e0177a7fb"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">&,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><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#8b8794efbfbae1b793d9cb62ce802285"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><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#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><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#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">}</span></a>) :=<br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8486b0ff5bfed6f6875afb7a9befbceb"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8486b0ff5bfed6f6875afb7a9befbceb"><span class="id" title="notation">fun</span></a> <span class="id" title="var">x1</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8486b0ff5bfed6f6875afb7a9befbceb"><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/V8.9.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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8486b0ff5bfed6f6875afb7a9befbceb"><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/V8.9.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#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><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#683bed2e43e8b9b52492c89e618e34b6"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><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/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">:></span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.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#24b4379335336f15427bd11e0177a7fb"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#24b4379335336f15427bd11e0177a7fb"><span class="id" title="notation">C_</span></a><a class="idref" href="mathcomp.fingroup.action.html#24b4379335336f15427bd11e0177a7fb"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.alt.html#c6380dd602db0fe4c329837012a38954"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#c6380dd602db0fe4c329837012a38954"><span class="id" title="notation">Alt_T</span></a><a class="idref" href="mathcomp.fingroup.action.html#24b4379335336f15427bd11e0177a7fb"><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#24b4379335336f15427bd11e0177a7fb"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.action.html#3eb38e105ce23aabcb8ebe6af6d1b8af"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#3eb38e105ce23aabcb8ebe6af6d1b8af"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.fingroup.action.html#24b4379335336f15427bd11e0177a7fb"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.alt.html#c6380dd602db0fe4c329837012a38954"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#c6380dd602db0fe4c329837012a38954"><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#234f50e13366f794cd6877cf832a5935"><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#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#73030c22bc0b1fa771c65aa5414c65f9"><span class="id" title="notation">≥</span></a> 5 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#simple"><span class="id" title="definition">simple</span></a> <a class="idref" href="mathcomp.solvable.alt.html#c6380dd602db0fe4c329837012a38954"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.alt.html#c6380dd602db0fe4c329837012a38954"><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 |