diff options
Diffstat (limited to 'docs/htmldoc/mathcomp.solvable.jordanholder.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.solvable.jordanholder.html | 430 |
1 files changed, 0 insertions, 430 deletions
diff --git a/docs/htmldoc/mathcomp.solvable.jordanholder.html b/docs/htmldoc/mathcomp.solvable.jordanholder.html deleted file mode 100644 index a65d14f..0000000 --- a/docs/htmldoc/mathcomp.solvable.jordanholder.html +++ /dev/null @@ -1,430 +0,0 @@ -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" -"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> -<html xmlns="http://www.w3.org/1999/xhtml"> -<head> -<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> -<link href="coqdoc.css" rel="stylesheet" type="text/css" /> -<title>mathcomp.solvable.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">(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. <br/> - Distributed under the terms of CeCILL-B. *)</span><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><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#dd8cd2228f051940101d045bfdffe2d9"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) := <a 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/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><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/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><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/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Infix</span> <a name="72616f8bac9eaf4a536f6be688ba6b27"><span class="id" title="notation">"</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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e0817251e7d67ad994b4d9b1aa82a412"><span class="id" title="notation">.1</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#3e65ad3edf5f7fb3ea6bc63a878112a8"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#675082cc4d4538da052b547bdc6ea4c9"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#675082cc4d4538da052b547bdc6ea4c9"><span class="id" title="notation">.2</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">)}</span></a> :=<br/> - <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#f6996ff347e6cf832aa130837b06a848"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#f6996ff347e6cf832aa130837b06a848"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f6996ff347e6cf832aa130837b06a848"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#f6996ff347e6cf832aa130837b06a848"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#Sections.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">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#685b4c9ab7ccde70d9229dfbdb93d490"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#685b4c9ab7ccde70d9229dfbdb93d490"><span class="id" title="notation">newType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#685b4c9ab7ccde70d9229dfbdb93d490"><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#685b4c9ab7ccde70d9229dfbdb93d490"><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#b361a0fe0b43cea5c506ee5eccc55542"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#b361a0fe0b43cea5c506ee5eccc55542"><span class="id" title="notation">eqMixin</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b361a0fe0b43cea5c506ee5eccc55542"><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#b361a0fe0b43cea5c506ee5eccc55542"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b361a0fe0b43cea5c506ee5eccc55542"><span class="id" title="notation"><:]</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#035054ba987e1c05f2985518b41ec31f"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#035054ba987e1c05f2985518b41ec31f"><span class="id" title="notation">choiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#035054ba987e1c05f2985518b41ec31f"><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#035054ba987e1c05f2985518b41ec31f"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#035054ba987e1c05f2985518b41ec31f"><span class="id" title="notation"><:]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">section_choiceType</span> :=<br/> - <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#c2a823e7a76d1d303efdd00309d93aca"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#c2a823e7a76d1d303efdd00309d93aca"><span class="id" title="notation">countMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#c2a823e7a76d1d303efdd00309d93aca"><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#c2a823e7a76d1d303efdd00309d93aca"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#c2a823e7a76d1d303efdd00309d93aca"><span class="id" title="notation"><:]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">section_countType</span> :=<br/> - <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#9bbd910cbebcec91f8279b0711b4702d"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#9bbd910cbebcec91f8279b0711b4702d"><span class="id" title="notation">subCountType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#9bbd910cbebcec91f8279b0711b4702d"><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#9bbd910cbebcec91f8279b0711b4702d"><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#fede21e6a36088be0833d2600143b39c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#fede21e6a36088be0833d2600143b39c"><span class="id" title="notation">finMixin</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#fede21e6a36088be0833d2600143b39c"><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#fede21e6a36088be0833d2600143b39c"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#fede21e6a36088be0833d2600143b39c"><span class="id" title="notation"><:]</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#ea70e506e168d39ce0ec3d3ecd2c349f"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#ea70e506e168d39ce0ec3d3ecd2c349f"><span class="id" title="notation">subFinType</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#ea70e506e168d39ce0ec3d3ecd2c349f"><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#ea70e506e168d39ce0ec3d3ecd2c349f"><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="mathcomp.ssreflect.ssrbool.html#b10b133940ca4a77925bb31e7ba5d15e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#b10b133940ca4a77925bb31e7ba5d15e"><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="mathcomp.ssreflect.ssrbool.html#b10b133940ca4a77925bb31e7ba5d15e"><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="mathcomp.ssreflect.ssrbool.html#b10b133940ca4a77925bb31e7ba5d15e"><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#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#b10b133940ca4a77925bb31e7ba5d15e"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#odflt"><span class="id" title="abbreviation">odflt</span></a> (1 <a class="idref" href="mathcomp.solvable.jordanholder.html#72616f8bac9eaf4a536f6be688ba6b27"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#d89396f990d6b54d736cfe259e498cf4"><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#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.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/> - <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#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#s2"><span class="id" title="variable">s2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#Sections.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#Sections.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) :=<br/> - <a class="idref" href="mathcomp.ssreflect.seq.html#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/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><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#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> 1%<span class="id" title="var">G</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">&&</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#d20e6db07424254201d52f8314a47040"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.gseries.html#d20e6db07424254201d52f8314a47040"><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/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 1%<span class="id" title="var">G</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#ba2b0e492d2b4675a0acf3ea92aabadd"><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="mathcomp.ssreflect.ssrbool.html#b10b133940ca4a77925bb31e7ba5d15e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#b10b133940ca4a77925bb31e7ba5d15e"><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="mathcomp.ssreflect.ssrbool.html#b10b133940ca4a77925bb31e7ba5d15e"><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="mathcomp.ssreflect.ssrbool.html#b10b133940ca4a77925bb31e7ba5d15e"><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="mathcomp.ssreflect.ssrbool.html#b10b133940ca4a77925bb31e7ba5d15e"><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/> - (<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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#b91223a7636398c530555b2312d1e79b"><span class="id" title="notation">:==:</span></a> 1<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#0a934e621391740b862762275992e626"><span class="id" title="notation">[::]</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>.<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#407cde5b61fbf27196d1a7c5a475e083"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#506674b18256ef8f50efed43fa1dfd7d"><span class="id" title="notation">[::</span></a> 1%<span class="id" title="var">G</span><a class="idref" href="mathcomp.ssreflect.seq.html#506674b18256ef8f50efed43fa1dfd7d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <span class="id" title="var">s</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><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/> - <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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><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#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> <a class="idref" href="mathcomp.fingroup.action.html#5f6ba238defaa44d6a01a22efc00d730"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.action.html#5f6ba238defaa44d6a01a22efc00d730"><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#5f6ba238defaa44d6a01a22efc00d730"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#5f6ba238defaa44d6a01a22efc00d730"><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#5f6ba238defaa44d6a01a22efc00d730"><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#5f6ba238defaa44d6a01a22efc00d730"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><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#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>) : <br/> - <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#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#N2"><span class="id" title="variable">N2</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#8b8794efbfbae1b793d9cb62ce802285"><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#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><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#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>) : <br/> - <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#b9596739b058766532fc6517a36fef9f"><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#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><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#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><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/> - <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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreGroupAction.A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#S"><span class="id" title="variable">S</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#S"><span class="id" title="variable">S</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>) (<a class="idref" href="mathcomp.solvable.jordanholder.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.action.html#c0af106a0ada6310ccb2e8e8c7766282"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#c0af106a0ada6310ccb2e8e8c7766282"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.action.html#c0af106a0ada6310ccb2e8e8c7766282"><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#c0af106a0ada6310ccb2e8e8c7766282"><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#c0af106a0ada6310ccb2e8e8c7766282"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><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#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.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#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) :<br/> - <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#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.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#f0bbce9238fab3dd03626439080979a9"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">K'</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) :<br/> - <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#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><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#ad04e00ef26e546e5433da83c9f70dee"><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#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#320f70d30c9a649ec82642b364681418"><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#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) : <br/> - <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#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#MoreQuotientAction.D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><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#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><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#915e8fb7bcea89ddadab4deff6ea659e"><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#ad04e00ef26e546e5433da83c9f70dee"><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#915e8fb7bcea89ddadab4deff6ea659e"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><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#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>) :=<br/> - <a class="idref" href="mathcomp.fingroup.fingroup.html#9dc7aaba1a150ad5c926725e5128fb48"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#9dc7aaba1a150ad5c926725e5128fb48"><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#9dc7aaba1a150ad5c926725e5128fb48"><span class="id" title="notation">of</span></a> <span class="id" title="var">H</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#9dc7aaba1a150ad5c926725e5128fb48"><span class="id" title="notation">|</span></a> <br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5a7d806905be2a0d04047156433535f1"><span class="id" title="notation">[&&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5a7d806905be2a0d04047156433535f1"><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#7e8095b432e7aa5c3c22bb87584658b7"><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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5a7d806905be2a0d04047156433535f1"><span class="id" title="notation">),</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b3ebd0deddd84fd60e149cb5ef719351"><span class="id" title="notation">~~</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b3ebd0deddd84fd60e149cb5ef719351"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.jordanholder.html#B"><span class="id" title="variable">B</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b3ebd0deddd84fd60e149cb5ef719351"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5a7d806905be2a0d04047156433535f1"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5a7d806905be2a0d04047156433535f1"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#9dc7aaba1a150ad5c926725e5128fb48"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#7e8095b432e7aa5c3c22bb87584658b7"><span class="id" title="notation"><|</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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#f8a5284fd4c86e7670efa54241b49929"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f8a5284fd4c86e7670efa54241b49929"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.action.html#c0af106a0ada6310ccb2e8e8c7766282"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#c0af106a0ada6310ccb2e8e8c7766282"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.action.html#c0af106a0ada6310ccb2e8e8c7766282"><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#c0af106a0ada6310ccb2e8e8c7766282"><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#c0af106a0ada6310ccb2e8e8c7766282"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.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#be2f022a539ec6d4d51932b5ea998e57"><span class="id" title="notation">:!=:</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#6556914db359db999889decec6a4a562"><span class="id" title="notation">{</span></a><span class="id" title="var">N</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#6556914db359db999889decec6a4a562"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#6556914db359db999889decec6a4a562"><span class="id" title="notation">|</span></a> <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/V8.9.0/stdlib//Coq.Init.Specif.html#6556914db359db999889decec6a4a562"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) :<br/> - <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#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <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#c6306907993ec830e8152150c233ecd3"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#8b8794efbfbae1b793d9cb62ce802285"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StableCompositionSeries.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><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/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#53e4c1e546d9b20e029d981f761726c2"><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#be2f022a539ec6d4d51932b5ea998e57"><span class="id" title="notation">:!=:</span></a> 1<br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#53e4c1e546d9b20e029d981f761726c2"><span class="id" title="notation">&</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#7e8095b432e7aa5c3c22bb87584658b7"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#f0bbce9238fab3dd03626439080979a9"><span class="id" title="notation">:=:</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#f031fe1957c4a4a8e217aa46af2b4e25"><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#f0bbce9238fab3dd03626439080979a9"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#53e4c1e546d9b20e029d981f761726c2"><span class="id" title="notation">]</span></a><br/> - (<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/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><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#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> 1%<span class="id" title="var">G</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><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="mathcomp.ssreflect.ssrbool.html#b10b133940ca4a77925bb31e7ba5d15e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#b10b133940ca4a77925bb31e7ba5d15e"><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="mathcomp.ssreflect.ssrbool.html#b10b133940ca4a77925bb31e7ba5d15e"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#b10b133940ca4a77925bb31e7ba5d15e"><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="mathcomp.ssreflect.ssrbool.html#b10b133940ca4a77925bb31e7ba5d15e"><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/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 1%<span class="id" title="var">G</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#ba2b0e492d2b4675a0acf3ea92aabadd"><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="mathcomp.ssreflect.ssrbool.html#b10b133940ca4a77925bb31e7ba5d15e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#b10b133940ca4a77925bb31e7ba5d15e"><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="mathcomp.ssreflect.ssrbool.html#b10b133940ca4a77925bb31e7ba5d15e"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#b10b133940ca4a77925bb31e7ba5d15e"><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="mathcomp.ssreflect.ssrbool.html#b10b133940ca4a77925bb31e7ba5d15e"><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/> - (<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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#b91223a7636398c530555b2312d1e79b"><span class="id" title="notation">:==:</span></a> 1<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#0a934e621391740b862762275992e626"><span class="id" title="notation">[::]</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>.<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#407cde5b61fbf27196d1a7c5a475e083"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#506674b18256ef8f50efed43fa1dfd7d"><span class="id" title="notation">[::</span></a> 1%<span class="id" title="var">G</span><a class="idref" href="mathcomp.ssreflect.seq.html#506674b18256ef8f50efed43fa1dfd7d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <span class="id" title="var">s</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.AuxiliaryLemmas.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.AuxiliaryLemmas.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.AuxiliaryLemmas.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) :<br/> - <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#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.AuxiliaryLemmas.D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#41672295fce40becd46688b39618a9e3"><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#3e65ad3edf5f7fb3ea6bc63a878112a8"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.AuxiliaryLemmas.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) :<br/> - <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#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.AuxiliaryLemmas.D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.AuxiliaryLemmas.D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.solvable.jordanholder.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7e8095b432e7aa5c3c22bb87584658b7"><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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.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#41672295fce40becd46688b39618a9e3"><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#3e65ad3edf5f7fb3ea6bc63a878112a8"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.AuxiliaryLemmas.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) : <br/> - <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#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.jordanholder.html#N1"><span class="id" title="variable">N1</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#N1"><span class="id" title="variable">N1</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.AuxiliaryLemmas.D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><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#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <br/> - <a class="idref" href="mathcomp.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#41672295fce40becd46688b39618a9e3"><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#3e65ad3edf5f7fb3ea6bc63a878112a8"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <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#41672295fce40becd46688b39618a9e3"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.fingroup.action.html#41672295fce40becd46688b39618a9e3"><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#83bfb527fd8c6ef7c38a16fb45f9e361"><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.action.html#41672295fce40becd46688b39618a9e3"><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#3e65ad3edf5f7fb3ea6bc63a878112a8"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#3e65ad3edf5f7fb3ea6bc63a878112a8"><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#b9596739b058766532fc6517a36fef9f"><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.quotient.html#3e65ad3edf5f7fb3ea6bc63a878112a8"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) :<br/> - <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#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.jordanholder.html#StrongJordanHolder.D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <br/> - <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 |