generate the documentation for 1.7

author: Enrico Tassi 2018-04-20 10:54:22 +0200
committer: Enrico Tassi 2018-04-20 10:54:22 +0200
commit: ed05182cece6bb3706e09b2ce14af4a41a2e8141 (patch)
tree: e850d7314b6372d0476cf2ffaf7d3830721db7b1 /docs/htmldoc/mathcomp.solvable.jordanholder.html
parent: 3d196f44681fb3b23ff8a79fbd44e12308680531 (diff)
1 files changed, 431 insertions, 0 deletions
diff --git a/docs/htmldoc/mathcomp.solvable.jordanholder.html b/docs/htmldoc/mathcomp.solvable.jordanholder.html
new file mode 100644
index 0000000..267e1a4
--- /dev/null
+++ b/docs/htmldoc/mathcomp.solvable.jordanholder.html
@@ -0,0 +1,431 @@
+<!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.jordanholder</title>
+</head>
+
+<body>
+
+<div id="page">
+
+<div id="header">
+</div>
+
+<div id="main">
+
+<h1 class="libtitle">Library mathcomp.solvable.jordanholder</h1>
+
+<div class="code">
+<span class="comment">(*&nbsp;(c)&nbsp;Copyright&nbsp;2006-2016&nbsp;Microsoft&nbsp;Corporation&nbsp;and&nbsp;Inria.&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br/>
+&nbsp;Distributed&nbsp;under&nbsp;the&nbsp;terms&nbsp;of&nbsp;CeCILL-B.&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;*)</span><br/>
+<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#"><span class="id" title="library">mathcomp.ssreflect.ssreflect</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ This files establishes Jordan-Holder theorems for finite groups. These     
+ theorems state the uniqueness up to permutation and isomorphism for the    
+ series of quotient built from the successive elements of any composition   
+ series of the same group. These quotients are also called factors of the   
+ composition series. To avoid the heavy use of highly polymorphic lists     
+ describing these quotient series, we introduce sections.                   
+ This library defines:                                                      
+         (G1 / G2)%sec == alias for the pair (G1, G2) of groups in the same 
+                          finGroupType, coerced to the actual quotient group
+                          group G1 / G2. We call this pseudo-quotient a     
+                          section of G1 and G2.                             
+    section_isog s1 s2 == s1 and s2 respectively coerce to isomorphic       
+                          quotient groups.                                  
+        section_repr s == canonical representative of the isomorphism class 
+                          of the section s.                                 
+         mksrepr G1 G2 == canonical representative of the isomorphism class 
+                          of (G1 / G2)%sec.                                 
+         mkfactors G s == if s is [:: s1, s2, ..., sn], constructs the list 
+                     [:: mksrepr G s1, mksrepr s1 s2, ..., mksrepr sn-1 sn] 
+             comps G s == s is a composition series for G i.e. s is a       
+                          decreasing sequence of subgroups of G             
+                          in which two adjacent elements are maxnormal one  
+                          in the other and the last element of s is 1.      
+ Given aT and rT two finGroupTypes, (D : {group rT}), (A : {group aT}) and  
+ (to : groupAction A D) an external action.                                 
+        maxainv to B C == C is a maximal proper normal subgroup of B        
+                          invariant by (the external action of A via) to.   
+          asimple to B == the maximal proper normal subgroup of B invariant 
+                          by the external action to is trivial.             
+         acomps to G s == s is a composition series for G invariant by to,  
+                          i.e. s is a decreasing sequence of subgroups of G 
+                          in which two adjacent elements are maximally      
+                          invariant by to one in the other and the          
+                          last element of s is 1.                           
+ We prove two versions of the result:                                       
+<ul class="doclist">
+<li> JordanHolderUniqueness establishes the uniqueness up to permutation   
+       and isomorphism of the lists of factors in composition series of a   
+       given group.                                                         
+
+</li>
+<li> StrongJordanHolderUniqueness extends the result to composition series 
+       invariant by an external group action.                               
+
+</li>
+</ul>
+ See also "The Rooster and the Butterflies", proceedings of Calculemus 2013,
+ by Assia Mahboubi.                                                          
+</div>
+<div class="code">
+
+<br/>
+<span class="id" title="keyword">Import</span> <span class="id" title="var">GroupScope</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Set Implicit Arguments</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Inductive</span> <a name="section"><span class="id" title="inductive">section</span></a> (<span class="id" title="var">gT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) := <a name="GSection"><span class="id" title="constructor">GSection</span></a> <span class="id" title="keyword">of</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.solvable.jordanholder.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><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.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Delimit</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">section_scope</span> <span class="id" title="keyword">with</span> <span class="id" title="var">sec</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="mkSec"><span class="id" title="definition">mkSec</span></a> (<span class="id" title="var">gT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<span class="id" title="var">G1</span> <span class="id" title="var">G2</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.solvable.jordanholder.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) := <a class="idref" href="mathcomp.solvable.jordanholder.html#GSection"><span class="id" title="constructor">GSection</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.jordanholder.html#G1"><span class="id" title="variable">G1</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#G2"><span class="id" title="variable">G2</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Infix</span> <a name="173b3ede47946e274e545159d060f62f"><span class="id" title="notation">&quot;</span></a>/" := <a class="idref" href="mathcomp.solvable.jordanholder.html#mkSec"><span class="id" title="definition">mkSec</span></a> : <span class="id" title="var">section_scope</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Coercion</span> <span class="id" title="var">pair_of_section</span> <span class="id" title="var">gT</span> (<span class="id" title="var">s</span> : <a class="idref" href="mathcomp.solvable.jordanholder.html#section"><span class="id" title="inductive">section</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#gT"><span class="id" title="variable">gT</span></a>) := <span class="id" title="keyword">let</span>: <a class="idref" href="mathcomp.solvable.jordanholder.html#GSection"><span class="id" title="constructor">GSection</span></a> <span class="id" title="var">u</span> := <a class="idref" href="mathcomp.solvable.jordanholder.html#s"><span class="id" title="variable">s</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">u</span>.<br/>
+
+<br/>
+<span class="id" title="keyword">Coercion</span> <span class="id" title="var">quotient_of_section</span> <span class="id" title="var">gT</span> (<span class="id" title="var">s</span> : <a class="idref" href="mathcomp.solvable.jordanholder.html#section"><span class="id" title="inductive">section</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#gT"><span class="id" title="variable">gT</span></a>) : <a class="idref" href="mathcomp.fingroup.fingroup.html#GroupSet.sort"><span class="id" title="definition">GroupSet.sort</span></a> <span class="id" title="var">_</span> := <a class="idref" href="mathcomp.solvable.jordanholder.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c4877bbfe60d8f22b47ac99ace86216a"><span class="id" title="notation">.1</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#c7768147d2d560601601fbf95706ddcc"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#f4827404159513e7fd691b60b7877737"><span class="id" title="notation">.2</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Coercion</span> <span class="id" title="var">section_group</span> <span class="id" title="var">gT</span> (<span class="id" title="var">s</span> : <a class="idref" href="mathcomp.solvable.jordanholder.html#section"><span class="id" title="inductive">section</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#gT"><span class="id" title="variable">gT</span></a>) : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.quotient.html#coset_of"><span class="id" title="record">coset_of</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#f4827404159513e7fd691b60b7877737"><span class="id" title="notation">.2</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">)}</span></a> :=<br/>
+&nbsp;&nbsp;<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.jordanholder.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ccb763a84253e971fd106aeeb9cd3cb0"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="Sections"><span class="id" title="section">Sections</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variables</span> (<a name="Sections.gT"><span class="id" title="variable">gT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>).<br/>
+<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#Sections.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">s</span> : <a class="idref" href="mathcomp.solvable.jordanholder.html#section"><span class="id" title="inductive">section</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#Sections.gT"><span class="id" title="variable">gT</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">section_subType</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.ssreflect.eqtype.html#d716e206e5129c6b3a60f0f640eaaeb0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#d716e206e5129c6b3a60f0f640eaaeb0"><span class="id" title="notation">newType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#d716e206e5129c6b3a60f0f640eaaeb0"><span class="id" title="notation">for</span></a> @<a class="idref" href="mathcomp.solvable.jordanholder.html#pair_of_section"><span class="id" title="definition">pair_of_section</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#Sections.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#d716e206e5129c6b3a60f0f640eaaeb0"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="section_eqMixin"><span class="id" title="definition">section_eqMixin</span></a> := <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.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">eqMixin</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#section"><span class="id" title="inductive">section</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#Sections.gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">&lt;:]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">section_eqType</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.ssreflect.eqtype.html#Equality.Exports.EqType"><span class="id" title="abbreviation">EqType</span></a> (<a class="idref" href="mathcomp.solvable.jordanholder.html#section"><span class="id" title="inductive">section</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#Sections.gT"><span class="id" title="variable">gT</span></a>) <a class="idref" href="mathcomp.solvable.jordanholder.html#section_eqMixin"><span class="id" title="definition">section_eqMixin</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="section_choiceMixin"><span class="id" title="definition">section_choiceMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">choiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#section"><span class="id" title="inductive">section</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#Sections.gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">&lt;:]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">section_choiceType</span> :=<br/>
+&nbsp;&nbsp;<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.ssreflect.choice.html#Choice.Exports.ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> (<a class="idref" href="mathcomp.solvable.jordanholder.html#section"><span class="id" title="inductive">section</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#Sections.gT"><span class="id" title="variable">gT</span></a>) <a class="idref" href="mathcomp.solvable.jordanholder.html#section_choiceMixin"><span class="id" title="definition">section_choiceMixin</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="section_countMixin"><span class="id" title="definition">section_countMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">countMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#section"><span class="id" title="inductive">section</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#Sections.gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">&lt;:]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">section_countType</span> :=<br/>
+&nbsp;&nbsp;<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.ssreflect.choice.html#Countable.Exports.CountType"><span class="id" title="abbreviation">CountType</span></a> (<a class="idref" href="mathcomp.solvable.jordanholder.html#section"><span class="id" title="inductive">section</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#Sections.gT"><span class="id" title="variable">gT</span></a>) <a class="idref" href="mathcomp.solvable.jordanholder.html#section_countMixin"><span class="id" title="definition">section_countMixin</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">section_subCountType</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.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">subCountType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#section"><span class="id" title="inductive">section</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#Sections.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="section_finMixin"><span class="id" title="definition">section_finMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.fintype.html#8c180561768185dd10396a5d3615104a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#8c180561768185dd10396a5d3615104a"><span class="id" title="notation">finMixin</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#8c180561768185dd10396a5d3615104a"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#section"><span class="id" title="inductive">section</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#Sections.gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#8c180561768185dd10396a5d3615104a"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#8c180561768185dd10396a5d3615104a"><span class="id" title="notation">&lt;:]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">section_finType</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.ssreflect.fintype.html#Finite.Exports.FinType"><span class="id" title="abbreviation">FinType</span></a> (<a class="idref" href="mathcomp.solvable.jordanholder.html#section"><span class="id" title="inductive">section</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#Sections.gT"><span class="id" title="variable">gT</span></a>) <a class="idref" href="mathcomp.solvable.jordanholder.html#section_finMixin"><span class="id" title="definition">section_finMixin</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">section_subFinType</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.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">subFinType</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#section"><span class="id" title="inductive">section</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#Sections.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">section_group</span>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ Isomorphic sections  
+</div>
+<div class="code">
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="section_isog"><span class="id" title="definition">section_isog</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#a3fa885266d530b93c1b9f67891df8e8"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#a3fa885266d530b93c1b9f67891df8e8"><span class="id" title="notation">rel</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#a3fa885266d530b93c1b9f67891df8e8"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#section"><span class="id" title="inductive">section</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#Sections.gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#a3fa885266d530b93c1b9f67891df8e8"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#x"><span class="id" title="variable">x</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.jordanholder.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#a3fa885266d530b93c1b9f67891df8e8"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ A witness of the isomorphism class of a section  
+</div>
+<div class="code">
+<span class="id" title="keyword">Definition</span> <a name="section_repr"><span class="id" title="definition">section_repr</span></a> <span class="id" title="var">s</span> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#odflt"><span class="id" title="abbreviation">odflt</span></a> (1 <a class="idref" href="mathcomp.solvable.jordanholder.html#173b3ede47946e274e545159d060f62f"><span class="id" title="notation">/</span></a> 1)%<span class="id" title="var">sec</span> (<a class="idref" href="mathcomp.ssreflect.fintype.html#pick"><span class="id" title="definition">pick</span></a> (<a class="idref" href="mathcomp.solvable.jordanholder.html#section_isog"><span class="id" title="definition">section_isog</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#8f28bbd804547edd8de802d63ef85617"><span class="id" title="notation">^~</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s"><span class="id" title="variable">s</span></a>)).<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="mksrepr"><span class="id" title="definition">mksrepr</span></a> <span class="id" title="var">G1</span> <span class="id" title="var">G2</span> := <a class="idref" href="mathcomp.solvable.jordanholder.html#section_repr"><span class="id" title="definition">section_repr</span></a> (<a class="idref" href="mathcomp.solvable.jordanholder.html#mkSec"><span class="id" title="definition">mkSec</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#G1"><span class="id" title="variable">G1</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#G2"><span class="id" title="variable">G2</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="section_reprP"><span class="id" title="lemma">section_reprP</span></a> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.solvable.jordanholder.html#section_repr"><span class="id" title="definition">section_repr</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s"><span class="id" title="variable">s</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.jordanholder.html#s"><span class="id" title="variable">s</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="section_repr_isog"><span class="id" title="lemma">section_repr_isog</span></a> <span class="id" title="var">s1</span> <span class="id" title="var">s2</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.jordanholder.html#s1"><span class="id" title="variable">s1</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.jordanholder.html#s2"><span class="id" title="variable">s2</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.jordanholder.html#section_repr"><span class="id" title="definition">section_repr</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s1"><span class="id" title="variable">s1</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.jordanholder.html#section_repr"><span class="id" title="definition">section_repr</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s2"><span class="id" title="variable">s2</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="mkfactors"><span class="id" title="definition">mkfactors</span></a> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#Sections.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">s</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#Sections.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) :=<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#section_repr"><span class="id" title="definition">section_repr</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#pairmap"><span class="id" title="definition">pairmap</span></a> (@<a class="idref" href="mathcomp.solvable.jordanholder.html#mkSec"><span class="id" title="definition">mkSec</span></a> <span class="id" title="var">_</span>) <a class="idref" href="mathcomp.solvable.jordanholder.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s"><span class="id" title="variable">s</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.jordanholder.html#Sections"><span class="id" title="section">Sections</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="CompositionSeries"><span class="id" title="section">CompositionSeries</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variable</span> <a name="CompositionSeries.gT"><span class="id" title="variable">gT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>.<br/>
+<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.solvable.jordanholder.html#gTg"><span class="id" title="abbreviation">gTg</span></a>) (<span class="id" title="var">s</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#gTg"><span class="id" title="abbreviation">gTg</span></a>).<br/>
+
+<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="comps"><span class="id" title="definition">comps</span></a> <span class="id" title="var">G</span> <span class="id" title="var">s</span> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#last"><span class="id" title="definition">last</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> 1%<span class="id" title="var">G</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">&amp;&amp;</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#compo"><span class="id" title="abbreviation">compo</span></a><a class="idref" href="mathcomp.solvable.gseries.html#6efcb060d1407a4d44d9b1cb19cf1e04"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.gseries.html#6efcb060d1407a4d44d9b1cb19cf1e04"><span class="id" title="notation">series</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s"><span class="id" title="variable">s</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="compsP"><span class="id" title="lemma">compsP</span></a> <span class="id" title="var">G</span> <span class="id" title="var">s</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#last"><span class="id" title="definition">last</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s"><span class="id" title="variable">s</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%<span class="id" title="var">G</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a>  <a class="idref" href="mathcomp.ssreflect.path.html#path"><span class="id" title="definition">path</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#a3fa885266d530b93c1b9f67891df8e8"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#a3fa885266d530b93c1b9f67891df8e8"><span class="id" title="notation">rel</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#a3fa885266d530b93c1b9f67891df8e8"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#gTg"><span class="id" title="abbreviation">gTg</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#a3fa885266d530b93c1b9f67891df8e8"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#maxnormal"><span class="id" title="definition">maxnormal</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#a3fa885266d530b93c1b9f67891df8e8"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s"><span class="id" title="variable">s</span></a>)<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a class="idref" href="mathcomp.solvable.jordanholder.html#comps"><span class="id" title="definition">comps</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s"><span class="id" title="variable">s</span></a>).<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="trivg_comps"><span class="id" title="lemma">trivg_comps</span></a> <span class="id" title="var">G</span> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.solvable.jordanholder.html#comps"><span class="id" title="definition">comps</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.jordanholder.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#24f47bb7b1a372904563d2bdb8a213a4"><span class="id" title="notation">:==:</span></a> 1<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#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.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.jordanholder.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#747e2b5d553b2dfe76e024e1f8fb39d1"><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>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="comps_cons"><span class="id" title="lemma">comps_cons</span></a> <span class="id" title="var">G</span> <span class="id" title="var">H</span> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.solvable.jordanholder.html#comps"><span class="id" title="definition">comps</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#G"><span class="id" title="variable">G</span></a> (<a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s"><span class="id" title="variable">s</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.jordanholder.html#comps"><span class="id" title="definition">comps</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s"><span class="id" title="variable">s</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="simple_compsP"><span class="id" title="lemma">simple_compsP</span></a> <span class="id" title="var">G</span> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.solvable.jordanholder.html#comps"><span class="id" title="definition">comps</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="mathcomp.solvable.jordanholder.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">[::</span></a> 1%<span class="id" title="var">G</span><a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><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.jordanholder.html#G"><span class="id" title="variable">G</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="exists_comps"><span class="id" title="lemma">exists_comps</span></a> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.solvable.jordanholder.html#gTg"><span class="id" title="abbreviation">gTg</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">s</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#comps"><span class="id" title="definition">comps</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s"><span class="id" title="variable">s</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ The factors associated to two composition series of the same group are     
+ the same up to isomorphism and permutation                                  
+</div>
+<div class="code">
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="JordanHolderUniqueness"><span class="id" title="lemma">JordanHolderUniqueness</span></a> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.solvable.jordanholder.html#gTg"><span class="id" title="abbreviation">gTg</span></a>) (<span class="id" title="var">s1</span> <span class="id" title="var">s2</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#gTg"><span class="id" title="abbreviation">gTg</span></a>) :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.jordanholder.html#comps"><span class="id" title="definition">comps</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s1"><span class="id" title="variable">s1</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.jordanholder.html#comps"><span class="id" title="definition">comps</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s2"><span class="id" title="variable">s2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#perm_eq"><span class="id" title="definition">perm_eq</span></a> (<a class="idref" href="mathcomp.solvable.jordanholder.html#mkfactors"><span class="id" title="definition">mkfactors</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s1"><span class="id" title="variable">s1</span></a>) (<a class="idref" href="mathcomp.solvable.jordanholder.html#mkfactors"><span class="id" title="definition">mkfactors</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s2"><span class="id" title="variable">s2</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.jordanholder.html#CompositionSeries"><span class="id" title="section">CompositionSeries</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ Helper lemmas for group actions.                                            
+</div>
+<div class="code">
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="MoreGroupAction"><span class="id" title="section">MoreGroupAction</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variables</span> (<a name="MoreGroupAction.aT"><span class="id" title="variable">aT</span></a> <a name="MoreGroupAction.rT"><span class="id" title="variable">rT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>).<br/>
+<span class="id" title="keyword">Variables</span> (<a name="MoreGroupAction.A"><span class="id" title="variable">A</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<a name="MoreGroupAction.D"><span class="id" title="variable">D</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>).<br/>
+<span class="id" title="keyword">Variable</span> <a name="MoreGroupAction.to"><span class="id" title="variable">to</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#groupAction"><span class="id" title="record">groupAction</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.D"><span class="id" title="variable">D</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="gactsP"><span class="id" title="lemma">gactsP</span></a> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> <a class="idref" href="mathcomp.fingroup.action.html#05449e0e2f87f06fca16a62c49e8b809"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.action.html#05449e0e2f87f06fca16a62c49e8b809"><span class="id" title="notation">acts</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#05449e0e2f87f06fca16a62c49e8b809"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#05449e0e2f87f06fca16a62c49e8b809"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.action.html#05449e0e2f87f06fca16a62c49e8b809"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#05449e0e2f87f06fca16a62c49e8b809"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">acts</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="gactsM"><span class="id" title="lemma">gactsM</span></a> (<span class="id" title="var">N1</span> <span class="id" title="var">N2</span> : <a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a>) : <br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.jordanholder.html#N1"><span class="id" title="variable">N1</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.jordanholder.html#MoreGroupAction.D"><span class="id" title="variable">D</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.jordanholder.html#N2"><span class="id" title="variable">N2</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.jordanholder.html#MoreGroupAction.D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">acts</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#N1"><span class="id" title="variable">N1</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">acts</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#N2"><span class="id" title="variable">N2</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">acts</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#N1"><span class="id" title="variable">N1</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#N2"><span class="id" title="variable">N2</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="gactsI"><span class="id" title="lemma">gactsI</span></a> (<span class="id" title="var">N1</span> <span class="id" title="var">N2</span> : <a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a>) : <br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">acts</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#N1"><span class="id" title="variable">N1</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">acts</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#N2"><span class="id" title="variable">N2</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">acts</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#N1"><span class="id" title="variable">N1</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#cb41714a5a23482f7a48a98975fa8c59"><span class="id" title="notation">:&amp;:</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#N2"><span class="id" title="variable">N2</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="gastabsP"><span class="id" title="lemma">gastabsP</span></a> (<span class="id" title="var">S</span> : <a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">a</span> : <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.aT"><span class="id" title="variable">aT</span></a>) :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.jordanholder.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.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.jordanholder.html#MoreGroupAction.A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#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#reflect"><span class="id" title="abbreviation">reflect</span></a> (<span class="id" title="keyword">∀</span> <span class="id" title="var">x</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.jordanholder.html#MoreGroupAction.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.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.jordanholder.html#S"><span class="id" title="variable">S</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.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.jordanholder.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#S"><span class="id" title="variable">S</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.jordanholder.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.action.html#f49be8276ad4d3d8f37fd1509306940d"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#f49be8276ad4d3d8f37fd1509306940d"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.action.html#f49be8276ad4d3d8f37fd1509306940d"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.jordanholder.html#S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.action.html#f49be8276ad4d3d8f37fd1509306940d"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#f49be8276ad4d3d8f37fd1509306940d"><span class="id" title="notation">)</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction"><span class="id" title="section">MoreGroupAction</span></a>.<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ Helper lemmas for quotient actions.                                         
+</div>
+<div class="code">
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="MoreQuotientAction"><span class="id" title="section">MoreQuotientAction</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variables</span> (<a name="MoreQuotientAction.aT"><span class="id" title="variable">aT</span></a> <a name="MoreQuotientAction.rT"><span class="id" title="variable">rT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>).<br/>
+<span class="id" title="keyword">Variables</span> (<a name="MoreQuotientAction.A"><span class="id" title="variable">A</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>)(<a name="MoreQuotientAction.D"><span class="id" title="variable">D</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>).<br/>
+<span class="id" title="keyword">Variable</span> <a name="MoreQuotientAction.to"><span class="id" title="variable">to</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#groupAction"><span class="id" title="record">groupAction</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.D"><span class="id" title="variable">D</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="qact_dom_doms"><span class="id" title="lemma">qact_dom_doms</span></a> (<span class="id" title="var">H</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) : <a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.D"><span class="id" title="variable">D</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.action.html#qact_dom"><span class="id" title="definition">qact_dom</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.A"><span class="id" title="variable">A</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="acts_qact_doms"><span class="id" title="lemma">acts_qact_doms</span></a> (<span class="id" title="var">H</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.D"><span class="id" title="variable">D</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.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">acts</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#qact_dom"><span class="id" title="definition">qact_dom</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#67291ec55239f54fa5aa0b0bb974446c"><span class="id" title="notation">:=:</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.A"><span class="id" title="variable">A</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="qacts_cosetpre"><span class="id" title="lemma">qacts_cosetpre</span></a> (<span class="id" title="var">H</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">K'</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.quotient.html#coset_of"><span class="id" title="record">coset_of</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) :<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.D"><span class="id" title="variable">D</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.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">acts</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">acts</span></a> <a class="idref" href="mathcomp.fingroup.action.html#qact_dom"><span class="id" title="definition">qact_dom</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#K'"><span class="id" title="variable">K'</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.fingroup.action.html#2e4ccc4d97341df4136dd243a5fe1a5c"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">acts</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#coset"><span class="id" title="definition">coset</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#619a2190d60a66179f3396458e2a09ae"><span class="id" title="notation">@*^-1</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#K'"><span class="id" title="variable">K'</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="qacts_coset"><span class="id" title="lemma">qacts_coset</span></a> (<span class="id" title="var">H</span> <span class="id" title="var">K</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.solvable.jordanholder.html#MoreQuotientAction.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) : <br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.D"><span class="id" title="variable">D</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.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">acts</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">acts</span></a> <a class="idref" href="mathcomp.fingroup.action.html#qact_dom"><span class="id" title="definition">qact_dom</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.quotient.html#coset"><span class="id" title="definition">coset</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.fingroup.action.html#2e4ccc4d97341df4136dd243a5fe1a5c"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction"><span class="id" title="section">MoreQuotientAction</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="StableCompositionSeries"><span class="id" title="section">StableCompositionSeries</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variables</span> (<a name="StableCompositionSeries.aT"><span class="id" title="variable">aT</span></a> <a name="StableCompositionSeries.rT"><span class="id" title="variable">rT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>).<br/>
+<span class="id" title="keyword">Variables</span> (<a name="StableCompositionSeries.D"><span class="id" title="variable">D</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>)(<a name="StableCompositionSeries.A"><span class="id" title="variable">A</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>).<br/>
+<span class="id" title="keyword">Variable</span> <a name="StableCompositionSeries.to"><span class="id" title="variable">to</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#groupAction"><span class="id" title="record">groupAction</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.D"><span class="id" title="variable">D</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="maxainv"><span class="id" title="definition">maxainv</span></a> (<span class="id" title="var">B</span> <span class="id" title="var">C</span> : <a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a>) :=<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.fingroup.html#c203c753b6e0cf91b69de08395409b1a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#c203c753b6e0cf91b69de08395409b1a"><span class="id" title="notation">max</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#C"><span class="id" title="variable">C</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#c203c753b6e0cf91b69de08395409b1a"><span class="id" title="notation">of</span></a> <span class="id" title="var">H</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#c203c753b6e0cf91b69de08395409b1a"><span class="id" title="notation">|</span></a> <br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2e9317c5f71a1305fb695cdc49716482"><span class="id" title="notation">[&amp;&amp;</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2e9317c5f71a1305fb695cdc49716482"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#c27c638e534bbb5b7de2d4b4aa0a3e82"><span class="id" title="notation">&lt;|</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2e9317c5f71a1305fb695cdc49716482"><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="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.jordanholder.html#B"><span class="id" title="variable">B</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.jordanholder.html#H"><span class="id" title="variable">H</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="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2e9317c5f71a1305fb695cdc49716482"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">acts</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2e9317c5f71a1305fb695cdc49716482"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#c203c753b6e0cf91b69de08395409b1a"><span class="id" title="notation">]</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="StableCompositionSeries.MaxAinvProps"><span class="id" title="section">MaxAinvProps</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variables</span> <a name="StableCompositionSeries.MaxAinvProps.K"><span class="id" title="variable">K</span></a> <a name="StableCompositionSeries.MaxAinvProps.N"><span class="id" title="variable">N</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="maxainv_norm"><span class="id" title="lemma">maxainv_norm</span></a> : <a class="idref" href="mathcomp.solvable.jordanholder.html#maxainv"><span class="id" title="definition">maxainv</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.MaxAinvProps.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.MaxAinvProps.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.solvable.jordanholder.html#StableCompositionSeries.MaxAinvProps.N"><span class="id" title="variable">N</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#c27c638e534bbb5b7de2d4b4aa0a3e82"><span class="id" title="notation">&lt;|</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.MaxAinvProps.K"><span class="id" title="variable">K</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="maxainv_proper"><span class="id" title="lemma">maxainv_proper</span></a> : <a class="idref" href="mathcomp.solvable.jordanholder.html#maxainv"><span class="id" title="definition">maxainv</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.MaxAinvProps.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.MaxAinvProps.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.solvable.jordanholder.html#StableCompositionSeries.MaxAinvProps.N"><span class="id" title="variable">N</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#219b95257a323aaee1742e9bec4975d7"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#219b95257a323aaee1742e9bec4975d7"><span class="id" title="notation">proper</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.MaxAinvProps.K"><span class="id" title="variable">K</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="maxainv_sub"><span class="id" title="lemma">maxainv_sub</span></a> : <a class="idref" href="mathcomp.solvable.jordanholder.html#maxainv"><span class="id" title="definition">maxainv</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.MaxAinvProps.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.MaxAinvProps.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.solvable.jordanholder.html#StableCompositionSeries.MaxAinvProps.N"><span class="id" title="variable">N</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.jordanholder.html#StableCompositionSeries.MaxAinvProps.K"><span class="id" title="variable">K</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="maxainv_ainvar"><span class="id" title="lemma">maxainv_ainvar</span></a> : <a class="idref" href="mathcomp.solvable.jordanholder.html#maxainv"><span class="id" title="definition">maxainv</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.MaxAinvProps.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.MaxAinvProps.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.solvable.jordanholder.html#StableCompositionSeries.A"><span class="id" title="variable">A</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.action.html#f49be8276ad4d3d8f37fd1509306940d"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#f49be8276ad4d3d8f37fd1509306940d"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.action.html#f49be8276ad4d3d8f37fd1509306940d"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.MaxAinvProps.N"><span class="id" title="variable">N</span></a> <a class="idref" href="mathcomp.fingroup.action.html#f49be8276ad4d3d8f37fd1509306940d"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#f49be8276ad4d3d8f37fd1509306940d"><span class="id" title="notation">)</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="maxainvS"><span class="id" title="lemma">maxainvS</span></a> : <a class="idref" href="mathcomp.solvable.jordanholder.html#maxainv"><span class="id" title="definition">maxainv</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.MaxAinvProps.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.MaxAinvProps.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.solvable.jordanholder.html#StableCompositionSeries.MaxAinvProps.N"><span class="id" title="variable">N</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.jordanholder.html#StableCompositionSeries.MaxAinvProps.K"><span class="id" title="variable">K</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="maxainv_exists"><span class="id" title="lemma">maxainv_exists</span></a> : <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.MaxAinvProps.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#36625695d37b6869c156bfcdf13834f7"><span class="id" title="notation">:!=:</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><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.Specif.html#72ca3fac4636a1b19c963b12162882cf"><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.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#maxainv"><span class="id" title="definition">maxainv</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.MaxAinvProps.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#N"><span class="id" title="variable">N</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">}</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.MaxAinvProps"><span class="id" title="section">MaxAinvProps</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="maxainvM"><span class="id" title="lemma">maxainvM</span></a> (<span class="id" title="var">G</span> <span class="id" title="var">H</span> <span class="id" title="var">K</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.solvable.jordanholder.html#StableCompositionSeries.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) :<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.D"><span class="id" title="variable">D</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.jordanholder.html#K"><span class="id" title="variable">K</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.jordanholder.html#StableCompositionSeries.D"><span class="id" title="variable">D</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.jordanholder.html#maxainv"><span class="id" title="definition">maxainv</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</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.jordanholder.html#maxainv"><span class="id" title="definition">maxainv</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#3ead863f625b94b2207b999cfcc823ba"><span class="id" title="notation">:&lt;&gt;:</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#G"><span class="id" title="variable">G</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="asimple"><span class="id" title="definition">asimple</span></a> (<span class="id" title="var">K</span> : <a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a>) := <a class="idref" href="mathcomp.solvable.jordanholder.html#maxainv"><span class="id" title="definition">maxainv</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#K"><span class="id" title="variable">K</span></a> 1.<br/>
+
+<br/>
+<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">H</span> <span class="id" title="var">K</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.solvable.jordanholder.html#StableCompositionSeries.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">s</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="asimpleP"><span class="id" title="lemma">asimpleP</span></a> <span class="id" title="var">K</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4d70beb460e783df2b7b2ad387c00194"><span class="id" title="notation">[/\</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#36625695d37b6869c156bfcdf13834f7"><span class="id" title="notation">:!=:</span></a> 1<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4d70beb460e783df2b7b2ad387c00194"><span class="id" title="notation">&amp;</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">H</span>, <a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#c27c638e534bbb5b7de2d4b4aa0a3e82"><span class="id" title="notation">&lt;|</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">acts</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#67291ec55239f54fa5aa0b0bb974446c"><span class="id" title="notation">:=:</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#7a45dffb109c3069e5c675be68643e60"><span class="id" title="notation">∨</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#67291ec55239f54fa5aa0b0bb974446c"><span class="id" title="notation">:=:</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4d70beb460e783df2b7b2ad387c00194"><span class="id" title="notation">]</span></a><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a class="idref" href="mathcomp.solvable.jordanholder.html#asimple"><span class="id" title="definition">asimple</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#K"><span class="id" title="variable">K</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Definition</span> <a name="acomps"><span class="id" title="definition">acomps</span></a> <span class="id" title="var">K</span> <span class="id" title="var">s</span> :=<br/>
+&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#last"><span class="id" title="definition">last</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> 1%<span class="id" title="var">G</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">&amp;&amp;</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#path"><span class="id" title="definition">path</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#a3fa885266d530b93c1b9f67891df8e8"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#a3fa885266d530b93c1b9f67891df8e8"><span class="id" title="notation">rel</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#a3fa885266d530b93c1b9f67891df8e8"><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.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#a3fa885266d530b93c1b9f67891df8e8"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#maxainv"><span class="id" title="definition">maxainv</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#a3fa885266d530b93c1b9f67891df8e8"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s"><span class="id" title="variable">s</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="acompsP"><span class="id" title="lemma">acompsP</span></a> <span class="id" title="var">K</span> <span class="id" title="var">s</span> :<br/>
+&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#last"><span class="id" title="definition">last</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s"><span class="id" title="variable">s</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%<span class="id" title="var">G</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a>  <a class="idref" href="mathcomp.ssreflect.path.html#path"><span class="id" title="definition">path</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#a3fa885266d530b93c1b9f67891df8e8"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#a3fa885266d530b93c1b9f67891df8e8"><span class="id" title="notation">rel</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#a3fa885266d530b93c1b9f67891df8e8"><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.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#a3fa885266d530b93c1b9f67891df8e8"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#maxainv"><span class="id" title="definition">maxainv</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#a3fa885266d530b93c1b9f67891df8e8"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s"><span class="id" title="variable">s</span></a>)<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a class="idref" href="mathcomp.solvable.jordanholder.html#acomps"><span class="id" title="definition">acomps</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s"><span class="id" title="variable">s</span></a>).<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="trivg_acomps"><span class="id" title="lemma">trivg_acomps</span></a> <span class="id" title="var">K</span> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.solvable.jordanholder.html#acomps"><span class="id" title="definition">acomps</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.jordanholder.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#24f47bb7b1a372904563d2bdb8a213a4"><span class="id" title="notation">:==:</span></a> 1<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#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.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.jordanholder.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#747e2b5d553b2dfe76e024e1f8fb39d1"><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>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="acomps_cons"><span class="id" title="lemma">acomps_cons</span></a> <span class="id" title="var">K</span> <span class="id" title="var">H</span> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.solvable.jordanholder.html#acomps"><span class="id" title="definition">acomps</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#K"><span class="id" title="variable">K</span></a> (<a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s"><span class="id" title="variable">s</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.jordanholder.html#acomps"><span class="id" title="definition">acomps</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s"><span class="id" title="variable">s</span></a>.<br/>
+ 
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="asimple_acompsP"><span class="id" title="lemma">asimple_acompsP</span></a> <span class="id" title="var">K</span> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.solvable.jordanholder.html#acomps"><span class="id" title="definition">acomps</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="mathcomp.solvable.jordanholder.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">[::</span></a> 1%<span class="id" title="var">G</span><a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">]</span></a>) (<a class="idref" href="mathcomp.solvable.jordanholder.html#asimple"><span class="id" title="definition">asimple</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#K"><span class="id" title="variable">K</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="exists_acomps"><span class="id" title="lemma">exists_acomps</span></a> <span class="id" title="var">K</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">s</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#acomps"><span class="id" title="definition">acomps</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s"><span class="id" title="variable">s</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries"><span class="id" title="section">StableCompositionSeries</span></a>.<br/>
+
+<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="StrongJordanHolder"><span class="id" title="section">StrongJordanHolder</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Section</span> <a name="StrongJordanHolder.AuxiliaryLemmas"><span class="id" title="section">AuxiliaryLemmas</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variables</span> <a name="StrongJordanHolder.AuxiliaryLemmas.aT"><span class="id" title="variable">aT</span></a> <a name="StrongJordanHolder.AuxiliaryLemmas.rT"><span class="id" title="variable">rT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>.<br/>
+<span class="id" title="keyword">Variables</span> (<a name="StrongJordanHolder.AuxiliaryLemmas.A"><span class="id" title="variable">A</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.AuxiliaryLemmas.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<a name="StrongJordanHolder.AuxiliaryLemmas.D"><span class="id" title="variable">D</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.AuxiliaryLemmas.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<a name="StrongJordanHolder.AuxiliaryLemmas.to"><span class="id" title="variable">to</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#groupAction"><span class="id" title="record">groupAction</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#D"><span class="id" title="variable">D</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="maxainv_asimple_quo"><span class="id" title="lemma">maxainv_asimple_quo</span></a> (<span class="id" title="var">G</span> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.AuxiliaryLemmas.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) :<br/>
+&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.AuxiliaryLemmas.D"><span class="id" title="variable">D</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.jordanholder.html#maxainv"><span class="id" title="definition">maxainv</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.AuxiliaryLemmas.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</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.jordanholder.html#asimple"><span class="id" title="definition">asimple</span></a> (<a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.AuxiliaryLemmas.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.fingroup.action.html#2756d213ba2c3f60f8b9fc530f7c4cdc"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a>) (<a class="idref" href="mathcomp.solvable.jordanholder.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#c7768147d2d560601601fbf95706ddcc"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="asimple_quo_maxainv"><span class="id" title="lemma">asimple_quo_maxainv</span></a> (<span class="id" title="var">G</span> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.AuxiliaryLemmas.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) :<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.AuxiliaryLemmas.D"><span class="id" title="variable">D</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.jordanholder.html#G"><span class="id" title="variable">G</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.jordanholder.html#StrongJordanHolder.AuxiliaryLemmas.D"><span class="id" title="variable">D</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.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">acts</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.AuxiliaryLemmas.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.AuxiliaryLemmas.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">acts</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.AuxiliaryLemmas.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.AuxiliaryLemmas.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#c27c638e534bbb5b7de2d4b4aa0a3e82"><span class="id" title="notation">&lt;|</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#asimple"><span class="id" title="definition">asimple</span></a> (<a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.AuxiliaryLemmas.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.fingroup.action.html#2756d213ba2c3f60f8b9fc530f7c4cdc"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a>) (<a class="idref" href="mathcomp.solvable.jordanholder.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#c7768147d2d560601601fbf95706ddcc"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.jordanholder.html#maxainv"><span class="id" title="definition">maxainv</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.AuxiliaryLemmas.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="asimpleI"><span class="id" title="lemma">asimpleI</span></a> (<span class="id" title="var">N1</span> <span class="id" title="var">N2</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.solvable.jordanholder.html#StrongJordanHolder.AuxiliaryLemmas.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) : <br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.jordanholder.html#N2"><span class="id" title="variable">N2</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.jordanholder.html#N1"><span class="id" title="variable">N1</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#N1"><span class="id" title="variable">N1</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.jordanholder.html#StrongJordanHolder.AuxiliaryLemmas.D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">acts</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.AuxiliaryLemmas.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#N1"><span class="id" title="variable">N1</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.AuxiliaryLemmas.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">acts</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.AuxiliaryLemmas.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#N2"><span class="id" title="variable">N2</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.AuxiliaryLemmas.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.jordanholder.html#asimple"><span class="id" title="definition">asimple</span></a> (<a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.AuxiliaryLemmas.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.fingroup.action.html#2756d213ba2c3f60f8b9fc530f7c4cdc"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#N1"><span class="id" title="variable">N1</span></a>) (<a class="idref" href="mathcomp.solvable.jordanholder.html#N2"><span class="id" title="variable">N2</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#c7768147d2d560601601fbf95706ddcc"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#N1"><span class="id" title="variable">N1</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.jordanholder.html#asimple"><span class="id" title="definition">asimple</span></a> (<a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.AuxiliaryLemmas.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.fingroup.action.html#2756d213ba2c3f60f8b9fc530f7c4cdc"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.fingroup.action.html#2756d213ba2c3f60f8b9fc530f7c4cdc"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.jordanholder.html#N2"><span class="id" title="variable">N2</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#afecdac1581fada66d09c1ab40cfc23e"><span class="id" title="notation">:&amp;:</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#N1"><span class="id" title="variable">N1</span></a><a class="idref" href="mathcomp.fingroup.action.html#2756d213ba2c3f60f8b9fc530f7c4cdc"><span class="id" title="notation">)</span></a>) (<a class="idref" href="mathcomp.solvable.jordanholder.html#N2"><span class="id" title="variable">N2</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#c7768147d2d560601601fbf95706ddcc"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#c7768147d2d560601601fbf95706ddcc"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.jordanholder.html#N2"><span class="id" title="variable">N2</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#cb41714a5a23482f7a48a98975fa8c59"><span class="id" title="notation">:&amp;:</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#N1"><span class="id" title="variable">N1</span></a><a class="idref" href="mathcomp.fingroup.quotient.html#c7768147d2d560601601fbf95706ddcc"><span class="id" title="notation">)</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.AuxiliaryLemmas"><span class="id" title="section">AuxiliaryLemmas</span></a>.<br/>
+
+<br/>
+<span class="id" title="keyword">Variables</span> (<a name="StrongJordanHolder.aT"><span class="id" title="variable">aT</span></a> <a name="StrongJordanHolder.rT"><span class="id" title="variable">rT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>).<br/>
+<span class="id" title="keyword">Variables</span> (<a name="StrongJordanHolder.A"><span class="id" title="variable">A</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<a name="StrongJordanHolder.D"><span class="id" title="variable">D</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<a name="StrongJordanHolder.to"><span class="id" title="variable">to</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#groupAction"><span class="id" title="record">groupAction</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#D"><span class="id" title="variable">D</span></a>).<br/>
+
+<br/>
+</div>
+
+<div class="doc">
+ The factors associated to two A-stable composition series of the same      
+ group are the same up to isomorphism and permutation                        
+</div>
+<div class="code">
+
+<br/>
+<span class="id" title="keyword">Lemma</span> <a name="StrongJordanHolderUniqueness"><span class="id" title="lemma">StrongJordanHolderUniqueness</span></a> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">s1</span> <span class="id" title="var">s2</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) :<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.jordanholder.html#G"><span class="id" title="variable">G</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.jordanholder.html#StrongJordanHolder.D"><span class="id" title="variable">D</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.jordanholder.html#acomps"><span class="id" title="definition">acomps</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s1"><span class="id" title="variable">s1</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.jordanholder.html#acomps"><span class="id" title="definition">acomps</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s2"><span class="id" title="variable">s2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.seq.html#perm_eq"><span class="id" title="definition">perm_eq</span></a> (<a class="idref" href="mathcomp.solvable.jordanholder.html#mkfactors"><span class="id" title="definition">mkfactors</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s1"><span class="id" title="variable">s1</span></a>) (<a class="idref" href="mathcomp.solvable.jordanholder.html#mkfactors"><span class="id" title="definition">mkfactors</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s2"><span class="id" title="variable">s2</span></a>).<br/>
+
+<br/>
+<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder"><span class="id" title="section">StrongJordanHolder</span></a>.<br/>
+
+<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
author	Enrico Tassi	2018-04-20 10:54:22 +0200
committer	Enrico Tassi	2018-04-20 10:54:22 +0200
commit	ed05182cece6bb3706e09b2ce14af4a41a2e8141 (patch)
tree	e850d7314b6372d0476cf2ffaf7d3830721db7b1 /docs/htmldoc/mathcomp.solvable.jordanholder.html
parent	3d196f44681fb3b23ff8a79fbd44e12308680531 (diff)