diff options
| author | Cyril Cohen | 2019-10-16 11:26:43 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2019-10-16 11:26:43 +0200 |
| commit | 6b59540a2460633df4e3d8347cb4dfe2fb3a3afb (patch) | |
| tree | 1239c1d5553d51a7d73f2f8b465f6a23178ff8a0 /docs/htmldoc/mathcomp.solvable.extraspecial.html | |
| parent | dd82aaeae7e9478efc178ce8430986649555b032 (diff) | |
removing everything but index which redirects to the new page
Diffstat (limited to 'docs/htmldoc/mathcomp.solvable.extraspecial.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.solvable.extraspecial.html | 334 |
1 files changed, 0 insertions, 334 deletions
diff --git a/docs/htmldoc/mathcomp.solvable.extraspecial.html b/docs/htmldoc/mathcomp.solvable.extraspecial.html deleted file mode 100644 index c0f4274..0000000 --- a/docs/htmldoc/mathcomp.solvable.extraspecial.html +++ /dev/null @@ -1,334 +0,0 @@ -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" -"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> -<html xmlns="http://www.w3.org/1999/xhtml"> -<head> -<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> -<link href="coqdoc.css" rel="stylesheet" type="text/css" /> -<title>mathcomp.solvable.extraspecial</title> -</head> - -<body> - -<div id="page"> - -<div id="header"> -</div> - -<div id="main"> - -<h1 class="libtitle">Library mathcomp.solvable.extraspecial</h1> - -<div class="code"> -<span class="comment">(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. <br/> - Distributed under the terms of CeCILL-B. *)</span><br/> - -<br/> -</div> - -<div class="doc"> - This file contains the fine structure thorems for extraspecial p-groups. - Together with the material in the maximal and extremal libraries, it - completes the coverage of Aschbacher, section 23. - We define canonical representatives for the group classes that cover the - extremal p-groups (non-abelian p-groups with a cyclic maximal subgroup): - 'Mod_m == the modular group of order m, for m = p ^ n, p prime and n >= 3. - 'D_m == the dihedral group of order m, for m = 2n >= 4. - 'Q_m == the generalized quaternion group of order m, for q = 2 ^ n >= 8. - 'SD_m == the semi-dihedral group of order m, for m = 2 ^ n >= 16. - In each case the notation is defined in the %type, %g and %G scopes, where - it denotes a finGroupType, a full gset and the full group for that type. - However each notation is only meaningful under the given conditions, in - We construct and study the following extraspecial groups: - p^{1+2} == if p is prime, an extraspecial group of order p^3 that has - exponent p or 4, and p-rank 2: thus p^{1+2} is isomorphic to - 'D_8 if p - 2, and NOT isomorphic to 'Mod(p^3) if p is odd. - p^{1+2*n} == the central product of n copies of p^{1+2}, thus of order - p^(1+2*n) if p is a prime, and, when n > 0, a representative - of the (unique) isomorphism class of extraspecial groups of - order p^(1+2*n), of exponent p or 4, and p-rank n+1. - 'D^n == an alternative (and preferred) notation for 2^{1+2*n}, which - is isomorphic to the central product of n copies od 'D_8. - 'D^n*Q == the central product of 'D^n with 'Q_8, thus isomorphic to - all extraspecial groups of order 2 ^ (2 * n + 3) that are - not isomorphic to 'D^n.+1 (or, equivalently, have 2-rank n). - As in extremal.v, these notations are simultaneously defined in the %type, - %g and %G scopes -- depending on the syntactic context, they denote either - a finGroupType, the set, or the group of all its elements. -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Set Implicit Arguments</span>.<br/> - -<br/> -<span class="id" title="keyword">Local Open</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">ring_scope</span>.<br/> -<span class="id" title="keyword">Import</span> <span class="id" title="var">GroupScope</span> <span class="id" title="var">GRing.Theory</span>.<br/> - -<br/> -<span class="id" title="keyword">Reserved Notation</span> "p ^{1+2}" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">format</span> "p ^{1+2}").<br/> -<span class="id" title="keyword">Reserved Notation</span> "p ^{1+2* n }"<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">n</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">format</span> "p ^{1+2* n }").<br/> -<span class="id" title="keyword">Reserved Notation</span> "''D^' n" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8, <span class="id" title="var">n</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">format</span> "''D^' n").<br/> -<span class="id" title="keyword">Reserved Notation</span> "''D^' n * 'Q'"<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8, <span class="id" title="var">n</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">format</span> "''D^' n * 'Q'").<br/> - -<br/> -<span class="id" title="keyword">Module</span> <a name="Pextraspecial"><span class="id" title="module">Pextraspecial</span></a>.<br/> - -<br/> -<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/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#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#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/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#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#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="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="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="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="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/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/> - -<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#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#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#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> - -<div class="doc"> - 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#13d1250ec3fb36839cafb80c8df79307"><span class="id" title="notation">^{1+2}</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - 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/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> - -<div class="doc"> - 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#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/> - -<br/> -<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/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#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#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/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/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> - -<div class="doc"> - 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/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> - -<div class="doc"> - 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/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> - -<div class="doc"> - 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#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> - -<div class="doc"> - This is the uniqueness half of Aschbacher (23.13); the proof incorporates - 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#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#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#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#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#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#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> - -<div class="doc"> - 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#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> - -<div class="doc"> - 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#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> - -<div class="doc"> - The uniqueness half of Achsbacher (23.14). The proof incorporates in part - the proof that symplectic spces are hyperbolic (Aschbacher (19.16)), and - the determination of quadratic spaces over 'F_2 (21.2); however we use - the second part of exercise (8.4) to avoid resorting to Witt's lemma and - 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#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> - -<div class="doc"> - 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#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> - -<div class="doc"> - 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#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> - -<div class="doc"> - 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/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> - -<div id="footer"> -<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a> -</div> - -</div> - -</body> -</html>
\ No newline at end of file |