diff options
| author | Enrico Tassi | 2018-04-20 10:54:22 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-04-20 10:54:22 +0200 |
| commit | ed05182cece6bb3706e09b2ce14af4a41a2e8141 (patch) | |
| tree | e850d7314b6372d0476cf2ffaf7d3830721db7b1 /docs/htmldoc/mathcomp.solvable.extraspecial.html | |
| parent | 3d196f44681fb3b23ff8a79fbd44e12308680531 (diff) | |
generate the documentation for 1.7
Diffstat (limited to 'docs/htmldoc/mathcomp.solvable.extraspecial.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.solvable.extraspecial.html | 335 |
1 files changed, 335 insertions, 0 deletions
diff --git a/docs/htmldoc/mathcomp.solvable.extraspecial.html b/docs/htmldoc/mathcomp.solvable.extraspecial.html new file mode 100644 index 0000000..4e8e995 --- /dev/null +++ b/docs/htmldoc/mathcomp.solvable.extraspecial.html @@ -0,0 +1,335 @@ +<!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/> +<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#"><span class="id" title="library">mathcomp.ssreflect.ssreflect</span></a>.<br/> + +<br/> +</div> + +<div class="doc"> + This 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/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="Pextraspecial.act"><span class="id" title="definition">act</span></a> <span class="id" title="var">ij</span> (<span class="id" title="var">k</span> : <a class="idref" href="mathcomp.algebra.zmodp.html#9daeb9ead3dc7cfd1f9338b8de9c8c09"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#9daeb9ead3dc7cfd1f9338b8de9c8c09"><span class="id" title="notation">Z_p</span></a>) := <span class="id" title="keyword">let</span>: <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <span class="id" title="var">j</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a> := <a class="idref" href="mathcomp.solvable.extraspecial.html#ij"><span class="id" title="variable">ij</span></a> <span class="id" title="tactic">in</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.algebra.ssralg.html#ae4d81913e6239182a9ac7467ffde8cd"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <span class="id" title="var">j</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <span class="id" title="var">j</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="Pextraspecial.actP"><span class="id" title="lemma">actP</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#is_action"><span class="id" title="definition">is_action</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#9daeb9ead3dc7cfd1f9338b8de9c8c09"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#9daeb9ead3dc7cfd1f9338b8de9c8c09"><span class="id" title="notation">Z_p</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Pextraspecial.act"><span class="id" title="definition">act</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">action</span> := <a class="idref" href="mathcomp.fingroup.action.html#Action"><span class="id" title="constructor">Action</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Pextraspecial.actP"><span class="id" title="lemma">actP</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Pextraspecial.gactP"><span class="id" title="lemma">gactP</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#is_groupAction"><span class="id" title="definition">is_groupAction</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#9daeb9ead3dc7cfd1f9338b8de9c8c09"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#9daeb9ead3dc7cfd1f9338b8de9c8c09"><span class="id" title="notation">Z_p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.zmodp.html#9daeb9ead3dc7cfd1f9338b8de9c8c09"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.zmodp.html#9daeb9ead3dc7cfd1f9338b8de9c8c09"><span class="id" title="notation">Z_p</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Pextraspecial.action"><span class="id" title="definition">action</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="Pextraspecial.groupAction"><span class="id" title="definition">groupAction</span></a> := <a class="idref" href="mathcomp.fingroup.action.html#GroupAction"><span class="id" title="constructor">GroupAction</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Pextraspecial.gactP"><span class="id" title="lemma">gactP</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Fact</span> <a name="Pextraspecial.gtype_key"><span class="id" title="lemma">gtype_key</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a>. <br/> +<span class="id" title="keyword">Definition</span> <a name="Pextraspecial.gtype"><span class="id" title="definition">gtype</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#locked_with"><span class="id" title="definition">locked_with</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Pextraspecial.gtype_key"><span class="id" title="lemma">gtype_key</span></a> (<a class="idref" href="mathcomp.fingroup.gproduct.html#sdprod_groupType"><span class="id" title="definition">sdprod_groupType</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Pextraspecial.groupAction"><span class="id" title="definition">groupAction</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="Pextraspecial.ngtype"><span class="id" title="definition">ngtype</span></a> := <a class="idref" href="mathcomp.solvable.center.html#ncprod"><span class="id" title="definition">ncprod</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Pextraspecial.gtype"><span class="id" title="definition">gtype</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.extraspecial.html#Pextraspecial.Construction"><span class="id" title="section">Construction</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="Pextraspecial.ngtypeQ"><span class="id" title="definition">ngtypeQ</span></a> <span class="id" title="var">n</span> := <a class="idref" href="mathcomp.solvable.center.html#xcprod"><span class="id" title="definition">xcprod</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Pextraspecial.ngtype"><span class="id" title="definition">ngtype</span></a> 2 <a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.solvable.extremal.html#24d327e6c4148d6dd7b561fa4e1277bd"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extremal.html#24d327e6c4148d6dd7b561fa4e1277bd"><span class="id" title="notation">Q_8</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.extraspecial.html#Pextraspecial"><span class="id" title="module">Pextraspecial</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="4930a1d10a5aad7b22b82525a70cd4ea"><span class="id" title="notation">"</span></a>p ^{1+2}" := (<a class="idref" href="mathcomp.solvable.extraspecial.html#gtype"><span class="id" title="definition">Pextraspecial.gtype</span></a> <span class="id" title="var">p</span>) : <span class="id" title="var">type_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="354a7719245e28a5f784cfb19c81f53a"><span class="id" title="notation">"</span></a>p ^{1+2}" := <a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#gsort"><span class="id" title="abbreviation">gsort</span></a> <span class="id" title="var">p</span><a class="idref" href="mathcomp.solvable.extraspecial.html#4930a1d10a5aad7b22b82525a70cd4ea"><span class="id" title="notation">^{1+2}</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">]</span></a> : <span class="id" title="var">group_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="fecf17babbfd20e65dfb992ab39dd060"><span class="id" title="notation">"</span></a>p ^{1+2}" := <a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#gsort"><span class="id" title="abbreviation">gsort</span></a> <span class="id" title="var">p</span><a class="idref" href="mathcomp.solvable.extraspecial.html#4930a1d10a5aad7b22b82525a70cd4ea"><span class="id" title="notation">^{1+2}</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">]</span></a>%<span class="id" title="var">G</span> : <span class="id" title="var">Group_scope</span>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="d5734ed590b969504e2a2cee2726792f"><span class="id" title="notation">"</span></a>p ^{1+2* n }" := (<a class="idref" href="mathcomp.solvable.extraspecial.html#ngtype"><span class="id" title="definition">Pextraspecial.ngtype</span></a> <span class="id" title="var">p</span> <span class="id" title="var">n</span>) : <span class="id" title="var">type_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="a7c316c84561ad9c93c7896226b3cab1"><span class="id" title="notation">"</span></a>p ^{1+2* n }" := <a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#gsort"><span class="id" title="abbreviation">gsort</span></a> <span class="id" title="var">p</span><a class="idref" href="mathcomp.solvable.extraspecial.html#d5734ed590b969504e2a2cee2726792f"><span class="id" title="notation">^{1+2*</span></a><span class="id" title="var">n</span><a class="idref" href="mathcomp.solvable.extraspecial.html#d5734ed590b969504e2a2cee2726792f"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">]</span></a> : <span class="id" title="var">group_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="6d7462d9f1e45e8985bc5fef0096491d"><span class="id" title="notation">"</span></a>p ^{1+2* n }" := <a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#gsort"><span class="id" title="abbreviation">gsort</span></a> <span class="id" title="var">p</span><a class="idref" href="mathcomp.solvable.extraspecial.html#d5734ed590b969504e2a2cee2726792f"><span class="id" title="notation">^{1+2*</span></a><span class="id" title="var">n</span><a class="idref" href="mathcomp.solvable.extraspecial.html#d5734ed590b969504e2a2cee2726792f"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">]</span></a>%<span class="id" title="var">G</span> : <span class="id" title="var">Group_scope</span>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="ba80690771cb8385c9d31dd9f3c06f59"><span class="id" title="notation">"</span></a>''D^' n" := (<a class="idref" href="mathcomp.solvable.extraspecial.html#ngtype"><span class="id" title="definition">Pextraspecial.ngtype</span></a> 2 <span class="id" title="var">n</span>) : <span class="id" title="var">type_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="a8a830ccefaf9cb4d4b2f49d65e5334b"><span class="id" title="notation">"</span></a>''D^' n" := <a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#gsort"><span class="id" title="abbreviation">gsort</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#ba80690771cb8385c9d31dd9f3c06f59"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#ba80690771cb8385c9d31dd9f3c06f59"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#ba80690771cb8385c9d31dd9f3c06f59"><span class="id" title="notation">^</span></a><span class="id" title="var">n</span><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">]</span></a> : <span class="id" title="var">group_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="11fb2c38b9f35b58f4576164683416e2"><span class="id" title="notation">"</span></a>''D^' n" := <a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#gsort"><span class="id" title="abbreviation">gsort</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#ba80690771cb8385c9d31dd9f3c06f59"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#ba80690771cb8385c9d31dd9f3c06f59"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#ba80690771cb8385c9d31dd9f3c06f59"><span class="id" title="notation">^</span></a><span class="id" title="var">n</span><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">]</span></a>%<span class="id" title="var">G</span> : <span class="id" title="var">Group_scope</span>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="060cb01c343ba334280fa026c9b5c80b"><span class="id" title="notation">"</span></a>''D^' n * 'Q'" := (<a class="idref" href="mathcomp.solvable.extraspecial.html#ngtypeQ"><span class="id" title="definition">Pextraspecial.ngtypeQ</span></a> <span class="id" title="var">n</span>) : <span class="id" title="var">type_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">"</span></a>''D^' n * 'Q'" := <a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#gsort"><span class="id" title="abbreviation">gsort</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#060cb01c343ba334280fa026c9b5c80b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#060cb01c343ba334280fa026c9b5c80b"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#060cb01c343ba334280fa026c9b5c80b"><span class="id" title="notation">^</span></a><span class="id" title="var">n</span><a class="idref" href="mathcomp.solvable.extraspecial.html#060cb01c343ba334280fa026c9b5c80b"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#060cb01c343ba334280fa026c9b5c80b"><span class="id" title="notation">Q</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">]</span></a> : <span class="id" title="var">group_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="802dab5ec0a31aa7f85d95659b7db935"><span class="id" title="notation">"</span></a>''D^' n * 'Q'" := <a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#gsort"><span class="id" title="abbreviation">gsort</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#060cb01c343ba334280fa026c9b5c80b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#060cb01c343ba334280fa026c9b5c80b"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#060cb01c343ba334280fa026c9b5c80b"><span class="id" title="notation">^</span></a><span class="id" title="var">n</span><a class="idref" href="mathcomp.solvable.extraspecial.html#060cb01c343ba334280fa026c9b5c80b"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#060cb01c343ba334280fa026c9b5c80b"><span class="id" title="notation">Q</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">]</span></a>%<span class="id" title="var">G</span> : <span class="id" title="var">Group_scope</span>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="ExponentPextraspecialTheory"><span class="id" title="section">ExponentPextraspecialTheory</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variable</span> <a name="ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> +<span class="id" title="keyword">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#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#354a7719245e28a5f784cfb19c81f53a"><span class="id" title="notation">^{1+2}</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> 3)%<span class="id" title="var">N</span>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Grp_pX1p2"><span class="id" title="lemma">Grp_pX1p2</span></a> :<br/> + <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#354a7719245e28a5f784cfb19c81f53a"><span class="id" title="notation">^{1+2}</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#2e7e6fdc2fcc257cb8670b6b97d9b9ee"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#2e7e6fdc2fcc257cb8670b6b97d9b9ee"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#2e7e6fdc2fcc257cb8670b6b97d9b9ee"><span class="id" title="notation">Grp</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#2e7e6fdc2fcc257cb8670b6b97d9b9ee"><span class="id" title="notation">(</span></a><span class="id" title="var">x</span> <a class="idref" href="mathcomp.fingroup.presentation.html#2e7e6fdc2fcc257cb8670b6b97d9b9ee"><span class="id" title="notation">:</span></a> <span class="id" title="var">y</span> <a class="idref" href="mathcomp.fingroup.presentation.html#953d1fbe50819ac104ff2928ed9f1f35"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#5b8f67ffc457596b97fe80b0e075accd"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#93f82d9635dc31e1d0b435f42eb3dc73"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#5b8f67ffc457596b97fe80b0e075accd"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#93f82d9635dc31e1d0b435f42eb3dc73"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#5b8f67ffc457596b97fe80b0e075accd"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#a0040f72df5ea25d5ed5fbb0e00c50b5"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#a0040f72df5ea25d5ed5fbb0e00c50b5"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#a0040f72df5ea25d5ed5fbb0e00c50b5"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#a0040f72df5ea25d5ed5fbb0e00c50b5"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#5b8f67ffc457596b97fe80b0e075accd"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#a0040f72df5ea25d5ed5fbb0e00c50b5"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#a0040f72df5ea25d5ed5fbb0e00c50b5"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#a0040f72df5ea25d5ed5fbb0e00c50b5"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#a0040f72df5ea25d5ed5fbb0e00c50b5"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#5b8f67ffc457596b97fe80b0e075accd"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#2e7e6fdc2fcc257cb8670b6b97d9b9ee"><span class="id" title="notation">)</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="pX1p2_pgroup"><span class="id" title="lemma">pX1p2_pgroup</span></a> : <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#354a7719245e28a5f784cfb19c81f53a"><span class="id" title="notation">^{1+2}</span></a>.<br/> + +<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#354a7719245e28a5f784cfb19c81f53a"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.abelian.html#exponent"><span class="id" title="definition">exponent</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#354a7719245e28a5f784cfb19c81f53a"><span class="id" title="notation">^{1+2}</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#aa34fd1c61c5cf0a3356b624a5d2afed"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a>.<br/> + +<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#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) :<br/> + <a class="idref" href="mathcomp.solvable.maximal.html#extraspecial"><span class="id" title="definition">extraspecial</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.abelian.html#exponent"><span class="id" title="definition">exponent</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#aa34fd1c61c5cf0a3356b624a5d2afed"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> 3)%<span class="id" title="var">N</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#ExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#354a7719245e28a5f784cfb19c81f53a"><span class="id" title="notation">^{1+2}</span></a>.<br/> + +<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/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="pX1p2id"><span class="id" title="lemma">pX1p2id</span></a> : <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a7c316c84561ad9c93c7896226b3cab1"><span class="id" title="notation">^{1+2*</span></a>1<a class="idref" href="mathcomp.solvable.extraspecial.html#a7c316c84561ad9c93c7896226b3cab1"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#354a7719245e28a5f784cfb19c81f53a"><span class="id" title="notation">^{1+2}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="pX1p2S"><span class="id" title="lemma">pX1p2S</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.solvable.center.html#xcprod_spec"><span class="id" title="inductive">xcprod_spec</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#fecf17babbfd20e65dfb992ab39dd060"><span class="id" title="notation">^{1+2}</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#6d7462d9f1e45e8985bc5fef0096491d"><span class="id" title="notation">^{1+2*</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#6d7462d9f1e45e8985bc5fef0096491d"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#d5734ed590b969504e2a2cee2726792f"><span class="id" title="notation">^{1+2*</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#d5734ed590b969504e2a2cee2726792f"><span class="id" title="notation">}</span></a>%<span class="id" title="keyword">type</span>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="card_pX1p2n"><span class="id" title="lemma">card_pX1p2n</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.prime.html#prime"><span class="id" title="definition">prime</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a7c316c84561ad9c93c7896226b3cab1"><span class="id" title="notation">^{1+2*</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a7c316c84561ad9c93c7896226b3cab1"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f460b977ac49dd1a229be682bc38c411"><span class="id" title="notation">.*2</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a>)%<span class="id" title="var">N</span>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="pX1p2n_pgroup"><span class="id" title="lemma">pX1p2n_pgroup</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.prime.html#prime"><span class="id" title="definition">prime</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a7c316c84561ad9c93c7896226b3cab1"><span class="id" title="notation">^{1+2*</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a7c316c84561ad9c93c7896226b3cab1"><span class="id" title="notation">}</span></a>.<br/> + +<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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#odd"><span class="id" title="definition">odd</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.abelian.html#exponent"><span class="id" title="definition">exponent</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a7c316c84561ad9c93c7896226b3cab1"><span class="id" title="notation">^{1+2*</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a7c316c84561ad9c93c7896226b3cab1"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a>.<br/> + +<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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#19ab5cfd7e4f60fa14f22b576013bd96"><span class="id" title="notation">></span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.maximal.html#extraspecial"><span class="id" title="definition">extraspecial</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a7c316c84561ad9c93c7896226b3cab1"><span class="id" title="notation">^{1+2*</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a7c316c84561ad9c93c7896226b3cab1"><span class="id" title="notation">}</span></a>.<br/> + +<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#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) :<br/> + <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.maximal.html#extraspecial"><span class="id" title="definition">extraspecial</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#odd"><span class="id" title="definition">odd</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <span class="id" title="keyword">let</span> <span class="id" title="var">Y</span> := <a class="idref" href="mathcomp.solvable.abelian.html#c300ec465942bb74c9d0df0e983eeb01"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.abelian.html#c300ec465942bb74c9d0df0e983eeb01"><span class="id" title="notation">Ohm_1</span></a><a class="idref" href="mathcomp.solvable.abelian.html#c300ec465942bb74c9d0df0e983eeb01"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.abelian.html#c300ec465942bb74c9d0df0e983eeb01"><span class="id" title="notation">)</span></a> <span class="id" title="tactic">in</span><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">[/\</span></a> <a class="idref" href="mathcomp.solvable.abelian.html#exponent"><span class="id" title="definition">exponent</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Y"><span class="id" title="variable">Y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Y"><span class="id" title="variable">Y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#aa34fd1c61c5cf0a3356b624a5d2afed"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Y"><span class="id" title="variable">Y</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">E</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ca13a32469ebe56c9f4cc99d00e8eeba"><span class="id" title="notation">[/\</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Y"><span class="id" title="variable">Y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ca13a32469ebe56c9f4cc99d00e8eeba"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#E"><span class="id" title="variable">E</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#7a45dffb109c3069e5c675be68643e60"><span class="id" title="notation">∨</span></a> <a class="idref" href="mathcomp.solvable.maximal.html#extraspecial"><span class="id" title="definition">extraspecial</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#E"><span class="id" title="variable">E</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ca13a32469ebe56c9f4cc99d00e8eeba"><span class="id" title="notation">,</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#fe60c20831f772c0c3c288abf68cc42a"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">X</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#fe60c20831f772c0c3c288abf68cc42a"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#fe60c20831f772c0c3c288abf68cc42a"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#X"><span class="id" title="variable">X</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#fe60c20831f772c0c3c288abf68cc42a"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#X"><span class="id" title="variable">X</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#3733c0e43956ad2062ab5f1e57ceb9a8"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.gproduct.html#3733c0e43956ad2062ab5f1e57ceb9a8"><span class="id" title="notation">x</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#E"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#Y"><span class="id" title="variable">Y</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ca13a32469ebe56c9f4cc99d00e8eeba"><span class="id" title="notation">&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">M</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">[/\</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.extremal.html#cde820eeae6e659d7da1ef2161ef68ea"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extremal.html#cde820eeae6e659d7da1ef2161ef68ea"><span class="id" title="notation">Mod_</span></a><a class="idref" href="mathcomp.solvable.extremal.html#cde820eeae6e659d7da1ef2161ef68ea"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> 3<a class="idref" href="mathcomp.solvable.extremal.html#cde820eeae6e659d7da1ef2161ef68ea"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#9607c0b7b0a7e59f4327b220d5a93330"><span class="id" title="notation">\*</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#E"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#cb41714a5a23482f7a48a98975fa8c59"><span class="id" title="notation">:&:</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#E"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#M"><span class="id" title="variable">M</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ca13a32469ebe56c9f4cc99d00e8eeba"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">]</span></a>.<br/> + +<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#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) :<br/> + <a class="idref" href="mathcomp.ssreflect.prime.html#prime"><span class="id" title="definition">prime</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.maximal.html#extraspecial"><span class="id" title="definition">extraspecial</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f460b977ac49dd1a229be682bc38c411"><span class="id" title="notation">.*2</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a>)%<span class="id" title="var">N</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.abelian.html#exponent"><span class="id" title="definition">exponent</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#aa34fd1c61c5cf0a3356b624a5d2afed"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a7c316c84561ad9c93c7896226b3cab1"><span class="id" title="notation">^{1+2*</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a7c316c84561ad9c93c7896226b3cab1"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.extraspecial.html#GeneralExponentPextraspecialTheory"><span class="id" title="section">GeneralExponentPextraspecialTheory</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="isog_2X1p2"><span class="id" title="lemma">isog_2X1p2</span></a> : 2<a class="idref" href="mathcomp.solvable.extraspecial.html#354a7719245e28a5f784cfb19c81f53a"><span class="id" title="notation">^{1+2}</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.extremal.html#114753a05fa1a4c728fd6c58cce9f74c"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extremal.html#114753a05fa1a4c728fd6c58cce9f74c"><span class="id" title="notation">D_8</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Q8_extraspecial"><span class="id" title="lemma">Q8_extraspecial</span></a> : <a class="idref" href="mathcomp.solvable.maximal.html#extraspecial"><span class="id" title="definition">extraspecial</span></a> <a class="idref" href="mathcomp.solvable.extremal.html#7a3ab294f809847ed7e277c085de5f5d"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extremal.html#7a3ab294f809847ed7e277c085de5f5d"><span class="id" title="notation">Q_8</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="DnQ_P"><span class="id" title="lemma">DnQ_P</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.solvable.center.html#xcprod_spec"><span class="id" title="inductive">xcprod_spec</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#11fb2c38b9f35b58f4576164683416e2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#11fb2c38b9f35b58f4576164683416e2"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#11fb2c38b9f35b58f4576164683416e2"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.solvable.extremal.html#24d327e6c4148d6dd7b561fa4e1277bd"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extremal.html#24d327e6c4148d6dd7b561fa4e1277bd"><span class="id" title="notation">Q_8</span></a> (<a class="idref" href="mathcomp.solvable.extraspecial.html#060cb01c343ba334280fa026c9b5c80b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#060cb01c343ba334280fa026c9b5c80b"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#060cb01c343ba334280fa026c9b5c80b"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#060cb01c343ba334280fa026c9b5c80b"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#060cb01c343ba334280fa026c9b5c80b"><span class="id" title="notation">Q</span></a>)%<span class="id" title="keyword">type</span>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="card_DnQ"><span class="id" title="lemma">card_DnQ</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">Q</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (2 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f460b977ac49dd1a229be682bc38c411"><span class="id" title="notation">.*2</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a>)%<span class="id" title="var">N</span>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="DnQ_pgroup"><span class="id" title="lemma">DnQ_pgroup</span></a> <span class="id" title="var">n</span> : 2<a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">Q</span></a>.<br/> + +<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#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">Q</span></a>.<br/> + +<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#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) :<br/> + <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 8 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.maximal.html#extraspecial"><span class="id" title="definition">extraspecial</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.extremal.html#114753a05fa1a4c728fd6c58cce9f74c"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extremal.html#114753a05fa1a4c728fd6c58cce9f74c"><span class="id" title="notation">D_8</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">||</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.extremal.html#7a3ab294f809847ed7e277c085de5f5d"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extremal.html#7a3ab294f809847ed7e277c085de5f5d"><span class="id" title="notation">Q_8</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#14a7a9c7dc61f86bfb664d400fabaf8a"><span class="id" title="notation">)</span></a>.<br/> + +<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#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) <span class="id" title="var">n</span> :<br/> + <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (2 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f460b977ac49dd1a229be682bc38c411"><span class="id" title="notation">.*2</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a>)%<span class="id" title="var">N</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.maximal.html#extraspecial"><span class="id" title="definition">extraspecial</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#a8a830ccefaf9cb4d4b2f49d65e5334b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a8a830ccefaf9cb4d4b2f49d65e5334b"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a8a830ccefaf9cb4d4b2f49d65e5334b"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#7a45dffb109c3069e5c675be68643e60"><span class="id" title="notation">∨</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><span class="id" title="notation">.-1</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">Q</span></a>.<br/> + +<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#2e018390d4609ecf460bceadff549bb3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.abelian.html#2e018390d4609ecf460bceadff549bb3"><span class="id" title="notation">r_2</span></a><a class="idref" href="mathcomp.solvable.abelian.html#2e018390d4609ecf460bceadff549bb3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a8a830ccefaf9cb4d4b2f49d65e5334b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a8a830ccefaf9cb4d4b2f49d65e5334b"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a8a830ccefaf9cb4d4b2f49d65e5334b"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.abelian.html#2e018390d4609ecf460bceadff549bb3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a>.<br/> + +<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#2e018390d4609ecf460bceadff549bb3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.abelian.html#2e018390d4609ecf460bceadff549bb3"><span class="id" title="notation">r_2</span></a><a class="idref" href="mathcomp.solvable.abelian.html#2e018390d4609ecf460bceadff549bb3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">Q</span></a><a class="idref" href="mathcomp.solvable.abelian.html#2e018390d4609ecf460bceadff549bb3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a>.<br/> + +<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/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">~~</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a8a830ccefaf9cb4d4b2f49d65e5334b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a8a830ccefaf9cb4d4b2f49d65e5334b"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#a8a830ccefaf9cb4d4b2f49d65e5334b"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">D</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><span class="id" title="notation">.-1</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">×</span></a><a class="idref" href="mathcomp.solvable.extraspecial.html#e3fa577cb2763741bb8ddb9fcf57e5b1"><span class="id" title="notation">Q</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">)</span></a>.<br/> +</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 |