diff options
| author | Cyril Cohen | 2019-10-16 11:26:43 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2019-10-16 11:26:43 +0200 |
| commit | 6b59540a2460633df4e3d8347cb4dfe2fb3a3afb (patch) | |
| tree | 1239c1d5553d51a7d73f2f8b465f6a23178ff8a0 /docs/htmldoc/mathcomp.solvable.gseries.html | |
| parent | dd82aaeae7e9478efc178ce8430986649555b032 (diff) | |
removing everything but index which redirects to the new page
Diffstat (limited to 'docs/htmldoc/mathcomp.solvable.gseries.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.solvable.gseries.html | 424 |
1 files changed, 0 insertions, 424 deletions
diff --git a/docs/htmldoc/mathcomp.solvable.gseries.html b/docs/htmldoc/mathcomp.solvable.gseries.html deleted file mode 100644 index d503193..0000000 --- a/docs/htmldoc/mathcomp.solvable.gseries.html +++ /dev/null @@ -1,424 +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.gseries</title> -</head> - -<body> - -<div id="page"> - -<div id="header"> -</div> - -<div id="main"> - -<h1 class="libtitle">Library mathcomp.solvable.gseries</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"> - H <|<| G <=> H is subnormal in G, i.e., H <| ... <| G. - invariant_factor A H G <=> A normalises both H and G, and H <| G. - A.-invariant <=> the (invariant_factor A) relation, in the context - of the g_rel.-series notation. - g_rel.-series H s <=> H :: s is a sequence of groups whose projection - to sets satisfies relation g_rel pairwise; for - example H <|<| G iff G = last H s for some s such - that normal.-series H s. - stable_factor A H G == H <| G and A centralises G / H. - A.-stable == the stable_factor relation, in the scope of the - r.-series notation. - G.-central == the central_factor relation, in the scope of the - r.-series notation. - maximal M G == M is a maximal proper subgroup of G. - maximal_eq M G == (M == G) or (maximal M G). - maxnormal M G N == M is a maximal subgroup of G normalized by N. - minnormal M N == M is a minimal nontrivial group normalized by N. - simple G == G is a (nontrivial) simple group. - := minnormal G G - G.-chief == the chief_factor relation, in the scope of the - r.-series notation. -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Set Implicit Arguments</span>.<br/> - -<br/> -<span class="id" title="keyword">Import</span> <span class="id" title="var">GroupScope</span>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="GroupDefs"><span class="id" title="section">GroupDefs</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="GroupDefs.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">A</span> <span class="id" title="var">B</span> <span class="id" title="var">U</span> <span class="id" title="var">V</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.gseries.html#GroupDefs.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>.<br/> - -<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="subnormal"><span class="id" title="definition">subnormal</span></a> <span class="id" title="var">A</span> <span class="id" title="var">B</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.solvable.gseries.html#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.solvable.gseries.html#B"><span class="id" title="variable">B</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="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.ssrnat.html#iter"><span class="id" title="definition">iter</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.gseries.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">N</span> ⇒ <a class="idref" href="mathcomp.fingroup.fingroup.html#generated"><span class="id" title="definition">generated</span></a> (<a class="idref" href="mathcomp.fingroup.fingroup.html#class_support"><span class="id" title="definition">class_support</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#N"><span class="id" title="variable">N</span></a>)) <a class="idref" href="mathcomp.solvable.gseries.html#B"><span class="id" title="variable">B</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#A"><span class="id" title="variable">A</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>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="invariant_factor"><span class="id" title="definition">invariant_factor</span></a> <span class="id" title="var">A</span> <span class="id" title="var">B</span> <span class="id" title="var">C</span> :=<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="mathcomp.solvable.gseries.html#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.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.gseries.html#B"><span class="id" title="variable">B</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.ssr.ssrbool.html#5a7d806905be2a0d04047156433535f1"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#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.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.gseries.html#C"><span class="id" title="variable">C</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.ssr.ssrbool.html#5a7d806905be2a0d04047156433535f1"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#B"><span class="id" title="variable">B</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7e8095b432e7aa5c3c22bb87584658b7"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#C"><span class="id" title="variable">C</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>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="group_rel_of"><span class="id" title="definition">group_rel_of</span></a> (<span class="id" title="var">r</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#GroupDefs.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><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.ssreflect.ssrbool.html#b10b133940ca4a77925bb31e7ba5d15e"><span class="id" title="notation">rel</span></a> <span class="id" title="var">H</span> <span class="id" title="var">G</span> <a class="idref" href="mathcomp.ssreflect.ssrbool.html#b10b133940ca4a77925bb31e7ba5d15e"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#groupT"><span class="id" title="abbreviation">groupT</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#r"><span class="id" title="variable">r</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#b10b133940ca4a77925bb31e7ba5d15e"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="stable_factor"><span class="id" title="definition">stable_factor</span></a> <span class="id" title="var">A</span> <span class="id" title="var">V</span> <span class="id" title="var">U</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.fingroup.fingroup.html#653e048e978e57b1e513b9d5de2caee6"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#U"><span class="id" title="variable">U</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#653e048e978e57b1e513b9d5de2caee6"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#653e048e978e57b1e513b9d5de2caee6"><span class="id" title="notation">]</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.gseries.html#V"><span class="id" title="variable">V</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="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.gseries.html#V"><span class="id" title="variable">V</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7e8095b432e7aa5c3c22bb87584658b7"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#U"><span class="id" title="variable">U</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>. <span class="comment">(* this orders allows and3P to be used *)</span><br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="central_factor"><span class="id" title="definition">central_factor</span></a> <span class="id" title="var">A</span> <span class="id" title="var">V</span> <span class="id" title="var">U</span> :=<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="mathcomp.fingroup.fingroup.html#653e048e978e57b1e513b9d5de2caee6"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#U"><span class="id" title="variable">U</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#653e048e978e57b1e513b9d5de2caee6"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#653e048e978e57b1e513b9d5de2caee6"><span class="id" title="notation">]</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.gseries.html#V"><span class="id" title="variable">V</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.gseries.html#V"><span class="id" title="variable">V</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.gseries.html#U"><span class="id" title="variable">U</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5a7d806905be2a0d04047156433535f1"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#U"><span class="id" title="variable">U</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.gseries.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#5a7d806905be2a0d04047156433535f1"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="maximal"><span class="id" title="definition">maximal</span></a> <span class="id" title="var">A</span> <span class="id" title="var">B</span> := <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.gseries.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#9dc7aaba1a150ad5c926725e5128fb48"><span class="id" title="notation">of</span></a> <span class="id" title="var">G</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#9dc7aaba1a150ad5c926725e5128fb48"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#G"><span class="id" title="variable">G</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.gseries.html#B"><span class="id" title="variable">B</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">Definition</span> <a name="maximal_eq"><span class="id" title="definition">maximal_eq</span></a> <span class="id" title="var">A</span> <span class="id" title="var">B</span> := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#081ff67d3116402bb680e8692aa39185"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.gseries.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#081ff67d3116402bb680e8692aa39185"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#081ff67d3116402bb680e8692aa39185"><span class="id" title="notation">||</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#maximal"><span class="id" title="definition">maximal</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#B"><span class="id" title="variable">B</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="maxnormal"><span class="id" title="definition">maxnormal</span></a> <span class="id" title="var">A</span> <span class="id" title="var">B</span> <span class="id" title="var">U</span> := <a class="idref" href="mathcomp.fingroup.fingroup.html#b3db3343365cce619068dbaf58ef6c99"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#b3db3343365cce619068dbaf58ef6c99"><span class="id" title="notation">max</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#b3db3343365cce619068dbaf58ef6c99"><span class="id" title="notation">of</span></a> <span class="id" title="var">G</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#b3db3343365cce619068dbaf58ef6c99"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#G"><span class="id" title="variable">G</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.gseries.html#B"><span class="id" title="variable">B</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#b3db3343365cce619068dbaf58ef6c99"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#U"><span class="id" title="variable">U</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.gseries.html#G"><span class="id" title="variable">G</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#b3db3343365cce619068dbaf58ef6c99"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="minnormal"><span class="id" title="definition">minnormal</span></a> <span class="id" title="var">A</span> <span class="id" title="var">B</span> := <a class="idref" href="mathcomp.fingroup.fingroup.html#83949b4ab4a5556fc861a975723584d5"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#83949b4ab4a5556fc861a975723584d5"><span class="id" title="notation">min</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#83949b4ab4a5556fc861a975723584d5"><span class="id" title="notation">of</span></a> <span class="id" title="var">G</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#83949b4ab4a5556fc861a975723584d5"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#be2f022a539ec6d4d51932b5ea998e57"><span class="id" title="notation">:!=:</span></a> 1 <a class="idref" href="mathcomp.fingroup.fingroup.html#83949b4ab4a5556fc861a975723584d5"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.gseries.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.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.gseries.html#G"><span class="id" title="variable">G</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#83949b4ab4a5556fc861a975723584d5"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="simple"><span class="id" title="definition">simple</span></a> <span class="id" title="var">A</span> := <a class="idref" href="mathcomp.solvable.gseries.html#minnormal"><span class="id" title="definition">minnormal</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#A"><span class="id" title="variable">A</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="chief_factor"><span class="id" title="definition">chief_factor</span></a> <span class="id" title="var">A</span> <span class="id" title="var">V</span> <span class="id" title="var">U</span> := <a class="idref" href="mathcomp.solvable.gseries.html#maxnormal"><span class="id" title="definition">maxnormal</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#V"><span class="id" title="variable">V</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#U"><span class="id" title="variable">U</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#A"><span class="id" title="variable">A</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="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.gseries.html#U"><span class="id" title="variable">U</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7e8095b432e7aa5c3c22bb87584658b7"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#A"><span class="id" title="variable">A</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>.<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gseries.html#GroupDefs"><span class="id" title="section">GroupDefs</span></a>.<br/> - -<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="52cdd2d549fa2e18a6c3687e75ce9c7c"><span class="id" title="notation">"</span></a>H <|<| G" := (<a class="idref" href="mathcomp.solvable.gseries.html#subnormal"><span class="id" title="definition">subnormal</span></a> <span class="id" title="var">H</span> <span class="id" title="var">G</span>)<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 70, <span class="id" title="keyword">no</span> <span class="id" title="keyword">associativity</span>) : <span class="id" title="var">group_scope</span>.<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="19a37940bf6d09f0d893364b76284331"><span class="id" title="notation">"</span></a>A .-invariant" := (<a class="idref" href="mathcomp.solvable.gseries.html#invariant_factor"><span class="id" title="definition">invariant_factor</span></a> <span class="id" title="var">A</span>)<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">format</span> "A .-invariant") : <span class="id" title="var">group_rel_scope</span>.<br/> -<span class="id" title="keyword">Notation</span> <a name="1733041c7cb576a0063469f41c7ade46"><span class="id" title="notation">"</span></a>A .-stable" := (<a class="idref" href="mathcomp.solvable.gseries.html#stable_factor"><span class="id" title="definition">stable_factor</span></a> <span class="id" title="var">A</span>)<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">format</span> "A .-stable") : <span class="id" title="var">group_rel_scope</span>.<br/> -<span class="id" title="keyword">Notation</span> <a name="cc81b5d388c2f555c988b815d6ad5f42"><span class="id" title="notation">"</span></a>A .-central" := (<a class="idref" href="mathcomp.solvable.gseries.html#central_factor"><span class="id" title="definition">central_factor</span></a> <span class="id" title="var">A</span>)<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">format</span> "A .-central") : <span class="id" title="var">group_rel_scope</span>.<br/> -<span class="id" title="keyword">Notation</span> <a name="466a2c8e043fca24105330dda0c4acf7"><span class="id" title="notation">"</span></a>G .-chief" := (<a class="idref" href="mathcomp.solvable.gseries.html#chief_factor"><span class="id" title="definition">chief_factor</span></a> <span class="id" title="var">G</span>)<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">format</span> "G .-chief") : <span class="id" title="var">group_rel_scope</span>.<br/> - -<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="d20e6db07424254201d52f8314a47040"><span class="id" title="notation">"</span></a>r .-series" := (<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#rel_of_simpl_rel"><span class="id" title="definition">rel_of_simpl_rel</span></a> (<a class="idref" href="mathcomp.solvable.gseries.html#group_rel_of"><span class="id" title="definition">group_rel_of</span></a> <span class="id" title="var">r</span>)))<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">format</span> "r .-series") : <span class="id" title="var">group_scope</span>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="Subnormal"><span class="id" title="section">Subnormal</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="Subnormal.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">A</span> <span class="id" title="var">B</span> <span class="id" title="var">C</span> <span class="id" title="var">D</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.gseries.html#Subnormal.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</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.gseries.html#Subnormal.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">Let</span> <a name="Subnormal.setIgr"><span class="id" title="variable">setIgr</span></a> <span class="id" title="var">H</span> <span class="id" title="var">G</span> := (<a class="idref" href="mathcomp.solvable.gseries.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#83bfb527fd8c6ef7c38a16fb45f9e361"><span class="id" title="notation">:&:</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#H"><span class="id" title="variable">H</span></a>)%<span class="id" title="var">G</span>.<br/> -<span class="id" title="keyword">Let</span> <a name="Subnormal.sub_setIgr"><span class="id" title="variable">sub_setIgr</span></a> <span class="id" title="var">G</span> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.solvable.gseries.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.gseries.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.gseries.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#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#Subnormal.setIgr"><span class="id" title="variable">setIgr</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Let</span> <a name="Subnormal.path_setIgr"><span class="id" title="variable">path_setIgr</span></a> <span class="id" title="var">H</span> <span class="id" title="var">G</span> <span class="id" title="var">s</span> :<br/> - <a class="idref" href="mathcomp.fingroup.fingroup.html#normal"><span class="id" title="definition">normal</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.gseries.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.gseries.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.fingroup.fingroup.html#normal"><span class="id" title="definition">normal</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.gseries.html#Subnormal.setIgr"><span class="id" title="variable">setIgr</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#H"><span class="id" title="variable">H</span></a>) (<a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> (<a class="idref" href="mathcomp.solvable.gseries.html#Subnormal.setIgr"><span class="id" title="variable">setIgr</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#G"><span class="id" title="variable">G</span></a>) <a class="idref" href="mathcomp.solvable.gseries.html#s"><span class="id" title="variable">s</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="subnormalP"><span class="id" title="lemma">subnormalP</span></a> <span class="id" title="var">H</span> <span class="id" title="var">G</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.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">exists2</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#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#normal"><span class="id" title="definition">normal</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.gseries.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.gseries.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#3df228c109f14f0423b4fccc967ee1ac"><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.gseries.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.gseries.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.gseries.html#G"><span class="id" title="variable">G</span></a>) (<a class="idref" href="mathcomp.solvable.gseries.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#52cdd2d549fa2e18a6c3687e75ce9c7c"><span class="id" title="notation"><|<|</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#G"><span class="id" title="variable">G</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="subnormal_refl"><span class="id" title="lemma">subnormal_refl</span></a> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.solvable.gseries.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#52cdd2d549fa2e18a6c3687e75ce9c7c"><span class="id" title="notation"><|<|</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="subnormal_trans"><span class="id" title="lemma">subnormal_trans</span></a> <span class="id" title="var">K</span> <span class="id" title="var">H</span> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.solvable.gseries.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#52cdd2d549fa2e18a6c3687e75ce9c7c"><span class="id" title="notation"><|<|</span></a> <a class="idref" href="mathcomp.solvable.gseries.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.gseries.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#52cdd2d549fa2e18a6c3687e75ce9c7c"><span class="id" title="notation"><|<|</span></a> <a class="idref" href="mathcomp.solvable.gseries.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.gseries.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#52cdd2d549fa2e18a6c3687e75ce9c7c"><span class="id" title="notation"><|<|</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="normal_subnormal"><span class="id" title="lemma">normal_subnormal</span></a> <span class="id" title="var">H</span> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.solvable.gseries.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.gseries.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.gseries.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#52cdd2d549fa2e18a6c3687e75ce9c7c"><span class="id" title="notation"><|<|</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="setI_subnormal"><span class="id" title="lemma">setI_subnormal</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.solvable.gseries.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.gseries.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.gseries.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#52cdd2d549fa2e18a6c3687e75ce9c7c"><span class="id" title="notation"><|<|</span></a> <a class="idref" href="mathcomp.solvable.gseries.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.gseries.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#b9596739b058766532fc6517a36fef9f"><span class="id" title="notation">:&:</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#52cdd2d549fa2e18a6c3687e75ce9c7c"><span class="id" title="notation"><|<|</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#K"><span class="id" title="variable">K</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="subnormal_sub"><span class="id" title="lemma">subnormal_sub</span></a> <span class="id" title="var">G</span> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.solvable.gseries.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#52cdd2d549fa2e18a6c3687e75ce9c7c"><span class="id" title="notation"><|<|</span></a> <a class="idref" href="mathcomp.solvable.gseries.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.gseries.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.gseries.html#G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="invariant_subnormal"><span class="id" title="lemma">invariant_subnormal</span></a> <span class="id" title="var">A</span> <span class="id" title="var">G</span> <span class="id" title="var">H</span> :<br/> - <a class="idref" href="mathcomp.solvable.gseries.html#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.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.gseries.html#G"><span class="id" title="variable">G</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.gseries.html#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.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.gseries.html#H"><span class="id" title="variable">H</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.gseries.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#52cdd2d549fa2e18a6c3687e75ce9c7c"><span class="id" title="notation"><|<|</span></a> <a class="idref" href="mathcomp.solvable.gseries.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><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">exists2</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#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">,</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#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.solvable.gseries.html#19a37940bf6d09f0d893364b76284331"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.gseries.html#19a37940bf6d09f0d893364b76284331"><span class="id" title="notation">invariant</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.gseries.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.gseries.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#3df228c109f14f0423b4fccc967ee1ac"><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.gseries.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.gseries.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.gseries.html#G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="subnormalEsupport"><span class="id" title="lemma">subnormalEsupport</span></a> <span class="id" title="var">G</span> <span class="id" title="var">H</span> :<br/> - <a class="idref" href="mathcomp.solvable.gseries.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#52cdd2d549fa2e18a6c3687e75ce9c7c"><span class="id" title="notation"><|<|</span></a> <a class="idref" href="mathcomp.solvable.gseries.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.gseries.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.gseries.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#f031fe1957c4a4a8e217aa46af2b4e25"><span class="id" title="notation">∨</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7fae3285ae0b14be2ed14c5a340c6d3d"><span class="id" title="notation"><<</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#class_support"><span class="id" title="definition">class_support</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#7fae3285ae0b14be2ed14c5a340c6d3d"><span class="id" title="notation">>></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.gseries.html#G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="subnormalEr"><span class="id" title="lemma">subnormalEr</span></a> <span class="id" title="var">G</span> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.solvable.gseries.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#52cdd2d549fa2e18a6c3687e75ce9c7c"><span class="id" title="notation"><|<|</span></a> <a class="idref" href="mathcomp.solvable.gseries.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> <br/> - <a class="idref" href="mathcomp.solvable.gseries.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.gseries.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#f031fe1957c4a4a8e217aa46af2b4e25"><span class="id" title="notation">∨</span></a> <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="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">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.gseries.html#Subnormal.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.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">[/\</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#52cdd2d549fa2e18a6c3687e75ce9c7c"><span class="id" title="notation"><|<|</span></a> <a class="idref" href="mathcomp.solvable.gseries.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#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7e8095b432e7aa5c3c22bb87584658b7"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#K"><span class="id" title="variable">K</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.gseries.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">]</span></a><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>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="subnormalEl"><span class="id" title="lemma">subnormalEl</span></a> <span class="id" title="var">G</span> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.solvable.gseries.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#52cdd2d549fa2e18a6c3687e75ce9c7c"><span class="id" title="notation"><|<|</span></a> <a class="idref" href="mathcomp.solvable.gseries.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><br/> - <a class="idref" href="mathcomp.solvable.gseries.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.gseries.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#f031fe1957c4a4a8e217aa46af2b4e25"><span class="id" title="notation">∨</span></a> <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="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">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.gseries.html#Subnormal.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.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">[/\</span></a> <a class="idref" href="mathcomp.solvable.gseries.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.gseries.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#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#52cdd2d549fa2e18a6c3687e75ce9c7c"><span class="id" title="notation"><|<|</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#H"><span class="id" title="variable">H</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.gseries.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#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">]</span></a><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>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gseries.html#Subnormal"><span class="id" title="section">Subnormal</span></a>.<br/> - -<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="MorphSubNormal"><span class="id" title="section">MorphSubNormal</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="MorphSubNormal.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">Type</span> <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.gseries.html#MorphSubNormal.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">Lemma</span> <a name="morphim_subnormal"><span class="id" title="lemma">morphim_subnormal</span></a> (<span class="id" title="var">rT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) <span class="id" title="var">G</span> (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.solvable.gseries.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">}</span></a>) <span class="id" title="var">H</span> <span class="id" title="var">K</span> :<br/> - <a class="idref" href="mathcomp.solvable.gseries.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#52cdd2d549fa2e18a6c3687e75ce9c7c"><span class="id" title="notation"><|<|</span></a> <a class="idref" href="mathcomp.solvable.gseries.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.gseries.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#52cdd2d549fa2e18a6c3687e75ce9c7c"><span class="id" title="notation"><|<|</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#K"><span class="id" title="variable">K</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="quotient_subnormal"><span class="id" title="lemma">quotient_subnormal</span></a> <span class="id" title="var">H</span> <span class="id" title="var">G</span> <span class="id" title="var">K</span> : <a class="idref" href="mathcomp.solvable.gseries.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#52cdd2d549fa2e18a6c3687e75ce9c7c"><span class="id" title="notation"><|<|</span></a> <a class="idref" href="mathcomp.solvable.gseries.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.gseries.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.gseries.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#52cdd2d549fa2e18a6c3687e75ce9c7c"><span class="id" title="notation"><|<|</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#3e65ad3edf5f7fb3ea6bc63a878112a8"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#H"><span class="id" title="variable">H</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gseries.html#MorphSubNormal"><span class="id" title="section">MorphSubNormal</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="MaxProps"><span class="id" title="section">MaxProps</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="MaxProps.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> <span class="id" title="var">H</span> <span class="id" title="var">M</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.gseries.html#MaxProps.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">Lemma</span> <a name="maximal_eqP"><span class="id" title="lemma">maximal_eqP</span></a> <span class="id" title="var">M</span> <span class="id" title="var">G</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.solvable.gseries.html#M"><span class="id" title="variable">M</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.gseries.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#ba2b0e492d2b4675a0acf3ea92aabadd"><span class="id" title="notation">∧</span></a><br/> - <span class="id" title="keyword">∀</span> <span class="id" title="var">H</span>, <a class="idref" href="mathcomp.solvable.gseries.html#M"><span class="id" title="variable">M</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.gseries.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.gseries.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.gseries.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.gseries.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.gseries.html#M"><span class="id" title="variable">M</span></a> <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.gseries.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.gseries.html#G"><span class="id" title="variable">G</span></a>)<br/> - (<a class="idref" href="mathcomp.solvable.gseries.html#maximal_eq"><span class="id" title="definition">maximal_eq</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#G"><span class="id" title="variable">G</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="maximal_exists"><span class="id" title="lemma">maximal_exists</span></a> <span class="id" title="var">H</span> <span class="id" title="var">G</span> :<br/> - <a class="idref" href="mathcomp.solvable.gseries.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.gseries.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><br/> - <a class="idref" href="mathcomp.solvable.gseries.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.gseries.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#f031fe1957c4a4a8e217aa46af2b4e25"><span class="id" title="notation">∨</span></a> <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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#59ba2b47d2814e66f8210a649ae6e6bc"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">M</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#59ba2b47d2814e66f8210a649ae6e6bc"><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.gseries.html#MaxProps.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.Logic.html#59ba2b47d2814e66f8210a649ae6e6bc"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#maximal"><span class="id" title="definition">maximal</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.solvable.gseries.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#59ba2b47d2814e66f8210a649ae6e6bc"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.gseries.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.gseries.html#M"><span class="id" title="variable">M</span></a><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>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="mulg_normal_maximal"><span class="id" title="lemma">mulg_normal_maximal</span></a> <span class="id" title="var">G</span> <span class="id" title="var">M</span> <span class="id" title="var">H</span> :<br/> - <a class="idref" href="mathcomp.solvable.gseries.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7e8095b432e7aa5c3c22bb87584658b7"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.solvable.gseries.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.gseries.html#maximal"><span class="id" title="definition">maximal</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.solvable.gseries.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.gseries.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.gseries.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="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.gseries.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.gseries.html#M"><span class="id" title="variable">M</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.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> (<a class="idref" href="mathcomp.solvable.gseries.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#8b8794efbfbae1b793d9cb62ce802285"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.solvable.gseries.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#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#G"><span class="id" title="variable">G</span></a>)%<span class="id" title="var">g</span>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gseries.html#MaxProps"><span class="id" title="section">MaxProps</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="MinProps"><span class="id" title="section">MinProps</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="MinProps.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> <span class="id" title="var">H</span> <span class="id" title="var">M</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.gseries.html#MinProps.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">Lemma</span> <a name="minnormal_exists"><span class="id" title="lemma">minnormal_exists</span></a> <span class="id" title="var">G</span> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.solvable.gseries.html#H"><span class="id" title="variable">H</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="mathcomp.solvable.gseries.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.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.gseries.html#H"><span class="id" title="variable">H</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><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">{</span></a><span class="id" title="var">M</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><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.gseries.html#MinProps.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.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#minnormal"><span class="id" title="definition">minnormal</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.solvable.gseries.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.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#M"><span class="id" title="variable">M</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.gseries.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.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gseries.html#MinProps"><span class="id" title="section">MinProps</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="MorphPreMax"><span class="id" title="section">MorphPreMax</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="MorphPreMax.gT"><span class="id" title="variable">gT</span></a> <a name="MorphPreMax.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>) (<a name="MorphPreMax.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.gseries.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 name="MorphPreMax.f"><span class="id" title="variable">f</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.solvable.gseries.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">}</span></a>).<br/> -<span class="id" title="keyword">Variables</span> (<a name="MorphPreMax.M"><span class="id" title="variable">M</span></a> <a name="MorphPreMax.G"><span class="id" title="variable">G</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.gseries.html#MorphPreMax.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">Hypotheses</span> (<a name="MorphPreMax.dM"><span class="id" title="variable">dM</span></a> : <a class="idref" href="mathcomp.solvable.gseries.html#MorphPreMax.M"><span class="id" title="variable">M</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.gseries.html#MorphPreMax.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#MorphPreMax.D"><span class="id" title="variable">D</span></a>) (<a name="MorphPreMax.dG"><span class="id" title="variable">dG</span></a> : <a class="idref" href="mathcomp.solvable.gseries.html#MorphPreMax.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.gseries.html#MorphPreMax.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#MorphPreMax.D"><span class="id" title="variable">D</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="morphpre_maximal"><span class="id" title="lemma">morphpre_maximal</span></a> : <a class="idref" href="mathcomp.solvable.gseries.html#maximal"><span class="id" title="definition">maximal</span></a> (<a class="idref" href="mathcomp.solvable.gseries.html#MorphPreMax.f"><span class="id" title="variable">f</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.gseries.html#MorphPreMax.M"><span class="id" title="variable">M</span></a>) (<a class="idref" href="mathcomp.solvable.gseries.html#MorphPreMax.f"><span class="id" title="variable">f</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.gseries.html#MorphPreMax.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#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#maximal"><span class="id" title="definition">maximal</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#MorphPreMax.M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#MorphPreMax.G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="morphpre_maximal_eq"><span class="id" title="lemma">morphpre_maximal_eq</span></a> : <a class="idref" href="mathcomp.solvable.gseries.html#maximal_eq"><span class="id" title="definition">maximal_eq</span></a> (<a class="idref" href="mathcomp.solvable.gseries.html#MorphPreMax.f"><span class="id" title="variable">f</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.gseries.html#MorphPreMax.M"><span class="id" title="variable">M</span></a>) (<a class="idref" href="mathcomp.solvable.gseries.html#MorphPreMax.f"><span class="id" title="variable">f</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.gseries.html#MorphPreMax.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#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#maximal_eq"><span class="id" title="definition">maximal_eq</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#MorphPreMax.M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#MorphPreMax.G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gseries.html#MorphPreMax"><span class="id" title="section">MorphPreMax</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="InjmMax"><span class="id" title="section">InjmMax</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="InjmMax.gT"><span class="id" title="variable">gT</span></a> <a name="InjmMax.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>) (<a name="InjmMax.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.gseries.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 name="InjmMax.f"><span class="id" title="variable">f</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.solvable.gseries.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">}</span></a>).<br/> -<span class="id" title="keyword">Variables</span> <a name="InjmMax.M"><span class="id" title="variable">M</span></a> <a name="InjmMax.G"><span class="id" title="variable">G</span></a> <a name="InjmMax.L"><span class="id" title="variable">L</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.gseries.html#InjmMax.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">Hypothesis</span> <a name="InjmMax.injf"><span class="id" title="variable">injf</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#InjmMax.f"><span class="id" title="variable">f</span></a>.<br/> -<span class="id" title="keyword">Hypotheses</span> (<a name="InjmMax.dM"><span class="id" title="variable">dM</span></a> : <a class="idref" href="mathcomp.solvable.gseries.html#InjmMax.M"><span class="id" title="variable">M</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.gseries.html#InjmMax.D"><span class="id" title="variable">D</span></a>) (<a name="InjmMax.dG"><span class="id" title="variable">dG</span></a> : <a class="idref" href="mathcomp.solvable.gseries.html#InjmMax.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.gseries.html#InjmMax.D"><span class="id" title="variable">D</span></a>) (<a name="InjmMax.dL"><span class="id" title="variable">dL</span></a> : <a class="idref" href="mathcomp.solvable.gseries.html#InjmMax.L"><span class="id" title="variable">L</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.gseries.html#InjmMax.D"><span class="id" title="variable">D</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="injm_maximal"><span class="id" title="lemma">injm_maximal</span></a> : <a class="idref" href="mathcomp.solvable.gseries.html#maximal"><span class="id" title="definition">maximal</span></a> (<a class="idref" href="mathcomp.solvable.gseries.html#InjmMax.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#InjmMax.M"><span class="id" title="variable">M</span></a>) (<a class="idref" href="mathcomp.solvable.gseries.html#InjmMax.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#InjmMax.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#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#maximal"><span class="id" title="definition">maximal</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#InjmMax.M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#InjmMax.G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="injm_maximal_eq"><span class="id" title="lemma">injm_maximal_eq</span></a> : <a class="idref" href="mathcomp.solvable.gseries.html#maximal_eq"><span class="id" title="definition">maximal_eq</span></a> (<a class="idref" href="mathcomp.solvable.gseries.html#InjmMax.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#InjmMax.M"><span class="id" title="variable">M</span></a>) (<a class="idref" href="mathcomp.solvable.gseries.html#InjmMax.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#InjmMax.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#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#maximal_eq"><span class="id" title="definition">maximal_eq</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#InjmMax.M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#InjmMax.G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="injm_maxnormal"><span class="id" title="lemma">injm_maxnormal</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.gseries.html#InjmMax.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#InjmMax.M"><span class="id" title="variable">M</span></a>) (<a class="idref" href="mathcomp.solvable.gseries.html#InjmMax.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#InjmMax.G"><span class="id" title="variable">G</span></a>) (<a class="idref" href="mathcomp.solvable.gseries.html#InjmMax.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#InjmMax.L"><span class="id" title="variable">L</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.gseries.html#maxnormal"><span class="id" title="definition">maxnormal</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#InjmMax.M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#InjmMax.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#InjmMax.L"><span class="id" title="variable">L</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="injm_minnormal"><span class="id" title="lemma">injm_minnormal</span></a> : <a class="idref" href="mathcomp.solvable.gseries.html#minnormal"><span class="id" title="definition">minnormal</span></a> (<a class="idref" href="mathcomp.solvable.gseries.html#InjmMax.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#InjmMax.M"><span class="id" title="variable">M</span></a>) (<a class="idref" href="mathcomp.solvable.gseries.html#InjmMax.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#InjmMax.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#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#minnormal"><span class="id" title="definition">minnormal</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#InjmMax.M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#InjmMax.G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gseries.html#InjmMax"><span class="id" title="section">InjmMax</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="QuoMax"><span class="id" title="section">QuoMax</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="QuoMax.gT"><span class="id" title="variable">gT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<a name="QuoMax.K"><span class="id" title="variable">K</span></a> <a name="QuoMax.G"><span class="id" title="variable">G</span></a> <a name="QuoMax.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><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gseries.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">Lemma</span> <a name="cosetpre_maximal"><span class="id" title="lemma">cosetpre_maximal</span></a> (<span class="id" title="var">Q</span> <span class="id" title="var">R</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.gseries.html#QuoMax.K"><span class="id" title="variable">K</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.gseries.html#maximal"><span class="id" title="definition">maximal</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.gseries.html#QuoMax.K"><span class="id" title="variable">K</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.gseries.html#Q"><span class="id" title="variable">Q</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.gseries.html#QuoMax.K"><span class="id" title="variable">K</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.gseries.html#R"><span class="id" title="variable">R</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.gseries.html#maximal"><span class="id" title="definition">maximal</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#R"><span class="id" title="variable">R</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="cosetpre_maximal_eq"><span class="id" title="lemma">cosetpre_maximal_eq</span></a> (<span class="id" title="var">Q</span> <span class="id" title="var">R</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.gseries.html#QuoMax.K"><span class="id" title="variable">K</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.gseries.html#maximal_eq"><span class="id" title="definition">maximal_eq</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.gseries.html#QuoMax.K"><span class="id" title="variable">K</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.gseries.html#Q"><span class="id" title="variable">Q</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.gseries.html#QuoMax.K"><span class="id" title="variable">K</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.gseries.html#R"><span class="id" title="variable">R</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.gseries.html#maximal_eq"><span class="id" title="definition">maximal_eq</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#R"><span class="id" title="variable">R</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="quotient_maximal"><span class="id" title="lemma">quotient_maximal</span></a> :<br/> - <a class="idref" href="mathcomp.solvable.gseries.html#QuoMax.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7e8095b432e7aa5c3c22bb87584658b7"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#QuoMax.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.gseries.html#QuoMax.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7e8095b432e7aa5c3c22bb87584658b7"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#QuoMax.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.gseries.html#maximal"><span class="id" title="definition">maximal</span></a> (<a class="idref" href="mathcomp.solvable.gseries.html#QuoMax.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.gseries.html#QuoMax.K"><span class="id" title="variable">K</span></a>) (<a class="idref" href="mathcomp.solvable.gseries.html#QuoMax.H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#3e65ad3edf5f7fb3ea6bc63a878112a8"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#QuoMax.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.gseries.html#maximal"><span class="id" title="definition">maximal</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#QuoMax.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#QuoMax.H"><span class="id" title="variable">H</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="quotient_maximal_eq"><span class="id" title="lemma">quotient_maximal_eq</span></a> :<br/> - <a class="idref" href="mathcomp.solvable.gseries.html#QuoMax.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7e8095b432e7aa5c3c22bb87584658b7"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#QuoMax.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.gseries.html#QuoMax.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7e8095b432e7aa5c3c22bb87584658b7"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#QuoMax.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.gseries.html#maximal_eq"><span class="id" title="definition">maximal_eq</span></a> (<a class="idref" href="mathcomp.solvable.gseries.html#QuoMax.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.gseries.html#QuoMax.K"><span class="id" title="variable">K</span></a>) (<a class="idref" href="mathcomp.solvable.gseries.html#QuoMax.H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#3e65ad3edf5f7fb3ea6bc63a878112a8"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#QuoMax.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.gseries.html#maximal_eq"><span class="id" title="definition">maximal_eq</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#QuoMax.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#QuoMax.H"><span class="id" title="variable">H</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="maximalJ"><span class="id" title="lemma">maximalJ</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.solvable.gseries.html#maximal"><span class="id" title="definition">maximal</span></a> (<a class="idref" href="mathcomp.solvable.gseries.html#QuoMax.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.solvable.gseries.html#QuoMax.H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#maximal"><span class="id" title="definition">maximal</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#QuoMax.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#QuoMax.H"><span class="id" title="variable">H</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="maximal_eqJ"><span class="id" title="lemma">maximal_eqJ</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.solvable.gseries.html#maximal_eq"><span class="id" title="definition">maximal_eq</span></a> (<a class="idref" href="mathcomp.solvable.gseries.html#QuoMax.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.solvable.gseries.html#QuoMax.H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#maximal_eq"><span class="id" title="definition">maximal_eq</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#QuoMax.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#QuoMax.H"><span class="id" title="variable">H</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gseries.html#QuoMax"><span class="id" title="section">QuoMax</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="MaxNormalProps"><span class="id" title="section">MaxNormalProps</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="MaxNormalProps.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">A</span> <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.gseries.html#MaxNormalProps.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">G</span> <span class="id" title="var">H</span> <span class="id" title="var">K</span> <span class="id" title="var">L</span> <span class="id" title="var">M</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.gseries.html#MaxNormalProps.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">Lemma</span> <a name="maxnormal_normal"><span class="id" title="lemma">maxnormal_normal</span></a> <span class="id" title="var">A</span> <span class="id" title="var">B</span> : <a class="idref" href="mathcomp.solvable.gseries.html#maxnormal"><span class="id" title="definition">maxnormal</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#B"><span class="id" title="variable">B</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#B"><span class="id" title="variable">B</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.gseries.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7e8095b432e7aa5c3c22bb87584658b7"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#B"><span class="id" title="variable">B</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="maxnormal_proper"><span class="id" title="lemma">maxnormal_proper</span></a> <span class="id" title="var">A</span> <span class="id" title="var">B</span> <span class="id" title="var">C</span> : <a class="idref" href="mathcomp.solvable.gseries.html#maxnormal"><span class="id" title="definition">maxnormal</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#B"><span class="id" title="variable">B</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#C"><span class="id" title="variable">C</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.gseries.html#A"><span class="id" title="variable">A</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.gseries.html#B"><span class="id" title="variable">B</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="maxnormal_sub"><span class="id" title="lemma">maxnormal_sub</span></a> <span class="id" title="var">A</span> <span class="id" title="var">B</span> <span class="id" title="var">C</span> : <a class="idref" href="mathcomp.solvable.gseries.html#maxnormal"><span class="id" title="definition">maxnormal</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#B"><span class="id" title="variable">B</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#C"><span class="id" title="variable">C</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.gseries.html#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.solvable.gseries.html#B"><span class="id" title="variable">B</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="ex_maxnormal_ntrivg"><span class="id" title="lemma">ex_maxnormal_ntrivg</span></a> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.solvable.gseries.html#G"><span class="id" title="variable">G</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.gseries.html#MaxNormalProps.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.Specif.html#6556914db359db999889decec6a4a562"><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.gseries.html#N"><span class="id" title="variable">N</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.gseries.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.Specif.html#6556914db359db999889decec6a4a562"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="maxnormalM"><span class="id" title="lemma">maxnormalM</span></a> <span class="id" title="var">G</span> <span class="id" title="var">H</span> <span class="id" title="var">K</span> :<br/> - <a class="idref" href="mathcomp.solvable.gseries.html#maxnormal"><span class="id" title="definition">maxnormal</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.gseries.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.gseries.html#maxnormal"><span class="id" title="definition">maxnormal</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.gseries.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.gseries.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.gseries.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.gseries.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.gseries.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.gseries.html#G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="maxnormal_minnormal"><span class="id" title="lemma">maxnormal_minnormal</span></a> <span class="id" title="var">G</span> <span class="id" title="var">L</span> <span class="id" title="var">M</span> :<br/> - <a class="idref" href="mathcomp.solvable.gseries.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.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.gseries.html#M"><span class="id" title="variable">M</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.gseries.html#L"><span class="id" title="variable">L</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.gseries.html#G"><span class="id" title="variable">G</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.gseries.html#maxnormal"><span class="id" title="definition">maxnormal</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#L"><span class="id" title="variable">L</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.gseries.html#minnormal"><span class="id" title="definition">minnormal</span></a> (<a class="idref" href="mathcomp.solvable.gseries.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.gseries.html#M"><span class="id" title="variable">M</span></a>) (<a class="idref" href="mathcomp.solvable.gseries.html#L"><span class="id" title="variable">L</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#3e65ad3edf5f7fb3ea6bc63a878112a8"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#M"><span class="id" title="variable">M</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="minnormal_maxnormal"><span class="id" title="lemma">minnormal_maxnormal</span></a> <span class="id" title="var">G</span> <span class="id" title="var">L</span> <span class="id" title="var">M</span> :<br/> - <a class="idref" href="mathcomp.solvable.gseries.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7e8095b432e7aa5c3c22bb87584658b7"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.solvable.gseries.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.gseries.html#L"><span class="id" title="variable">L</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.gseries.html#M"><span class="id" title="variable">M</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.gseries.html#minnormal"><span class="id" title="definition">minnormal</span></a> (<a class="idref" href="mathcomp.solvable.gseries.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.gseries.html#M"><span class="id" title="variable">M</span></a>) (<a class="idref" href="mathcomp.solvable.gseries.html#L"><span class="id" title="variable">L</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#3e65ad3edf5f7fb3ea6bc63a878112a8"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#M"><span class="id" title="variable">M</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.gseries.html#maxnormal"><span class="id" title="definition">maxnormal</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#L"><span class="id" title="variable">L</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gseries.html#MaxNormalProps"><span class="id" title="section">MaxNormalProps</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="Simple"><span class="id" title="section">Simple</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">gT</span> <span class="id" title="var">rT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="simpleP"><span class="id" title="lemma">simpleP</span></a> <span class="id" title="var">gT</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.gseries.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/> - <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.gseries.html#G"><span class="id" title="variable">G</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#ba2b0e492d2b4675a0acf3ea92aabadd"><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.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.gseries.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.gseries.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.gseries.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.gseries.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.gseries.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.gseries.html#G"><span class="id" title="variable">G</span></a>)<br/> - (<a class="idref" href="mathcomp.solvable.gseries.html#simple"><span class="id" title="definition">simple</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#G"><span class="id" title="variable">G</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="quotient_simple"><span class="id" title="lemma">quotient_simple</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#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.gseries.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/> - <a class="idref" href="mathcomp.solvable.gseries.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.gseries.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.gseries.html#simple"><span class="id" title="definition">simple</span></a> (<a class="idref" href="mathcomp.solvable.gseries.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.gseries.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#6cd0f7b28b6092304087c7049437bb1a"><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.gseries.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="isog_simple"><span class="id" title="lemma">isog_simple</span></a> <span class="id" title="var">gT</span> <span class="id" title="var">rT</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.gseries.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>) (<span class="id" title="var">M</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.gseries.html#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.gseries.html#G"><span class="id" title="variable">G</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.gseries.html#M"><span class="id" title="variable">M</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.gseries.html#simple"><span class="id" title="definition">simple</span></a> <a class="idref" href="mathcomp.solvable.gseries.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#6cd0f7b28b6092304087c7049437bb1a"><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.gseries.html#M"><span class="id" title="variable">M</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="simple_maxnormal"><span class="id" title="lemma">simple_maxnormal</span></a> <span class="id" title="var">gT</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.gseries.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.gseries.html#simple"><span class="id" title="definition">simple</span></a> <a class="idref" href="mathcomp.solvable.gseries.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#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#maxnormal"><span class="id" title="definition">maxnormal</span></a> 1 <a class="idref" href="mathcomp.solvable.gseries.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gseries.html#Simple"><span class="id" title="section">Simple</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="Chiefs"><span class="id" title="section">Chiefs</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="Chiefs.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> <span class="id" title="var">H</span> <span class="id" title="var">U</span> <span class="id" title="var">V</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.gseries.html#Chiefs.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">Lemma</span> <a name="chief_factor_minnormal"><span class="id" title="lemma">chief_factor_minnormal</span></a> <span class="id" title="var">G</span> <span class="id" title="var">V</span> <span class="id" title="var">U</span> :<br/> - <a class="idref" href="mathcomp.solvable.gseries.html#chief_factor"><span class="id" title="definition">chief_factor</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#V"><span class="id" title="variable">V</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#U"><span class="id" title="variable">U</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.gseries.html#minnormal"><span class="id" title="definition">minnormal</span></a> (<a class="idref" href="mathcomp.solvable.gseries.html#U"><span class="id" title="variable">U</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#3e65ad3edf5f7fb3ea6bc63a878112a8"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#V"><span class="id" title="variable">V</span></a>) (<a class="idref" href="mathcomp.solvable.gseries.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.gseries.html#V"><span class="id" title="variable">V</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="acts_irrQ"><span class="id" title="lemma">acts_irrQ</span></a> <span class="id" title="var">G</span> <span class="id" title="var">U</span> <span class="id" title="var">V</span> :<br/> - <a class="idref" href="mathcomp.solvable.gseries.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.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.gseries.html#V"><span class="id" title="variable">V</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.gseries.html#V"><span class="id" title="variable">V</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7e8095b432e7aa5c3c22bb87584658b7"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#U"><span class="id" title="variable">U</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#acts_irreducibly"><span class="id" title="definition">acts_irreducibly</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#G"><span class="id" title="variable">G</span></a> (<a class="idref" href="mathcomp.solvable.gseries.html#U"><span class="id" title="variable">U</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#3e65ad3edf5f7fb3ea6bc63a878112a8"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#V"><span class="id" title="variable">V</span></a>) <a class="idref" href="mathcomp.fingroup.action.html#7dcafbe20414081f1fadfdd82eb4964c"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#7dcafbe20414081f1fadfdd82eb4964c"><span class="id" title="notation">Q</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.gseries.html#minnormal"><span class="id" title="definition">minnormal</span></a> (<a class="idref" href="mathcomp.solvable.gseries.html#U"><span class="id" title="variable">U</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#3e65ad3edf5f7fb3ea6bc63a878112a8"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#V"><span class="id" title="variable">V</span></a>) (<a class="idref" href="mathcomp.solvable.gseries.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.gseries.html#V"><span class="id" title="variable">V</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="chief_series_exists"><span class="id" title="lemma">chief_series_exists</span></a> <span class="id" title="var">H</span> <span class="id" title="var">G</span> :<br/> - <a class="idref" href="mathcomp.solvable.gseries.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.gseries.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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#c0bbd202248f4def7aaf0c316cf2c29e"><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.Specif.html#c0bbd202248f4def7aaf0c316cf2c29e"><span class="id" title="notation">|</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#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.gseries.html#466a2c8e043fca24105330dda0c4acf7"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.gseries.html#466a2c8e043fca24105330dda0c4acf7"><span class="id" title="notation">chief</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> 1%<span class="id" title="var">G</span> <a class="idref" href="mathcomp.solvable.gseries.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.Specif.html#c0bbd202248f4def7aaf0c316cf2c29e"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#last"><span class="id" title="definition">last</span></a> 1%<span class="id" title="var">G</span> <a class="idref" href="mathcomp.solvable.gseries.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.gseries.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.Specif.html#c0bbd202248f4def7aaf0c316cf2c29e"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gseries.html#Chiefs"><span class="id" title="section">Chiefs</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="Central"><span class="id" title="section">Central</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="Central.gT"><span class="id" title="variable">gT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<a name="Central.G"><span class="id" title="variable">G</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.gseries.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/> -<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.gseries.html#Central.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">Lemma</span> <a name="central_factor_central"><span class="id" title="lemma">central_factor_central</span></a> <span class="id" title="var">H</span> <span class="id" title="var">K</span> :<br/> - <a class="idref" href="mathcomp.solvable.gseries.html#central_factor"><span class="id" title="definition">central_factor</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#Central.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.gseries.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.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.gseries.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#3e65ad3edf5f7fb3ea6bc63a878112a8"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.gseries.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">\</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.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.gseries.html#Central.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.gseries.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="central_central_factor"><span class="id" title="lemma">central_central_factor</span></a> <span class="id" title="var">H</span> <span class="id" title="var">K</span> :<br/> - <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.gseries.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#3e65ad3edf5f7fb3ea6bc63a878112a8"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.gseries.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">\</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.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.gseries.html#Central.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.gseries.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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.gseries.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.gseries.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.gseries.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.gseries.html#Central.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.gseries.html#central_factor"><span class="id" title="definition">central_factor</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#Central.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#K"><span class="id" title="variable">K</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gseries.html#Central"><span class="id" title="section">Central</span></a>.<br/> -</div> -</div> - -<div id="footer"> -<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a> -</div> - -</div> - -</body> -</html>
\ No newline at end of file |