diff options
| author | Enrico Tassi | 2019-05-22 13:43:08 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-05-22 15:34:14 +0200 |
| commit | 748d716efb2f2f75946c8386e441ce1789806a39 (patch) | |
| tree | fe7bb1c5235550410c64e968f4a4d69b7f10a047 /docs/htmldoc/mathcomp.solvable.extraspecial.html | |
| parent | 415be3b908daadabf178a292c885db78e5b2c9a4 (diff) | |
htmldoc regenerated
Diffstat (limited to 'docs/htmldoc/mathcomp.solvable.extraspecial.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.solvable.extraspecial.html | 123 |
1 files changed, 61 insertions, 62 deletions
diff --git a/docs/htmldoc/mathcomp.solvable.extraspecial.html b/docs/htmldoc/mathcomp.solvable.extraspecial.html index 4e8e995..c0f4274 100644 --- a/docs/htmldoc/mathcomp.solvable.extraspecial.html +++ b/docs/htmldoc/mathcomp.solvable.extraspecial.html @@ -21,7 +21,6 @@ <div class="code"> <span class="comment">(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. <br/> Distributed under the terms of CeCILL-B. *)</span><br/> -<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#"><span class="id" title="library">mathcomp.ssreflect.ssreflect</span></a>.<br/> <br/> </div> @@ -80,58 +79,58 @@ <span class="id" title="keyword">Section</span> <a name="Pextraspecial.Construction"><span class="id" title="section">Construction</span></a>.<br/> <br/> -<span class="id" title="keyword">Variable</span> <a name="Pextraspecial.Construction.p"><span class="id" title="variable">p</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> +<span class="id" title="keyword">Variable</span> <a name="Pextraspecial.Construction.p"><span class="id" title="variable">p</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="Pextraspecial.act"><span class="id" title="definition">act</span></a> <span class="id" title="var">ij</span> (<span class="id" title="var">k</span> : <a class="idref" href="mathcomp.algebra.zmodp.html#9daeb9ead3dc7cfd1f9338b8de9c8c09"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#9daeb9ead3dc7cfd1f9338b8de9c8c09"><span class="id" title="notation">Z_p</span></a>) := <span class="id" title="keyword">let</span>: <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <span class="id" title="var">j</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a> := <a class="idref" href="mathcomp.solvable.extraspecial.html#ij"><span class="id" title="variable">ij</span></a> <span class="id" title="tactic">in</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.algebra.ssralg.html#ae4d81913e6239182a9ac7467ffde8cd"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <span class="id" title="var">j</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <span class="id" title="var">j</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a>.<br/> -<span class="id" title="keyword">Lemma</span> <a name="Pextraspecial.actP"><span class="id" title="lemma">actP</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#is_action"><span class="id" title="definition">is_action</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#9daeb9ead3dc7cfd1f9338b8de9c8c09"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#9daeb9ead3dc7cfd1f9338b8de9c8c09"><span class="id" title="notation">Z_p</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Pextraspecial.act"><span class="id" title="definition">act</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="Pextraspecial.act"><span class="id" title="definition">act</span></a> <span class="id" title="var">ij</span> (<span class="id" title="var">k</span> : <a class="idref" href="mathcomp.algebra.zmodp.html#fdcfc8589237bc0c67b9484f75e68729"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#fdcfc8589237bc0c67b9484f75e68729"><span class="id" title="notation">Z_p</span></a>) := <span class="id" title="keyword">let</span>: <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <span class="id" title="var">j</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> := <a class="idref" href="mathcomp.solvable.extraspecial.html#ij"><span class="id" title="variable">ij</span></a> <span class="id" title="tactic">in</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.algebra.ssralg.html#c7f78cf1f6a5e4f664654f7d671ca752"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <span class="id" title="var">j</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <span class="id" title="var">j</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="Pextraspecial.actP"><span class="id" title="lemma">actP</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#is_action"><span class="id" title="definition">is_action</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#fdcfc8589237bc0c67b9484f75e68729"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#fdcfc8589237bc0c67b9484f75e68729"><span class="id" title="notation">Z_p</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Pextraspecial.act"><span class="id" title="definition">act</span></a>.<br/> <span class="id" title="keyword">Canonical</span> <span class="id" title="var">action</span> := <a class="idref" href="mathcomp.fingroup.action.html#Action"><span class="id" title="constructor">Action</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Pextraspecial.actP"><span class="id" title="lemma">actP</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="Pextraspecial.gactP"><span class="id" title="lemma">gactP</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#is_groupAction"><span class="id" title="definition">is_groupAction</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#9daeb9ead3dc7cfd1f9338b8de9c8c09"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#9daeb9ead3dc7cfd1f9338b8de9c8c09"><span class="id" title="notation">Z_p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#9daeb9ead3dc7cfd1f9338b8de9c8c09"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#9daeb9ead3dc7cfd1f9338b8de9c8c09"><span class="id" title="notation">Z_p</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Pextraspecial.action"><span class="id" title="definition">action</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="Pextraspecial.gactP"><span class="id" title="lemma">gactP</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#is_groupAction"><span class="id" title="definition">is_groupAction</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#fdcfc8589237bc0c67b9484f75e68729"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#fdcfc8589237bc0c67b9484f75e68729"><span class="id" title="notation">Z_p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#fdcfc8589237bc0c67b9484f75e68729"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#fdcfc8589237bc0c67b9484f75e68729"><span class="id" title="notation">Z_p</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Pextraspecial.action"><span class="id" title="definition">action</span></a>.<br/> <span class="id" title="keyword">Definition</span> <a name="Pextraspecial.groupAction"><span class="id" title="definition">groupAction</span></a> := <a class="idref" href="mathcomp.fingroup.action.html#GroupAction"><span class="id" title="constructor">GroupAction</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Pextraspecial.gactP"><span class="id" title="lemma">gactP</span></a>.<br/> <br/> -<span class="id" title="keyword">Fact</span> <a name="Pextraspecial.gtype_key"><span class="id" title="lemma">gtype_key</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a>. <br/> -<span class="id" title="keyword">Definition</span> <a name="Pextraspecial.gtype"><span class="id" title="definition">gtype</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#locked_with"><span class="id" title="definition">locked_with</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Pextraspecial.gtype_key"><span class="id" title="lemma">gtype_key</span></a> (<a class="idref" href="mathcomp.fingroup.gproduct.html#sdprod_groupType"><span class="id" title="definition">sdprod_groupType</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Pextraspecial.groupAction"><span class="id" title="definition">groupAction</span></a>).<br/> +<span class="id" title="keyword">Fact</span> <a name="Pextraspecial.gtype_key"><span class="id" title="lemma">gtype_key</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a>. <br/> +<span class="id" title="keyword">Definition</span> <a name="Pextraspecial.gtype"><span class="id" title="definition">gtype</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#locked_with"><span class="id" title="definition">locked_with</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Pextraspecial.gtype_key"><span class="id" title="lemma">gtype_key</span></a> (<a class="idref" href="mathcomp.fingroup.gproduct.html#sdprod_groupType"><span class="id" title="definition">sdprod_groupType</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Pextraspecial.groupAction"><span class="id" title="definition">groupAction</span></a>).<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="Pextraspecial.ngtype"><span class="id" title="definition">ngtype</span></a> := <a class="idref" href="mathcomp.solvable.center.html#ncprod"><span class="id" title="definition">ncprod</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Pextraspecial.gtype"><span class="id" title="definition">gtype</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="Pextraspecial.ngtype"><span class="id" title="definition">ngtype</span></a> := <a class="idref" href="mathcomp.solvable.center.html#ncprod"><span class="id" title="definition">ncprod</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#e98634a3dc0445a0bdea71fc5975bb33"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#e98634a3dc0445a0bdea71fc5975bb33"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#e98634a3dc0445a0bdea71fc5975bb33"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Pextraspecial.gtype"><span class="id" title="definition">gtype</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#e98634a3dc0445a0bdea71fc5975bb33"><span class="id" title="notation">]</span></a>.<br/> <br/> <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.extraspecial.html#Pextraspecial.Construction"><span class="id" title="section">Construction</span></a>.<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="Pextraspecial.ngtypeQ"><span class="id" title="definition">ngtypeQ</span></a> <span class="id" title="var">n</span> := <a class="idref" href="mathcomp.solvable.center.html#xcprod"><span class="id" title="definition">xcprod</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Pextraspecial.ngtype"><span class="id" title="definition">ngtype</span></a> 2 <a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.solvable.extremal.html#24d327e6c4148d6dd7b561fa4e1277bd"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extremal.html#24d327e6c4148d6dd7b561fa4e1277bd"><span class="id" title="notation">Q_8</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="Pextraspecial.ngtypeQ"><span class="id" title="definition">ngtypeQ</span></a> <span class="id" title="var">n</span> := <a class="idref" href="mathcomp.solvable.center.html#xcprod"><span class="id" title="definition">xcprod</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#e98634a3dc0445a0bdea71fc5975bb33"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#e98634a3dc0445a0bdea71fc5975bb33"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#e98634a3dc0445a0bdea71fc5975bb33"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Pextraspecial.ngtype"><span class="id" title="definition">ngtype</span></a> 2 <a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#e98634a3dc0445a0bdea71fc5975bb33"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.solvable.extremal.html#de4614b692797c6dc4c82a4b56748090"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extremal.html#de4614b692797c6dc4c82a4b56748090"><span class="id" title="notation">Q_8</span></a>.<br/> <br/> <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.extraspecial.html#Pextraspecial"><span class="id" title="module">Pextraspecial</span></a>.<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="4930a1d10a5aad7b22b82525a70cd4ea"><span class="id" title="notation">"</span></a>p ^{1+2}" := (<a class="idref" href="mathcomp.solvable.extraspecial.html#gtype"><span class="id" title="definition">Pextraspecial.gtype</span></a> <span class="id" title="var">p</span>) : <span class="id" title="var">type_scope</span>.<br/> -<span class="id" title="keyword">Notation</span> <a name="354a7719245e28a5f784cfb19c81f53a"><span class="id" title="notation">"</span></a>p ^{1+2}" := <a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#gsort"><span class="id" title="abbreviation">gsort</span></a> <span class="id" title="var">p</span><a class="idref" href="mathcomp.solvable.extraspecial.html#4930a1d10a5aad7b22b82525a70cd4ea"><span class="id" title="notation">^{1+2}</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">]</span></a> : <span class="id" title="var">group_scope</span>.<br/> -<span class="id" title="keyword">Notation</span> <a name="fecf17babbfd20e65dfb992ab39dd060"><span class="id" title="notation">"</span></a>p ^{1+2}" := <a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#gsort"><span class="id" title="abbreviation">gsort</span></a> <span class="id" title="var">p</span><a class="idref" href="mathcomp.solvable.extraspecial.html#4930a1d10a5aad7b22b82525a70cd4ea"><span class="id" title="notation">^{1+2}</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">]</span></a>%<span class="id" title="var">G</span> : <span class="id" title="var">Group_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="a2aa0b4db369a3ee2789c992498a5e0e"><span class="id" title="notation">"</span></a>p ^{1+2}" := (<a class="idref" href="mathcomp.solvable.extraspecial.html#gtype"><span class="id" title="definition">Pextraspecial.gtype</span></a> <span class="id" title="var">p</span>) : <span class="id" title="var">type_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="13d1250ec3fb36839cafb80c8df79307"><span class="id" title="notation">"</span></a>p ^{1+2}" := <a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#gsort"><span class="id" title="abbreviation">gsort</span></a> <span class="id" title="var">p</span><a class="idref" href="mathcomp.solvable.extraspecial.html#a2aa0b4db369a3ee2789c992498a5e0e"><span class="id" title="notation">^{1+2}</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">]</span></a> : <span class="id" title="var">group_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="733630db88ea59f0786eda47f95f579b"><span class="id" title="notation">"</span></a>p ^{1+2}" := <a class="idref" href="mathcomp.fingroup.fingroup.html#e98634a3dc0445a0bdea71fc5975bb33"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#e98634a3dc0445a0bdea71fc5975bb33"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#e98634a3dc0445a0bdea71fc5975bb33"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#gsort"><span class="id" title="abbreviation">gsort</span></a> <span class="id" title="var">p</span><a class="idref" href="mathcomp.solvable.extraspecial.html#a2aa0b4db369a3ee2789c992498a5e0e"><span class="id" title="notation">^{1+2}</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#e98634a3dc0445a0bdea71fc5975bb33"><span class="id" title="notation">]</span></a>%<span class="id" title="var">G</span> : <span class="id" title="var">Group_scope</span>.<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="d5734ed590b969504e2a2cee2726792f"><span class="id" title="notation">"</span></a>p ^{1+2* n }" := (<a class="idref" href="mathcomp.solvable.extraspecial.html#ngtype"><span class="id" title="definition">Pextraspecial.ngtype</span></a> <span class="id" title="var">p</span> <span class="id" title="var">n</span>) : <span class="id" title="var">type_scope</span>.<br/> -<span class="id" title="keyword">Notation</span> <a name="a7c316c84561ad9c93c7896226b3cab1"><span class="id" title="notation">"</span></a>p ^{1+2* n }" := <a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#gsort"><span class="id" title="abbreviation">gsort</span></a> <span class="id" title="var">p</span><a class="idref" href="mathcomp.solvable.extraspecial.html#d5734ed590b969504e2a2cee2726792f"><span class="id" title="notation">^{1+2*</span></a><span class="id" title="var">n</span><a class="idref" href="mathcomp.solvable.extraspecial.html#d5734ed590b969504e2a2cee2726792f"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">]</span></a> : <span class="id" title="var">group_scope</span>.<br/> -<span class="id" title="keyword">Notation</span> <a name="6d7462d9f1e45e8985bc5fef0096491d"><span class="id" title="notation">"</span></a>p ^{1+2* n }" := <a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#gsort"><span class="id" title="abbreviation">gsort</span></a> <span class="id" title="var">p</span><a class="idref" href="mathcomp.solvable.extraspecial.html#d5734ed590b969504e2a2cee2726792f"><span class="id" title="notation">^{1+2*</span></a><span class="id" title="var">n</span><a class="idref" href="mathcomp.solvable.extraspecial.html#d5734ed590b969504e2a2cee2726792f"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">]</span></a>%<span class="id" title="var">G</span> : <span class="id" title="var">Group_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="e83f70c26e2f0fabe22aa5af61f12478"><span class="id" title="notation">"</span></a>p ^{1+2* n }" := (<a class="idref" href="mathcomp.solvable.extraspecial.html#ngtype"><span class="id" title="definition">Pextraspecial.ngtype</span></a> <span class="id" title="var">p</span> <span class="id" title="var">n</span>) : <span class="id" title="var">type_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="50748714e6bbf7d0964fc12c665fb268"><span class="id" title="notation">"</span></a>p ^{1+2* n }" := <a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#gsort"><span class="id" title="abbreviation">gsort</span></a> <span class="id" title="var">p</span><a class="idref" href="mathcomp.solvable.extraspecial.html#e83f70c26e2f0fabe22aa5af61f12478"><span class="id" title="notation">^{1+2*</span></a><span class="id" title="var">n</span><a class="idref" href="mathcomp.solvable.extraspecial.html#e83f70c26e2f0fabe22aa5af61f12478"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">]</span></a> : <span class="id" title="var">group_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="1858156ab389b20f00955cf2f88b8d78"><span class="id" title="notation">"</span></a>p ^{1+2* n }" := <a class="idref" href="mathcomp.fingroup.fingroup.html#e98634a3dc0445a0bdea71fc5975bb33"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#e98634a3dc0445a0bdea71fc5975bb33"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#e98634a3dc0445a0bdea71fc5975bb33"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#gsort"><span class="id" title="abbreviation">gsort</span></a> <span class="id" title="var">p</span><a class="idref" href="mathcomp.solvable.extraspecial.html#e83f70c26e2f0fabe22aa5af61f12478"><span class="id" title="notation">^{1+2*</span></a><span class="id" title="var">n</span><a class="idref" href="mathcomp.solvable.extraspecial.html#e83f70c26e2f0fabe22aa5af61f12478"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#e98634a3dc0445a0bdea71fc5975bb33"><span class="id" title="notation">]</span></a>%<span class="id" title="var">G</span> : <span class="id" title="var">Group_scope</span>.<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="ba80690771cb8385c9d31dd9f3c06f59"><span class="id" title="notation">"</span></a>''D^' n" := (<a class="idref" href="mathcomp.solvable.extraspecial.html#ngtype"><span class="id" title="definition">Pextraspecial.ngtype</span></a> 2 <span class="id" title="var">n</span>) : <span class="id" title="var">type_scope</span>.<br/> -<span class="id" title="keyword">Notation</span> <a name="a8a830ccefaf9cb4d4b2f49d65e5334b"><span class="id" title="notation">"</span></a>''D^' n" := <a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#gsort"><span class="id" title="abbreviation">gsort</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#ba80690771cb8385c9d31dd9f3c06f59"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#ba80690771cb8385c9d31dd9f3c06f59"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#ba80690771cb8385c9d31dd9f3c06f59"><span class="id" title="notation">^</span></a><span class="id" title="var">n</span><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">]</span></a> : <span class="id" title="var">group_scope</span>.<br/> -<span class="id" title="keyword">Notation</span> <a name="11fb2c38b9f35b58f4576164683416e2"><span class="id" title="notation">"</span></a>''D^' n" := <a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#gsort"><span class="id" title="abbreviation">gsort</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#ba80690771cb8385c9d31dd9f3c06f59"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#ba80690771cb8385c9d31dd9f3c06f59"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#ba80690771cb8385c9d31dd9f3c06f59"><span class="id" title="notation">^</span></a><span class="id" title="var">n</span><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">]</span></a>%<span class="id" title="var">G</span> : <span class="id" title="var">Group_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="eb94ddf01a1cc46d38672f746abe2ce3"><span class="id" title="notation">"</span></a>''D^' n" := (<a class="idref" href="mathcomp.solvable.extraspecial.html#ngtype"><span class="id" title="definition">Pextraspecial.ngtype</span></a> 2 <span class="id" title="var">n</span>) : <span class="id" title="var">type_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="7aef83b7aca71eca9cb3114e50804f53"><span class="id" title="notation">"</span></a>''D^' n" := <a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#gsort"><span class="id" title="abbreviation">gsort</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#eb94ddf01a1cc46d38672f746abe2ce3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#eb94ddf01a1cc46d38672f746abe2ce3"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#eb94ddf01a1cc46d38672f746abe2ce3"><span class="id" title="notation">^</span></a><span class="id" title="var">n</span><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">]</span></a> : <span class="id" title="var">group_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="85fbcdd7ed3c17a1a9687625c1366d82"><span class="id" title="notation">"</span></a>''D^' n" := <a class="idref" href="mathcomp.fingroup.fingroup.html#e98634a3dc0445a0bdea71fc5975bb33"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#e98634a3dc0445a0bdea71fc5975bb33"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#e98634a3dc0445a0bdea71fc5975bb33"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#gsort"><span class="id" title="abbreviation">gsort</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#eb94ddf01a1cc46d38672f746abe2ce3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#eb94ddf01a1cc46d38672f746abe2ce3"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#eb94ddf01a1cc46d38672f746abe2ce3"><span class="id" title="notation">^</span></a><span class="id" title="var">n</span><a class="idref" href="mathcomp.fingroup.fingroup.html#e98634a3dc0445a0bdea71fc5975bb33"><span class="id" title="notation">]</span></a>%<span class="id" title="var">G</span> : <span class="id" title="var">Group_scope</span>.<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="060cb01c343ba334280fa026c9b5c80b"><span class="id" title="notation">"</span></a>''D^' n * 'Q'" := (<a class="idref" href="mathcomp.solvable.extraspecial.html#ngtypeQ"><span class="id" title="definition">Pextraspecial.ngtypeQ</span></a> <span class="id" title="var">n</span>) : <span class="id" title="var">type_scope</span>.<br/> -<span class="id" title="keyword">Notation</span> <a name="e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">"</span></a>''D^' n * 'Q'" := <a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#gsort"><span class="id" title="abbreviation">gsort</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#060cb01c343ba334280fa026c9b5c80b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#060cb01c343ba334280fa026c9b5c80b"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#060cb01c343ba334280fa026c9b5c80b"><span class="id" title="notation">^</span></a><span class="id" title="var">n</span><a class="idref" href="mathcomp.solvable.extraspecial.html#060cb01c343ba334280fa026c9b5c80b"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#060cb01c343ba334280fa026c9b5c80b"><span class="id" title="notation">Q</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">]</span></a> : <span class="id" title="var">group_scope</span>.<br/> -<span class="id" title="keyword">Notation</span> <a name="802dab5ec0a31aa7f85d95659b7db935"><span class="id" title="notation">"</span></a>''D^' n * 'Q'" := <a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#gsort"><span class="id" title="abbreviation">gsort</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#060cb01c343ba334280fa026c9b5c80b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#060cb01c343ba334280fa026c9b5c80b"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#060cb01c343ba334280fa026c9b5c80b"><span class="id" title="notation">^</span></a><span class="id" title="var">n</span><a class="idref" href="mathcomp.solvable.extraspecial.html#060cb01c343ba334280fa026c9b5c80b"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#060cb01c343ba334280fa026c9b5c80b"><span class="id" title="notation">Q</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">]</span></a>%<span class="id" title="var">G</span> : <span class="id" title="var">Group_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="5ae1a9e1f84a4c1cf90fc959c1b39206"><span class="id" title="notation">"</span></a>''D^' n * 'Q'" := (<a class="idref" href="mathcomp.solvable.extraspecial.html#ngtypeQ"><span class="id" title="definition">Pextraspecial.ngtypeQ</span></a> <span class="id" title="var">n</span>) : <span class="id" title="var">type_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="7c4503382583a2ccddcad8489a0e4194"><span class="id" title="notation">"</span></a>''D^' n * 'Q'" := <a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#gsort"><span class="id" title="abbreviation">gsort</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#5ae1a9e1f84a4c1cf90fc959c1b39206"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#5ae1a9e1f84a4c1cf90fc959c1b39206"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#5ae1a9e1f84a4c1cf90fc959c1b39206"><span class="id" title="notation">^</span></a><span class="id" title="var">n</span><a class="idref" href="mathcomp.solvable.extraspecial.html#5ae1a9e1f84a4c1cf90fc959c1b39206"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#5ae1a9e1f84a4c1cf90fc959c1b39206"><span class="id" title="notation">Q</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">]</span></a> : <span class="id" title="var">group_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="2ed054a5fadef06f690f45c3e07dc0d7"><span class="id" title="notation">"</span></a>''D^' n * 'Q'" := <a class="idref" href="mathcomp.fingroup.fingroup.html#e98634a3dc0445a0bdea71fc5975bb33"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#e98634a3dc0445a0bdea71fc5975bb33"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#e98634a3dc0445a0bdea71fc5975bb33"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#gsort"><span class="id" title="abbreviation">gsort</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#5ae1a9e1f84a4c1cf90fc959c1b39206"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#5ae1a9e1f84a4c1cf90fc959c1b39206"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#5ae1a9e1f84a4c1cf90fc959c1b39206"><span class="id" title="notation">^</span></a><span class="id" title="var">n</span><a class="idref" href="mathcomp.solvable.extraspecial.html#5ae1a9e1f84a4c1cf90fc959c1b39206"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#5ae1a9e1f84a4c1cf90fc959c1b39206"><span class="id" title="notation">Q</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#e98634a3dc0445a0bdea71fc5975bb33"><span class="id" title="notation">]</span></a>%<span class="id" title="var">G</span> : <span class="id" title="var">Group_scope</span>.<br/> <br/> <span class="id" title="keyword">Section</span> <a name="ExponentPextraspecialTheory"><span class="id" title="section">ExponentPextraspecialTheory</span></a>.<br/> <br/> -<span class="id" title="keyword">Variable</span> <a name="ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> +<span class="id" title="keyword">Variable</span> <a name="ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> <span class="id" title="keyword">Hypothesis</span> <a name="ExponentPextraspecialTheory.p_pr"><span class="id" title="variable">p_pr</span></a> : <a class="idref" href="mathcomp.ssreflect.prime.html#prime"><span class="id" title="definition">prime</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a>.<br/> <span class="id" title="keyword">Let</span> <a name="ExponentPextraspecialTheory.p_gt1"><span class="id" title="variable">p_gt1</span></a> := <a class="idref" href="mathcomp.ssreflect.prime.html#prime_gt1"><span class="id" title="lemma">prime_gt1</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p_pr"><span class="id" title="variable">p_pr</span></a>.<br/> <span class="id" title="keyword">Let</span> <a name="ExponentPextraspecialTheory.p_gt0"><span class="id" title="variable">p_gt0</span></a> := <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ltnW"><span class="id" title="lemma">ltnW</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p_gt1"><span class="id" title="variable">p_gt1</span></a>.<br/> @@ -139,14 +138,14 @@ <br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="card_pX1p2"><span class="id" title="lemma">card_pX1p2</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#354a7719245e28a5f784cfb19c81f53a"><span class="id" title="notation">^{1+2}</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> 3)%<span class="id" title="var">N</span>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="card_pX1p2"><span class="id" title="lemma">card_pX1p2</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#13d1250ec3fb36839cafb80c8df79307"><span class="id" title="notation">^{1+2}</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> (<a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#81fd94e251a61ee523cdd7855774ae7c"><span class="id" title="notation">^</span></a> 3)%<span class="id" title="var">N</span>.<br/> <br/> <span class="id" title="keyword">Lemma</span> <a name="Grp_pX1p2"><span class="id" title="lemma">Grp_pX1p2</span></a> :<br/> - <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#354a7719245e28a5f784cfb19c81f53a"><span class="id" title="notation">^{1+2}</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#2e7e6fdc2fcc257cb8670b6b97d9b9ee"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#2e7e6fdc2fcc257cb8670b6b97d9b9ee"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#2e7e6fdc2fcc257cb8670b6b97d9b9ee"><span class="id" title="notation">Grp</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#2e7e6fdc2fcc257cb8670b6b97d9b9ee"><span class="id" title="notation">(</span></a><span class="id" title="var">x</span> <a class="idref" href="mathcomp.fingroup.presentation.html#2e7e6fdc2fcc257cb8670b6b97d9b9ee"><span class="id" title="notation">:</span></a> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.fingroup.presentation.html#953d1fbe50819ac104ff2928ed9f1f35"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#5b8f67ffc457596b97fe80b0e075accd"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#93f82d9635dc31e1d0b435f42eb3dc73"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#5b8f67ffc457596b97fe80b0e075accd"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#93f82d9635dc31e1d0b435f42eb3dc73"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#5b8f67ffc457596b97fe80b0e075accd"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#a0040f72df5ea25d5ed5fbb0e00c50b5"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#a0040f72df5ea25d5ed5fbb0e00c50b5"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#a0040f72df5ea25d5ed5fbb0e00c50b5"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#a0040f72df5ea25d5ed5fbb0e00c50b5"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#5b8f67ffc457596b97fe80b0e075accd"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#a0040f72df5ea25d5ed5fbb0e00c50b5"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#a0040f72df5ea25d5ed5fbb0e00c50b5"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#a0040f72df5ea25d5ed5fbb0e00c50b5"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#a0040f72df5ea25d5ed5fbb0e00c50b5"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#5b8f67ffc457596b97fe80b0e075accd"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#2e7e6fdc2fcc257cb8670b6b97d9b9ee"><span class="id" title="notation">)</span></a>.<br/> + <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#13d1250ec3fb36839cafb80c8df79307"><span class="id" title="notation">^{1+2}</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#b9a7ff3fba421494dc2f1155a1739bdd"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#b9a7ff3fba421494dc2f1155a1739bdd"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#b9a7ff3fba421494dc2f1155a1739bdd"><span class="id" title="notation">Grp</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#b9a7ff3fba421494dc2f1155a1739bdd"><span class="id" title="notation">(</span></a><span class="id" title="var">x</span> <a class="idref" href="mathcomp.fingroup.presentation.html#b9a7ff3fba421494dc2f1155a1739bdd"><span class="id" title="notation">:</span></a> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.fingroup.presentation.html#dabeb9211165bee23a272123a1fbb765"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#2ae8188eecf4af229df8a7611e947bc2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#0280afab3b6487b32e979a01bfa577e6"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#2ae8188eecf4af229df8a7611e947bc2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#0280afab3b6487b32e979a01bfa577e6"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#2ae8188eecf4af229df8a7611e947bc2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#2363e834cb9646bb24ef8d00777408b1"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#2363e834cb9646bb24ef8d00777408b1"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#2363e834cb9646bb24ef8d00777408b1"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#2363e834cb9646bb24ef8d00777408b1"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#2ae8188eecf4af229df8a7611e947bc2"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#2363e834cb9646bb24ef8d00777408b1"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#2363e834cb9646bb24ef8d00777408b1"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#2363e834cb9646bb24ef8d00777408b1"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#2363e834cb9646bb24ef8d00777408b1"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#2ae8188eecf4af229df8a7611e947bc2"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#b9a7ff3fba421494dc2f1155a1739bdd"><span class="id" title="notation">)</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="pX1p2_pgroup"><span class="id" title="lemma">pX1p2_pgroup</span></a> : <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#354a7719245e28a5f784cfb19c81f53a"><span class="id" title="notation">^{1+2}</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="pX1p2_pgroup"><span class="id" title="lemma">pX1p2_pgroup</span></a> : <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#15605b2ce8a0bd336aafa96c5cc1afdc"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#15605b2ce8a0bd336aafa96c5cc1afdc"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#13d1250ec3fb36839cafb80c8df79307"><span class="id" title="notation">^{1+2}</span></a>.<br/> <br/> </div> @@ -155,7 +154,7 @@ This is part of the existence half of Aschbacher ex. (8.7)(1) </div> <div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="pX1p2_extraspecial"><span class="id" title="lemma">pX1p2_extraspecial</span></a> : <a class="idref" href="mathcomp.solvable.maximal.html#extraspecial"><span class="id" title="definition">extraspecial</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#354a7719245e28a5f784cfb19c81f53a"><span class="id" title="notation">^{1+2}</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="pX1p2_extraspecial"><span class="id" title="lemma">pX1p2_extraspecial</span></a> : <a class="idref" href="mathcomp.solvable.maximal.html#extraspecial"><span class="id" title="definition">extraspecial</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#13d1250ec3fb36839cafb80c8df79307"><span class="id" title="notation">^{1+2}</span></a>.<br/> <br/> </div> @@ -164,7 +163,7 @@ This is part of the existence half of Aschbacher ex. (8.7)(1) </div> <div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="exponent_pX1p2"><span class="id" title="lemma">exponent_pX1p2</span></a> : <a class="idref" href="mathcomp.ssreflect.ssrnat.html#odd"><span class="id" title="definition">odd</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.abelian.html#exponent"><span class="id" title="definition">exponent</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#354a7719245e28a5f784cfb19c81f53a"><span class="id" title="notation">^{1+2}</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#aa34fd1c61c5cf0a3356b624a5d2afed"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="exponent_pX1p2"><span class="id" title="lemma">exponent_pX1p2</span></a> : <a class="idref" href="mathcomp.ssreflect.ssrnat.html#odd"><span class="id" title="definition">odd</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.abelian.html#exponent"><span class="id" title="definition">exponent</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#13d1250ec3fb36839cafb80c8df79307"><span class="id" title="notation">^{1+2}</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#bde82eab2fe4a0799bc2419e587505d4"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a>.<br/> <br/> </div> @@ -173,8 +172,8 @@ This is the uniqueness half of Aschbacher ex. (8.7)(1) </div> <div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="isog_pX1p2"><span class="id" title="lemma">isog_pX1p2</span></a> (<span class="id" title="var">gT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) :<br/> - <a class="idref" href="mathcomp.solvable.maximal.html#extraspecial"><span class="id" title="definition">extraspecial</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.abelian.html#exponent"><span class="id" title="definition">exponent</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#aa34fd1c61c5cf0a3356b624a5d2afed"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> 3)%<span class="id" title="var">N</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#354a7719245e28a5f784cfb19c81f53a"><span class="id" title="notation">^{1+2}</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="isog_pX1p2"><span class="id" title="lemma">isog_pX1p2</span></a> (<span class="id" title="var">gT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<span class="id" title="var">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.extraspecial.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.maximal.html#extraspecial"><span class="id" title="definition">extraspecial</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.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.abelian.html#exponent"><span class="id" title="definition">exponent</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#bde82eab2fe4a0799bc2419e587505d4"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> (<a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#81fd94e251a61ee523cdd7855774ae7c"><span class="id" title="notation">^</span></a> 3)%<span class="id" title="var">N</span> <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.extraspecial.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.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#13d1250ec3fb36839cafb80c8df79307"><span class="id" title="notation">^{1+2}</span></a>.<br/> <br/> <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory"><span class="id" title="section">ExponentPextraspecialTheory</span></a>.<br/> @@ -183,19 +182,19 @@ <span class="id" title="keyword">Section</span> <a name="GeneralExponentPextraspecialTheory"><span class="id" title="section">GeneralExponentPextraspecialTheory</span></a>.<br/> <br/> -<span class="id" title="keyword">Variable</span> <a name="GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> +<span class="id" title="keyword">Variable</span> <a name="GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="pX1p2id"><span class="id" title="lemma">pX1p2id</span></a> : <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a7c316c84561ad9c93c7896226b3cab1"><span class="id" title="notation">^{1+2*</span></a>1<a class="idref" href="mathcomp.solvable.extraspecial.html#a7c316c84561ad9c93c7896226b3cab1"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#354a7719245e28a5f784cfb19c81f53a"><span class="id" title="notation">^{1+2}</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="pX1p2id"><span class="id" title="lemma">pX1p2id</span></a> : <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#50748714e6bbf7d0964fc12c665fb268"><span class="id" title="notation">^{1+2*</span></a>1<a class="idref" href="mathcomp.solvable.extraspecial.html#50748714e6bbf7d0964fc12c665fb268"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#13d1250ec3fb36839cafb80c8df79307"><span class="id" title="notation">^{1+2}</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="pX1p2S"><span class="id" title="lemma">pX1p2S</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.solvable.center.html#xcprod_spec"><span class="id" title="inductive">xcprod_spec</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#fecf17babbfd20e65dfb992ab39dd060"><span class="id" title="notation">^{1+2}</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#6d7462d9f1e45e8985bc5fef0096491d"><span class="id" title="notation">^{1+2*</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#6d7462d9f1e45e8985bc5fef0096491d"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#d5734ed590b969504e2a2cee2726792f"><span class="id" title="notation">^{1+2*</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#d5734ed590b969504e2a2cee2726792f"><span class="id" title="notation">}</span></a>%<span class="id" title="keyword">type</span>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="pX1p2S"><span class="id" title="lemma">pX1p2S</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.solvable.center.html#xcprod_spec"><span class="id" title="inductive">xcprod_spec</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#733630db88ea59f0786eda47f95f579b"><span class="id" title="notation">^{1+2}</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#1858156ab389b20f00955cf2f88b8d78"><span class="id" title="notation">^{1+2*</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#1858156ab389b20f00955cf2f88b8d78"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e83f70c26e2f0fabe22aa5af61f12478"><span class="id" title="notation">^{1+2*</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e83f70c26e2f0fabe22aa5af61f12478"><span class="id" title="notation">}</span></a>%<span class="id" title="keyword">type</span>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="card_pX1p2n"><span class="id" title="lemma">card_pX1p2n</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.prime.html#prime"><span class="id" title="definition">prime</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a7c316c84561ad9c93c7896226b3cab1"><span class="id" title="notation">^{1+2*</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a7c316c84561ad9c93c7896226b3cab1"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f460b977ac49dd1a229be682bc38c411"><span class="id" title="notation">.*2</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a>)%<span class="id" title="var">N</span>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="card_pX1p2n"><span class="id" title="lemma">card_pX1p2n</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.prime.html#prime"><span class="id" title="definition">prime</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#50748714e6bbf7d0964fc12c665fb268"><span class="id" title="notation">^{1+2*</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#50748714e6bbf7d0964fc12c665fb268"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="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.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#81fd94e251a61ee523cdd7855774ae7c"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bff172cdafaf4b86cefb300b16285e42"><span class="id" title="notation">.*2</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a>)%<span class="id" title="var">N</span>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="pX1p2n_pgroup"><span class="id" title="lemma">pX1p2n_pgroup</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.prime.html#prime"><span class="id" title="definition">prime</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a7c316c84561ad9c93c7896226b3cab1"><span class="id" title="notation">^{1+2*</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a7c316c84561ad9c93c7896226b3cab1"><span class="id" title="notation">}</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="pX1p2n_pgroup"><span class="id" title="lemma">pX1p2n_pgroup</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.prime.html#prime"><span class="id" title="definition">prime</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#15605b2ce8a0bd336aafa96c5cc1afdc"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#15605b2ce8a0bd336aafa96c5cc1afdc"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#50748714e6bbf7d0964fc12c665fb268"><span class="id" title="notation">^{1+2*</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#50748714e6bbf7d0964fc12c665fb268"><span class="id" title="notation">}</span></a>.<br/> <br/> </div> @@ -204,7 +203,7 @@ This is part of the existence half of Aschbacher (23.13) </div> <div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="exponent_pX1p2n"><span class="id" title="lemma">exponent_pX1p2n</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.prime.html#prime"><span class="id" title="definition">prime</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#odd"><span class="id" title="definition">odd</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.abelian.html#exponent"><span class="id" title="definition">exponent</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a7c316c84561ad9c93c7896226b3cab1"><span class="id" title="notation">^{1+2*</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a7c316c84561ad9c93c7896226b3cab1"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="exponent_pX1p2n"><span class="id" title="lemma">exponent_pX1p2n</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.prime.html#prime"><span class="id" title="definition">prime</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#odd"><span class="id" title="definition">odd</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.abelian.html#exponent"><span class="id" title="definition">exponent</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#50748714e6bbf7d0964fc12c665fb268"><span class="id" title="notation">^{1+2*</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#50748714e6bbf7d0964fc12c665fb268"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a>.<br/> <br/> </div> @@ -213,7 +212,7 @@ This is part of the existence half of Aschbacher (23.13) and (23.14) </div> <div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="pX1p2n_extraspecial"><span class="id" title="lemma">pX1p2n_extraspecial</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.prime.html#prime"><span class="id" title="definition">prime</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#19ab5cfd7e4f60fa14f22b576013bd96"><span class="id" title="notation">></span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.maximal.html#extraspecial"><span class="id" title="definition">extraspecial</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a7c316c84561ad9c93c7896226b3cab1"><span class="id" title="notation">^{1+2*</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a7c316c84561ad9c93c7896226b3cab1"><span class="id" title="notation">}</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="pX1p2n_extraspecial"><span class="id" title="lemma">pX1p2n_extraspecial</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.prime.html#prime"><span class="id" title="definition">prime</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#7f2a7ef2c63af7359b22787a9daf336e"><span class="id" title="notation">></span></a> 0 <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.maximal.html#extraspecial"><span class="id" title="definition">extraspecial</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#50748714e6bbf7d0964fc12c665fb268"><span class="id" title="notation">^{1+2*</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#50748714e6bbf7d0964fc12c665fb268"><span class="id" title="notation">}</span></a>.<br/> <br/> </div> @@ -222,16 +221,16 @@ This is Aschbacher (23.12) </div> <div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="Ohm1_extraspecial_odd"><span class="id" title="lemma">Ohm1_extraspecial_odd</span></a> (<span class="id" title="var">gT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) :<br/> - <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.maximal.html#extraspecial"><span class="id" title="definition">extraspecial</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#odd"><span class="id" title="definition">odd</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> - <span class="id" title="keyword">let</span> <span class="id" title="var">Y</span> := <a class="idref" href="mathcomp.solvable.abelian.html#c300ec465942bb74c9d0df0e983eeb01"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.abelian.html#c300ec465942bb74c9d0df0e983eeb01"><span class="id" title="notation">Ohm_1</span></a><a class="idref" href="mathcomp.solvable.abelian.html#c300ec465942bb74c9d0df0e983eeb01"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.abelian.html#c300ec465942bb74c9d0df0e983eeb01"><span class="id" title="notation">)</span></a> <span class="id" title="tactic">in</span><br/> - <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">[/\</span></a> <a class="idref" href="mathcomp.solvable.abelian.html#exponent"><span class="id" title="definition">exponent</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Y"><span class="id" title="variable">Y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Y"><span class="id" title="variable">Y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#aa34fd1c61c5cf0a3356b624a5d2afed"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Y"><span class="id" title="variable">Y</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">E</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ca13a32469ebe56c9f4cc99d00e8eeba"><span class="id" title="notation">[/\</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Y"><span class="id" title="variable">Y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ca13a32469ebe56c9f4cc99d00e8eeba"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#E"><span class="id" title="variable">E</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#7a45dffb109c3069e5c675be68643e60"><span class="id" title="notation">∨</span></a> <a class="idref" href="mathcomp.solvable.maximal.html#extraspecial"><span class="id" title="definition">extraspecial</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#E"><span class="id" title="variable">E</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ca13a32469ebe56c9f4cc99d00e8eeba"><span class="id" title="notation">,</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#fe60c20831f772c0c3c288abf68cc42a"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">X</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#fe60c20831f772c0c3c288abf68cc42a"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#fe60c20831f772c0c3c288abf68cc42a"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#X"><span class="id" title="variable">X</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#fe60c20831f772c0c3c288abf68cc42a"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#X"><span class="id" title="variable">X</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#3733c0e43956ad2062ab5f1e57ceb9a8"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.gproduct.html#3733c0e43956ad2062ab5f1e57ceb9a8"><span class="id" title="notation">x</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#E"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Y"><span class="id" title="variable">Y</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ca13a32469ebe56c9f4cc99d00e8eeba"><span class="id" title="notation">&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">M</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">[/\</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.extremal.html#cde820eeae6e659d7da1ef2161ef68ea"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extremal.html#cde820eeae6e659d7da1ef2161ef68ea"><span class="id" title="notation">Mod_</span></a><a class="idref" href="mathcomp.solvable.extremal.html#cde820eeae6e659d7da1ef2161ef68ea"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> 3<a class="idref" href="mathcomp.solvable.extremal.html#cde820eeae6e659d7da1ef2161ef68ea"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#9607c0b7b0a7e59f4327b220d5a93330"><span class="id" title="notation">\*</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#E"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#cb41714a5a23482f7a48a98975fa8c59"><span class="id" title="notation">:&:</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#E"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#M"><span class="id" title="variable">M</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ca13a32469ebe56c9f4cc99d00e8eeba"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="Ohm1_extraspecial_odd"><span class="id" title="lemma">Ohm1_extraspecial_odd</span></a> (<span class="id" title="var">gT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<span class="id" title="var">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.extraspecial.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.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#15605b2ce8a0bd336aafa96c5cc1afdc"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#15605b2ce8a0bd336aafa96c5cc1afdc"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.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.maximal.html#extraspecial"><span class="id" title="definition">extraspecial</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.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.ssreflect.ssrnat.html#odd"><span class="id" title="definition">odd</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> + <span class="id" title="keyword">let</span> <span class="id" title="var">Y</span> := <a class="idref" href="mathcomp.solvable.abelian.html#c56ec4cf607c781766b0d2cf7a260ba8"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.abelian.html#c56ec4cf607c781766b0d2cf7a260ba8"><span class="id" title="notation">Ohm_1</span></a><a class="idref" href="mathcomp.solvable.abelian.html#c56ec4cf607c781766b0d2cf7a260ba8"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.abelian.html#c56ec4cf607c781766b0d2cf7a260ba8"><span class="id" title="notation">)</span></a> <span class="id" title="tactic">in</span><br/> + <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.abelian.html#exponent"><span class="id" title="definition">exponent</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Y"><span class="id" title="variable">Y</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.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Y"><span class="id" title="variable">Y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#bde82eab2fe4a0799bc2419e587505d4"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><br/> + <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.extraspecial.html#Y"><span class="id" title="variable">Y</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.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#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <span class="id" title="var">E</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.extraspecial.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><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#554fc3f3cf0a27fe0863b7741d119014"><span class="id" title="notation">[/\</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Y"><span class="id" title="variable">Y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#554fc3f3cf0a27fe0863b7741d119014"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#E"><span class="id" title="variable">E</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#f031fe1957c4a4a8e217aa46af2b4e25"><span class="id" title="notation">∨</span></a> <a class="idref" href="mathcomp.solvable.maximal.html#extraspecial"><span class="id" title="definition">extraspecial</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#E"><span class="id" title="variable">E</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#554fc3f3cf0a27fe0863b7741d119014"><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#59ba2b47d2814e66f8210a649ae6e6bc"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">X</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.extraspecial.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#59ba2b47d2814e66f8210a649ae6e6bc"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#X"><span class="id" title="variable">X</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#59ba2b47d2814e66f8210a649ae6e6bc"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#X"><span class="id" title="variable">X</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#191b5570f070a51bd5c860222c206828"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.gproduct.html#191b5570f070a51bd5c860222c206828"><span class="id" title="notation">x</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#E"><span class="id" title="variable">E</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.extraspecial.html#Y"><span class="id" title="variable">Y</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#554fc3f3cf0a27fe0863b7741d119014"><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">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.extraspecial.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><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#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">[/\</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#M"><span class="id" title="variable">M</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.extremal.html#c2d446c30f0f14edd1423d2a23612932"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extremal.html#c2d446c30f0f14edd1423d2a23612932"><span class="id" title="notation">Mod_</span></a><a class="idref" href="mathcomp.solvable.extremal.html#c2d446c30f0f14edd1423d2a23612932"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#81fd94e251a61ee523cdd7855774ae7c"><span class="id" title="notation">^</span></a> 3<a class="idref" href="mathcomp.solvable.extremal.html#c2d446c30f0f14edd1423d2a23612932"><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.extraspecial.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#1c2e0971edf6e9b6c6dd4a5951d04f36"><span class="id" title="notation">\*</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#E"><span class="id" title="variable">E</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.extraspecial.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.extraspecial.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#b9596739b058766532fc6517a36fef9f"><span class="id" title="notation">:&:</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#E"><span class="id" title="variable">E</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.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.extraspecial.html#M"><span class="id" title="variable">M</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.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.ssr.ssrbool.html#554fc3f3cf0a27fe0863b7741d119014"><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>.<br/> <br/> </div> @@ -241,27 +240,27 @@ in part the proof that symplectic spaces are hyperbolic (19.16). </div> <div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="isog_pX1p2n"><span class="id" title="lemma">isog_pX1p2n</span></a> <span class="id" title="var">n</span> (<span class="id" title="var">gT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) :<br/> - <a class="idref" href="mathcomp.ssreflect.prime.html#prime"><span class="id" title="definition">prime</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.maximal.html#extraspecial"><span class="id" title="definition">extraspecial</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f460b977ac49dd1a229be682bc38c411"><span class="id" title="notation">.*2</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a>)%<span class="id" title="var">N</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.abelian.html#exponent"><span class="id" title="definition">exponent</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#aa34fd1c61c5cf0a3356b624a5d2afed"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a7c316c84561ad9c93c7896226b3cab1"><span class="id" title="notation">^{1+2*</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a7c316c84561ad9c93c7896226b3cab1"><span class="id" title="notation">}</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="isog_pX1p2n"><span class="id" title="lemma">isog_pX1p2n</span></a> <span class="id" title="var">n</span> (<span class="id" title="var">gT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<span class="id" title="var">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.extraspecial.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.ssreflect.prime.html#prime"><span class="id" title="definition">prime</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.maximal.html#extraspecial"><span class="id" title="definition">extraspecial</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.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.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> (<a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#81fd94e251a61ee523cdd7855774ae7c"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bff172cdafaf4b86cefb300b16285e42"><span class="id" title="notation">.*2</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a>)%<span class="id" title="var">N</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.abelian.html#exponent"><span class="id" title="definition">exponent</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#bde82eab2fe4a0799bc2419e587505d4"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.solvable.extraspecial.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.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#50748714e6bbf7d0964fc12c665fb268"><span class="id" title="notation">^{1+2*</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#50748714e6bbf7d0964fc12c665fb268"><span class="id" title="notation">}</span></a>.<br/> <br/> <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory"><span class="id" title="section">GeneralExponentPextraspecialTheory</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="isog_2X1p2"><span class="id" title="lemma">isog_2X1p2</span></a> : 2<a class="idref" href="mathcomp.solvable.extraspecial.html#354a7719245e28a5f784cfb19c81f53a"><span class="id" title="notation">^{1+2}</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.extremal.html#114753a05fa1a4c728fd6c58cce9f74c"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extremal.html#114753a05fa1a4c728fd6c58cce9f74c"><span class="id" title="notation">D_8</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="isog_2X1p2"><span class="id" title="lemma">isog_2X1p2</span></a> : 2<a class="idref" href="mathcomp.solvable.extraspecial.html#13d1250ec3fb36839cafb80c8df79307"><span class="id" title="notation">^{1+2}</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.extremal.html#eda4b377edf33c7306089a3c2ef64a9a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extremal.html#eda4b377edf33c7306089a3c2ef64a9a"><span class="id" title="notation">D_8</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="Q8_extraspecial"><span class="id" title="lemma">Q8_extraspecial</span></a> : <a class="idref" href="mathcomp.solvable.maximal.html#extraspecial"><span class="id" title="definition">extraspecial</span></a> <a class="idref" href="mathcomp.solvable.extremal.html#7a3ab294f809847ed7e277c085de5f5d"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extremal.html#7a3ab294f809847ed7e277c085de5f5d"><span class="id" title="notation">Q_8</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="Q8_extraspecial"><span class="id" title="lemma">Q8_extraspecial</span></a> : <a class="idref" href="mathcomp.solvable.maximal.html#extraspecial"><span class="id" title="definition">extraspecial</span></a> <a class="idref" href="mathcomp.solvable.extremal.html#85cb21871fd18e66dbfa2ee4bffbe55c"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extremal.html#85cb21871fd18e66dbfa2ee4bffbe55c"><span class="id" title="notation">Q_8</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="DnQ_P"><span class="id" title="lemma">DnQ_P</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.solvable.center.html#xcprod_spec"><span class="id" title="inductive">xcprod_spec</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#11fb2c38b9f35b58f4576164683416e2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#11fb2c38b9f35b58f4576164683416e2"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#11fb2c38b9f35b58f4576164683416e2"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.solvable.extremal.html#24d327e6c4148d6dd7b561fa4e1277bd"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extremal.html#24d327e6c4148d6dd7b561fa4e1277bd"><span class="id" title="notation">Q_8</span></a> (<a class="idref" href="mathcomp.solvable.extraspecial.html#060cb01c343ba334280fa026c9b5c80b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#060cb01c343ba334280fa026c9b5c80b"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#060cb01c343ba334280fa026c9b5c80b"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#060cb01c343ba334280fa026c9b5c80b"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#060cb01c343ba334280fa026c9b5c80b"><span class="id" title="notation">Q</span></a>)%<span class="id" title="keyword">type</span>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="DnQ_P"><span class="id" title="lemma">DnQ_P</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.solvable.center.html#xcprod_spec"><span class="id" title="inductive">xcprod_spec</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#85fbcdd7ed3c17a1a9687625c1366d82"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#85fbcdd7ed3c17a1a9687625c1366d82"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#85fbcdd7ed3c17a1a9687625c1366d82"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.solvable.extremal.html#de4614b692797c6dc4c82a4b56748090"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extremal.html#de4614b692797c6dc4c82a4b56748090"><span class="id" title="notation">Q_8</span></a> (<a class="idref" href="mathcomp.solvable.extraspecial.html#5ae1a9e1f84a4c1cf90fc959c1b39206"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#5ae1a9e1f84a4c1cf90fc959c1b39206"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#5ae1a9e1f84a4c1cf90fc959c1b39206"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#5ae1a9e1f84a4c1cf90fc959c1b39206"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#5ae1a9e1f84a4c1cf90fc959c1b39206"><span class="id" title="notation">Q</span></a>)%<span class="id" title="keyword">type</span>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="card_DnQ"><span class="id" title="lemma">card_DnQ</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">Q</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (2 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f460b977ac49dd1a229be682bc38c411"><span class="id" title="notation">.*2</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a>)%<span class="id" title="var">N</span>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="card_DnQ"><span class="id" title="lemma">card_DnQ</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#7c4503382583a2ccddcad8489a0e4194"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#7c4503382583a2ccddcad8489a0e4194"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#7c4503382583a2ccddcad8489a0e4194"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#7c4503382583a2ccddcad8489a0e4194"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#7c4503382583a2ccddcad8489a0e4194"><span class="id" title="notation">Q</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> (2 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#81fd94e251a61ee523cdd7855774ae7c"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bff172cdafaf4b86cefb300b16285e42"><span class="id" title="notation">.*2</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a>)%<span class="id" title="var">N</span>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="DnQ_pgroup"><span class="id" title="lemma">DnQ_pgroup</span></a> <span class="id" title="var">n</span> : 2<a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">Q</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="DnQ_pgroup"><span class="id" title="lemma">DnQ_pgroup</span></a> <span class="id" title="var">n</span> : 2<a class="idref" href="mathcomp.solvable.pgroup.html#15605b2ce8a0bd336aafa96c5cc1afdc"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#15605b2ce8a0bd336aafa96c5cc1afdc"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#7c4503382583a2ccddcad8489a0e4194"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#7c4503382583a2ccddcad8489a0e4194"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#7c4503382583a2ccddcad8489a0e4194"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#7c4503382583a2ccddcad8489a0e4194"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#7c4503382583a2ccddcad8489a0e4194"><span class="id" title="notation">Q</span></a>.<br/> <br/> </div> @@ -270,7 +269,7 @@ Final part of the existence half of Aschbacher (23.14). </div> <div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="DnQ_extraspecial"><span class="id" title="lemma">DnQ_extraspecial</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.solvable.maximal.html#extraspecial"><span class="id" title="definition">extraspecial</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">Q</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="DnQ_extraspecial"><span class="id" title="lemma">DnQ_extraspecial</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.solvable.maximal.html#extraspecial"><span class="id" title="definition">extraspecial</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#7c4503382583a2ccddcad8489a0e4194"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#7c4503382583a2ccddcad8489a0e4194"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#7c4503382583a2ccddcad8489a0e4194"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#7c4503382583a2ccddcad8489a0e4194"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#7c4503382583a2ccddcad8489a0e4194"><span class="id" title="notation">Q</span></a>.<br/> <br/> </div> @@ -279,8 +278,8 @@ A special case of the uniqueness half of Achsbacher (23.14). </div> <div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="card_isog8_extraspecial"><span class="id" title="lemma">card_isog8_extraspecial</span></a> (<span class="id" title="var">gT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) :<br/> - <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 8 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.maximal.html#extraspecial"><span class="id" title="definition">extraspecial</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.extremal.html#114753a05fa1a4c728fd6c58cce9f74c"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extremal.html#114753a05fa1a4c728fd6c58cce9f74c"><span class="id" title="notation">D_8</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">||</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.extremal.html#7a3ab294f809847ed7e277c085de5f5d"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extremal.html#7a3ab294f809847ed7e277c085de5f5d"><span class="id" title="notation">Q_8</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">)</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="card_isog8_extraspecial"><span class="id" title="lemma">card_isog8_extraspecial</span></a> (<span class="id" title="var">gT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<span class="id" title="var">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.extraspecial.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.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 8 <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.maximal.html#extraspecial"><span class="id" title="definition">extraspecial</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.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.Datatypes.html#081ff67d3116402bb680e8692aa39185"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.extraspecial.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.extremal.html#eda4b377edf33c7306089a3c2ef64a9a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extremal.html#eda4b377edf33c7306089a3c2ef64a9a"><span class="id" title="notation">D_8</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="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.extraspecial.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.extremal.html#85cb21871fd18e66dbfa2ee4bffbe55c"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extremal.html#85cb21871fd18e66dbfa2ee4bffbe55c"><span class="id" title="notation">Q_8</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>.<br/> <br/> </div> @@ -293,8 +292,8 @@ Galois theory as in (20.9) and (21.1). </div> <div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="isog_2extraspecial"><span class="id" title="lemma">isog_2extraspecial</span></a> (<span class="id" title="var">gT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) <span class="id" title="var">n</span> :<br/> - <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (2 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f460b977ac49dd1a229be682bc38c411"><span class="id" title="notation">.*2</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a>)%<span class="id" title="var">N</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.maximal.html#extraspecial"><span class="id" title="definition">extraspecial</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#a8a830ccefaf9cb4d4b2f49d65e5334b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a8a830ccefaf9cb4d4b2f49d65e5334b"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a8a830ccefaf9cb4d4b2f49d65e5334b"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#7a45dffb109c3069e5c675be68643e60"><span class="id" title="notation">∨</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><span class="id" title="notation">.-1</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">Q</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="isog_2extraspecial"><span class="id" title="lemma">isog_2extraspecial</span></a> (<span class="id" title="var">gT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<span class="id" title="var">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.extraspecial.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">n</span> :<br/> + <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> (2 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#81fd94e251a61ee523cdd7855774ae7c"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bff172cdafaf4b86cefb300b16285e42"><span class="id" title="notation">.*2</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a>)%<span class="id" title="var">N</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.maximal.html#extraspecial"><span class="id" title="definition">extraspecial</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.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.extraspecial.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.extraspecial.html#7aef83b7aca71eca9cb3114e50804f53"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#7aef83b7aca71eca9cb3114e50804f53"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#7aef83b7aca71eca9cb3114e50804f53"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#f031fe1957c4a4a8e217aa46af2b4e25"><span class="id" title="notation">∨</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.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.extraspecial.html#7c4503382583a2ccddcad8489a0e4194"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#7c4503382583a2ccddcad8489a0e4194"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#7c4503382583a2ccddcad8489a0e4194"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f953bf7095e0da1cb644443fd0e17d6d"><span class="id" title="notation">.-1</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#7c4503382583a2ccddcad8489a0e4194"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#7c4503382583a2ccddcad8489a0e4194"><span class="id" title="notation">Q</span></a>.<br/> <br/> </div> @@ -303,7 +302,7 @@ The first concluding remark of Aschbacher (23.14). </div> <div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="rank_Dn"><span class="id" title="lemma">rank_Dn</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.solvable.abelian.html#2e018390d4609ecf460bceadff549bb3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.abelian.html#2e018390d4609ecf460bceadff549bb3"><span class="id" title="notation">r_2</span></a><a class="idref" href="mathcomp.solvable.abelian.html#2e018390d4609ecf460bceadff549bb3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a8a830ccefaf9cb4d4b2f49d65e5334b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a8a830ccefaf9cb4d4b2f49d65e5334b"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a8a830ccefaf9cb4d4b2f49d65e5334b"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.abelian.html#2e018390d4609ecf460bceadff549bb3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="rank_Dn"><span class="id" title="lemma">rank_Dn</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.solvable.abelian.html#6b61dcfb093dfe93d87341f88d96ca9f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.abelian.html#6b61dcfb093dfe93d87341f88d96ca9f"><span class="id" title="notation">r_2</span></a><a class="idref" href="mathcomp.solvable.abelian.html#6b61dcfb093dfe93d87341f88d96ca9f"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#7aef83b7aca71eca9cb3114e50804f53"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#7aef83b7aca71eca9cb3114e50804f53"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#7aef83b7aca71eca9cb3114e50804f53"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.abelian.html#6b61dcfb093dfe93d87341f88d96ca9f"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a>.<br/> <br/> </div> @@ -312,7 +311,7 @@ The second concluding remark of Aschbacher (23.14). </div> <div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="rank_DnQ"><span class="id" title="lemma">rank_DnQ</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.solvable.abelian.html#2e018390d4609ecf460bceadff549bb3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.abelian.html#2e018390d4609ecf460bceadff549bb3"><span class="id" title="notation">r_2</span></a><a class="idref" href="mathcomp.solvable.abelian.html#2e018390d4609ecf460bceadff549bb3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">Q</span></a><a class="idref" href="mathcomp.solvable.abelian.html#2e018390d4609ecf460bceadff549bb3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="rank_DnQ"><span class="id" title="lemma">rank_DnQ</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.solvable.abelian.html#6b61dcfb093dfe93d87341f88d96ca9f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.abelian.html#6b61dcfb093dfe93d87341f88d96ca9f"><span class="id" title="notation">r_2</span></a><a class="idref" href="mathcomp.solvable.abelian.html#6b61dcfb093dfe93d87341f88d96ca9f"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#7c4503382583a2ccddcad8489a0e4194"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#7c4503382583a2ccddcad8489a0e4194"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#7c4503382583a2ccddcad8489a0e4194"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#7c4503382583a2ccddcad8489a0e4194"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#7c4503382583a2ccddcad8489a0e4194"><span class="id" title="notation">Q</span></a><a class="idref" href="mathcomp.solvable.abelian.html#6b61dcfb093dfe93d87341f88d96ca9f"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a>.<br/> <br/> </div> @@ -321,7 +320,7 @@ The final concluding remark of Aschbacher (23.14). </div> <div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="not_isog_Dn_DnQ"><span class="id" title="lemma">not_isog_Dn_DnQ</span></a> <span class="id" title="var">n</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">~~</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a8a830ccefaf9cb4d4b2f49d65e5334b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a8a830ccefaf9cb4d4b2f49d65e5334b"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a8a830ccefaf9cb4d4b2f49d65e5334b"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><span class="id" title="notation">.-1</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">Q</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">)</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="not_isog_Dn_DnQ"><span class="id" title="lemma">not_isog_Dn_DnQ</span></a> <span class="id" title="var">n</span> : <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.extraspecial.html#7aef83b7aca71eca9cb3114e50804f53"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#7aef83b7aca71eca9cb3114e50804f53"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#7aef83b7aca71eca9cb3114e50804f53"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</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.extraspecial.html#7c4503382583a2ccddcad8489a0e4194"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#7c4503382583a2ccddcad8489a0e4194"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#7c4503382583a2ccddcad8489a0e4194"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f953bf7095e0da1cb644443fd0e17d6d"><span class="id" title="notation">.-1</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#7c4503382583a2ccddcad8489a0e4194"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#7c4503382583a2ccddcad8489a0e4194"><span class="id" title="notation">Q</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>.<br/> </div> </div> |