diff options
Diffstat (limited to 'docs/htmldoc/mathcomp.solvable.hall.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.solvable.hall.html | 369 |
1 files changed, 0 insertions, 369 deletions
diff --git a/docs/htmldoc/mathcomp.solvable.hall.html b/docs/htmldoc/mathcomp.solvable.hall.html deleted file mode 100644 index b7a1b3b..0000000 --- a/docs/htmldoc/mathcomp.solvable.hall.html +++ /dev/null @@ -1,369 +0,0 @@ -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" -"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> -<html xmlns="http://www.w3.org/1999/xhtml"> -<head> -<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> -<link href="coqdoc.css" rel="stylesheet" type="text/css" /> -<title>mathcomp.solvable.hall</title> -</head> - -<body> - -<div id="page"> - -<div id="header"> -</div> - -<div id="main"> - -<h1 class="libtitle">Library mathcomp.solvable.hall</h1> - -<div class="code"> -<span class="comment">(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. <br/> - Distributed under the terms of CeCILL-B. *)</span><br/> - -<br/> -</div> - -<div class="doc"> - In this files we prove the Schur-Zassenhaus splitting and transitivity - theorems (under solvability assumptions), then derive P. Hall's - generalization of Sylow's theorem to solvable groups and its corollaries, - in particular the theory of coprime action. We develop both the theory of - coprime action of a solvable group on Sylow subgroups (as in Aschbacher - 18.7), and that of coprime action on Hall subgroups of a solvable group - as per B & G, Proposition 1.5; however we only support external group - action (as opposed to internal action by conjugation) for the latter case - because it is much harder to apply in practice. -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Set Implicit Arguments</span>.<br/> - -<br/> -<span class="id" title="keyword">Import</span> <span class="id" title="var">GroupScope</span>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="Hall"><span class="id" title="section">Hall</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Type</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>.<br/> - -<br/> -<span class="id" title="keyword">Theorem</span> <a name="SchurZassenhaus_split"><span class="id" title="lemma">SchurZassenhaus_split</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) :<br/> - <a class="idref" href="mathcomp.solvable.pgroup.html#Hall"><span class="id" title="definition">Hall</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7e8095b432e7aa5c3c22bb87584658b7"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#67112b78cdc76dbd18c8794f085f2d35"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.gproduct.html#67112b78cdc76dbd18c8794f085f2d35"><span class="id" title="notation">splits</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.gproduct.html#67112b78cdc76dbd18c8794f085f2d35"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#67112b78cdc76dbd18c8794f085f2d35"><span class="id" title="notation">over</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.gproduct.html#67112b78cdc76dbd18c8794f085f2d35"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Theorem</span> <a name="SchurZassenhaus_trans_sol"><span class="id" title="lemma">SchurZassenhaus_trans_sol</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">H</span> <span class="id" title="var">K</span> <span class="id" title="var">K1</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) :<br/> - <a class="idref" href="mathcomp.solvable.nilpotent.html#solvable"><span class="id" title="definition">solvable</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#K1"><span class="id" title="variable">K1</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#8b8794efbfbae1b793d9cb62ce802285"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.solvable.hall.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.ssreflect.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#K1"><span class="id" title="variable">K1</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.hall.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.hall.html#K1"><span class="id" title="variable">K1</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#f0bbce9238fab3dd03626439080979a9"><span class="id" title="notation">:=:</span></a> <a class="idref" href="mathcomp.solvable.hall.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.hall.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="SchurZassenhaus_trans_actsol"><span class="id" title="lemma">SchurZassenhaus_trans_actsol</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> <span class="id" title="var">A</span> <span class="id" title="var">B</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) :<br/> - <a class="idref" href="mathcomp.solvable.nilpotent.html#solvable"><span class="id" title="definition">solvable</span></a> <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#B"><span class="id" title="variable">B</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#0d7ccd69af81527d9facc6293603bbef"><span class="id" title="notation"><*></span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.ssreflect.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.hall.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.hall.html#B"><span class="id" title="variable">B</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#f0bbce9238fab3dd03626439080979a9"><span class="id" title="notation">:=:</span></a> <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.hall.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Hall_exists_subJ"><span class="id" title="lemma">Hall_exists_subJ</span></a> <span class="id" title="var">pi</span> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) :<br/> - <a class="idref" href="mathcomp.solvable.nilpotent.html#solvable"><span class="id" title="definition">solvable</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#59ba2b47d2814e66f8210a649ae6e6bc"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">H</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#59ba2b47d2814e66f8210a649ae6e6bc"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#59ba2b47d2814e66f8210a649ae6e6bc"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.hall.html#pi"><span class="id" title="variable">pi</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">Hall</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#59ba2b47d2814e66f8210a649ae6e6bc"><span class="id" title="notation">&</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">K</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>, <a class="idref" href="mathcomp.solvable.hall.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#pi"><span class="id" title="variable">pi</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#15605b2ce8a0bd336aafa96c5cc1afdc"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#15605b2ce8a0bd336aafa96c5cc1afdc"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.hall.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.hall.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.hall.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.hall.html#Hall"><span class="id" title="section">Hall</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="HallCorollaries"><span class="id" title="section">HallCorollaries</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="HallCorollaries.gT"><span class="id" title="variable">gT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Corollary</span> <a name="Hall_exists"><span class="id" title="lemma">Hall_exists</span></a> <span class="id" title="var">pi</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#HallCorollaries.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) :<br/> - <a class="idref" href="mathcomp.solvable.nilpotent.html#solvable"><span class="id" title="definition">solvable</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#HallCorollaries.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.hall.html#pi"><span class="id" title="variable">pi</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">Hall</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Corollary</span> <a name="Hall_trans"><span class="id" title="lemma">Hall_trans</span></a> <span class="id" title="var">pi</span> (<span class="id" title="var">G</span> <span class="id" title="var">H1</span> <span class="id" title="var">H2</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#HallCorollaries.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) :<br/> - <a class="idref" href="mathcomp.solvable.nilpotent.html#solvable"><span class="id" title="definition">solvable</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#pi"><span class="id" title="variable">pi</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">Hall</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H1"><span class="id" title="variable">H1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#pi"><span class="id" title="variable">pi</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">Hall</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H2"><span class="id" title="variable">H2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.hall.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H1"><span class="id" title="variable">H1</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#f0bbce9238fab3dd03626439080979a9"><span class="id" title="notation">:=:</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H2"><span class="id" title="variable">H2</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.hall.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Corollary</span> <a name="Hall_superset"><span class="id" title="lemma">Hall_superset</span></a> <span class="id" title="var">pi</span> (<span class="id" title="var">G</span> <span class="id" title="var">K</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#HallCorollaries.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) :<br/> - <a class="idref" href="mathcomp.solvable.nilpotent.html#solvable"><span class="id" title="definition">solvable</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#pi"><span class="id" title="variable">pi</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#15605b2ce8a0bd336aafa96c5cc1afdc"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#15605b2ce8a0bd336aafa96c5cc1afdc"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#59ba2b47d2814e66f8210a649ae6e6bc"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">H</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#59ba2b47d2814e66f8210a649ae6e6bc"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#HallCorollaries.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#59ba2b47d2814e66f8210a649ae6e6bc"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.hall.html#pi"><span class="id" title="variable">pi</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">Hall</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#59ba2b47d2814e66f8210a649ae6e6bc"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.hall.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Corollary</span> <a name="Hall_subJ"><span class="id" title="lemma">Hall_subJ</span></a> <span class="id" title="var">pi</span> (<span class="id" title="var">G</span> <span class="id" title="var">H</span> <span class="id" title="var">K</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#HallCorollaries.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) :<br/> - <a class="idref" href="mathcomp.solvable.nilpotent.html#solvable"><span class="id" title="definition">solvable</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#pi"><span class="id" title="variable">pi</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">Hall</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#pi"><span class="id" title="variable">pi</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#15605b2ce8a0bd336aafa96c5cc1afdc"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#15605b2ce8a0bd336aafa96c5cc1afdc"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.hall.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.hall.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.hall.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Corollary</span> <a name="Hall_Jsub"><span class="id" title="lemma">Hall_Jsub</span></a> <span class="id" title="var">pi</span> (<span class="id" title="var">G</span> <span class="id" title="var">H</span> <span class="id" title="var">K</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#HallCorollaries.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) :<br/> - <a class="idref" href="mathcomp.solvable.nilpotent.html#solvable"><span class="id" title="definition">solvable</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#pi"><span class="id" title="variable">pi</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">Hall</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#pi"><span class="id" title="variable">pi</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#15605b2ce8a0bd336aafa96c5cc1afdc"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#15605b2ce8a0bd336aafa96c5cc1afdc"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.hall.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.hall.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.hall.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Hall_Frattini_arg"><span class="id" title="lemma">Hall_Frattini_arg</span></a> <span class="id" title="var">pi</span> (<span class="id" title="var">G</span> <span class="id" title="var">K</span> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#HallCorollaries.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) :<br/> - <a class="idref" href="mathcomp.solvable.nilpotent.html#solvable"><span class="id" title="definition">solvable</span></a> <a class="idref" href="mathcomp.solvable.hall.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7e8095b432e7aa5c3c22bb87584658b7"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#pi"><span class="id" title="variable">pi</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">Hall</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#8b8794efbfbae1b793d9cb62ce802285"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#ee98cf35a816a182ecdf169a5f07c7f5"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ee98cf35a816a182ecdf169a5f07c7f5"><span class="id" title="notation">N_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ee98cf35a816a182ecdf169a5f07c7f5"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ee98cf35a816a182ecdf169a5f07c7f5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.hall.html#HallCorollaries"><span class="id" title="section">HallCorollaries</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="InternalAction"><span class="id" title="section">InternalAction</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="InternalAction.pi"><span class="id" title="variable">pi</span></a> : <a class="idref" href="mathcomp.ssreflect.prime.html#nat_pred"><span class="id" title="definition">nat_pred</span></a>) (<a name="InternalAction.gT"><span class="id" title="variable">gT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>).<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">G</span> <span class="id" title="var">H</span> <span class="id" title="var">K</span> <span class="id" title="var">A</span> <span class="id" title="var">X</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#InternalAction.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - Part of Aschbacher (18.7.4). -</div> -<div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="coprime_norm_cent"><span class="id" title="lemma">coprime_norm_cent</span></a> <span class="id" title="var">A</span> <span class="id" title="var">G</span> :<br/> - <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#ee98cf35a816a182ecdf169a5f07c7f5"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ee98cf35a816a182ecdf169a5f07c7f5"><span class="id" title="notation">N_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ee98cf35a816a182ecdf169a5f07c7f5"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ee98cf35a816a182ecdf169a5f07c7f5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">)</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - This is B & G, Proposition 1.5(a) -</div> -<div class="code"> -<span class="id" title="keyword">Proposition</span> <a name="coprime_Hall_exists"><span class="id" title="lemma">coprime_Hall_exists</span></a> <span class="id" title="var">A</span> <span class="id" title="var">G</span> :<br/> - <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.nilpotent.html#solvable"><span class="id" title="definition">solvable</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#59ba2b47d2814e66f8210a649ae6e6bc"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">H</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#59ba2b47d2814e66f8210a649ae6e6bc"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#InternalAction.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#59ba2b47d2814e66f8210a649ae6e6bc"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.hall.html#InternalAction.pi"><span class="id" title="variable">pi</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">Hall</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#59ba2b47d2814e66f8210a649ae6e6bc"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - This is B & G, Proposition 1.5(c) -</div> -<div class="code"> -<span class="id" title="keyword">Proposition</span> <a name="coprime_Hall_trans"><span class="id" title="lemma">coprime_Hall_trans</span></a> <span class="id" title="var">A</span> <span class="id" title="var">G</span> <span class="id" title="var">H1</span> <span class="id" title="var">H2</span> :<br/> - <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.nilpotent.html#solvable"><span class="id" title="definition">solvable</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.solvable.hall.html#InternalAction.pi"><span class="id" title="variable">pi</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">Hall</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H1"><span class="id" title="variable">H1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#H1"><span class="id" title="variable">H1</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.solvable.hall.html#InternalAction.pi"><span class="id" title="variable">pi</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">Hall</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H2"><span class="id" title="variable">H2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#H2"><span class="id" title="variable">H2</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.hall.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H1"><span class="id" title="variable">H1</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#f0bbce9238fab3dd03626439080979a9"><span class="id" title="notation">:=:</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H2"><span class="id" title="variable">H2</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.hall.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - A complement to the above: 'C(A) acts on 'Nby(A) -</div> -<div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="norm_conj_cent"><span class="id" title="lemma">norm_conj_cent</span></a> <span class="id" title="var">A</span> <span class="id" title="var">G</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.solvable.hall.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#313ef60ac6c7566906fa5b28c1bbf405"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#313ef60ac6c7566906fa5b28c1bbf405"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#313ef60ac6c7566906fa5b28c1bbf405"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#313ef60ac6c7566906fa5b28c1bbf405"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.hall.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - Strongest version of the centraliser lemma -- not found in textbooks! - Obviously, the solvability condition could be removed once we have the - Odd Order Theorem. -</div> -<div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="strongest_coprime_quotient_cent"><span class="id" title="lemma">strongest_coprime_quotient_cent</span></a> <span class="id" title="var">A</span> <span class="id" title="var">G</span> <span class="id" title="var">H</span> :<br/> - <span class="id" title="keyword">let</span> <span class="id" title="var">R</span> := <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#b9596739b058766532fc6517a36fef9f"><span class="id" title="notation">:&:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#653e048e978e57b1e513b9d5de2caee6"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#653e048e978e57b1e513b9d5de2caee6"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#653e048e978e57b1e513b9d5de2caee6"><span class="id" title="notation">]</span></a> <span class="id" title="tactic">in</span><br/> - <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#R"><span class="id" title="variable">R</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.solvable.nilpotent.html#solvable"><span class="id" title="definition">solvable</span></a> <a class="idref" href="mathcomp.solvable.hall.html#R"><span class="id" title="variable">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#081ff67d3116402bb680e8692aa39185"><span class="id" title="notation">||</span></a> <a class="idref" href="mathcomp.solvable.nilpotent.html#solvable"><span class="id" title="definition">solvable</span></a> <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#3e65ad3edf5f7fb3ea6bc63a878112a8"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1229b60a3ad237c4221725993c4f13c1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1229b60a3ad237c4221725993c4f13c1"><span class="id" title="notation">C_</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1229b60a3ad237c4221725993c4f13c1"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#3e65ad3edf5f7fb3ea6bc63a878112a8"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1229b60a3ad237c4221725993c4f13c1"><span class="id" title="notation">)(</span></a><a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#3e65ad3edf5f7fb3ea6bc63a878112a8"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1229b60a3ad237c4221725993c4f13c1"><span class="id" title="notation">)</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - A weaker but more practical version, still stronger than the usual form - (viz. Aschbacher 18.7.4), similar to the one needed in Aschbacher's - proof of Thompson factorization. Note that the coprime and solvability - assumptions could be further weakened to H :&: G (and hence become - trivial if H and G are TI). However, the assumption that A act on G is - needed in this case. -</div> -<div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="coprime_norm_quotient_cent"><span class="id" title="lemma">coprime_norm_quotient_cent</span></a> <span class="id" title="var">A</span> <span class="id" title="var">G</span> <span class="id" title="var">H</span> :<br/> - <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.nilpotent.html#solvable"><span class="id" title="definition">solvable</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#3e65ad3edf5f7fb3ea6bc63a878112a8"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1229b60a3ad237c4221725993c4f13c1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1229b60a3ad237c4221725993c4f13c1"><span class="id" title="notation">C_</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1229b60a3ad237c4221725993c4f13c1"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#3e65ad3edf5f7fb3ea6bc63a878112a8"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1229b60a3ad237c4221725993c4f13c1"><span class="id" title="notation">)(</span></a><a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#3e65ad3edf5f7fb3ea6bc63a878112a8"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1229b60a3ad237c4221725993c4f13c1"><span class="id" title="notation">)</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - A useful consequence (similar to Ex. 6.1 in Aschbacher) of the stronger - theorem. -</div> -<div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="coprime_cent_mulG"><span class="id" title="lemma">coprime_cent_mulG</span></a> <span class="id" title="var">A</span> <span class="id" title="var">G</span> <span class="id" title="var">H</span> :<br/> - <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.ssreflect.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.nilpotent.html#solvable"><span class="id" title="definition">solvable</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.fingroup.fingroup.html#1229b60a3ad237c4221725993c4f13c1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1229b60a3ad237c4221725993c4f13c1"><span class="id" title="notation">C_</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1229b60a3ad237c4221725993c4f13c1"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#8b8794efbfbae1b793d9cb62ce802285"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1229b60a3ad237c4221725993c4f13c1"><span class="id" title="notation">)(</span></a><a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1229b60a3ad237c4221725993c4f13c1"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">C_H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#8b8794efbfbae1b793d9cb62ce802285"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">)</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - Another special case of the strong coprime quotient lemma; not found in - textbooks, but nevertheless used implicitly throughout B & G, sometimes - justified by switching to external action. -</div> -<div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="quotient_TI_subcent"><span class="id" title="lemma">quotient_TI_subcent</span></a> <span class="id" title="var">K</span> <span class="id" title="var">G</span> <span class="id" title="var">H</span> :<br/> - <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#b9596739b058766532fc6517a36fef9f"><span class="id" title="notation">:&:</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">C_K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#3e65ad3edf5f7fb3ea6bc63a878112a8"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1229b60a3ad237c4221725993c4f13c1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1229b60a3ad237c4221725993c4f13c1"><span class="id" title="notation">C_</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1229b60a3ad237c4221725993c4f13c1"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#3e65ad3edf5f7fb3ea6bc63a878112a8"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1229b60a3ad237c4221725993c4f13c1"><span class="id" title="notation">)(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#3e65ad3edf5f7fb3ea6bc63a878112a8"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1229b60a3ad237c4221725993c4f13c1"><span class="id" title="notation">)</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - This is B & G, Proposition 1.5(d): the more traditional form of the lemma - above, with the assumption H <| G weakened to H \subset G. The stronger - coprime and solvability assumptions are easier to satisfy in practice. -</div> -<div class="code"> -<span class="id" title="keyword">Proposition</span> <a name="coprime_quotient_cent"><span class="id" title="lemma">coprime_quotient_cent</span></a> <span class="id" title="var">A</span> <span class="id" title="var">G</span> <span class="id" title="var">H</span> :<br/> - <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.nilpotent.html#solvable"><span class="id" title="definition">solvable</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#3e65ad3edf5f7fb3ea6bc63a878112a8"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1229b60a3ad237c4221725993c4f13c1"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1229b60a3ad237c4221725993c4f13c1"><span class="id" title="notation">C_</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1229b60a3ad237c4221725993c4f13c1"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#3e65ad3edf5f7fb3ea6bc63a878112a8"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1229b60a3ad237c4221725993c4f13c1"><span class="id" title="notation">)(</span></a><a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#3e65ad3edf5f7fb3ea6bc63a878112a8"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1229b60a3ad237c4221725993c4f13c1"><span class="id" title="notation">)</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - This is B & G, Proposition 1.5(e). -</div> -<div class="code"> -<span class="id" title="keyword">Proposition</span> <a name="coprime_comm_pcore"><span class="id" title="lemma">coprime_comm_pcore</span></a> <span class="id" title="var">A</span> <span class="id" title="var">G</span> <span class="id" title="var">K</span> :<br/> - <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.nilpotent.html#solvable"><span class="id" title="definition">solvable</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.solvable.hall.html#InternalAction.pi"><span class="id" title="variable">pi</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#ca29ecf9a3780bf15fe608e2d2c00594"><span class="id" title="notation">^'</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">Hall</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.hall.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.fingroup.fingroup.html#653e048e978e57b1e513b9d5de2caee6"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#653e048e978e57b1e513b9d5de2caee6"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#653e048e978e57b1e513b9d5de2caee6"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.pgroup.html#64e6c9ddce70097e2cb88e9baa3b5a39"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#64e6c9ddce70097e2cb88e9baa3b5a39"><span class="id" title="notation">O_pi</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#64e6c9ddce70097e2cb88e9baa3b5a39"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#64e6c9ddce70097e2cb88e9baa3b5a39"><span class="id" title="notation">)</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.hall.html#InternalAction"><span class="id" title="section">InternalAction</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - This is B & G, Proposition 1.5(b). -</div> -<div class="code"> -<span class="id" title="keyword">Proposition</span> <a name="coprime_Hall_subset"><span class="id" title="lemma">coprime_Hall_subset</span></a> <span class="id" title="var">pi</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">A</span> <span class="id" title="var">G</span> <span class="id" title="var">X</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) :<br/> - <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.nilpotent.html#solvable"><span class="id" title="definition">solvable</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.solvable.hall.html#X"><span class="id" title="variable">X</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#pi"><span class="id" title="variable">pi</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#15605b2ce8a0bd336aafa96c5cc1afdc"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#15605b2ce8a0bd336aafa96c5cc1afdc"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#X"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#X"><span class="id" title="variable">X</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">[/\</span></a> <a class="idref" href="mathcomp.solvable.hall.html#pi"><span class="id" title="variable">pi</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">Hall</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.hall.html#X"><span class="id" title="variable">X</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="ExternalAction"><span class="id" title="section">ExternalAction</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="ExternalAction.pi"><span class="id" title="variable">pi</span></a> : <a class="idref" href="mathcomp.ssreflect.prime.html#nat_pred"><span class="id" title="definition">nat_pred</span></a>) (<a name="ExternalAction.aT"><span class="id" title="variable">aT</span></a> <a name="ExternalAction.gT"><span class="id" title="variable">gT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>).<br/> -<span class="id" title="keyword">Variables</span> (<a name="ExternalAction.A"><span class="id" title="variable">A</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) (<a name="ExternalAction.G"><span class="id" title="variable">G</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) (<a name="ExternalAction.to"><span class="id" title="variable">to</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#groupAction"><span class="id" title="record">groupAction</span></a> <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="ExternalAction.FullExtension"><span class="id" title="section">FullExtension</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Let</span> <a name="ExternalAction.FullExtension.injG"><span class="id" title="variable">injG</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.solvable.hall.html#inG"><span class="id" title="abbreviation">inG</span></a> := <a class="idref" href="mathcomp.fingroup.gproduct.html#injm_sdpair1"><span class="id" title="lemma">injm_sdpair1</span></a> <span class="id" title="var">_</span>.<br/> -<span class="id" title="keyword">Let</span> <a name="ExternalAction.FullExtension.injA"><span class="id" title="variable">injA</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.solvable.hall.html#inA"><span class="id" title="abbreviation">inA</span></a> := <a class="idref" href="mathcomp.fingroup.gproduct.html#injm_sdpair2"><span class="id" title="lemma">injm_sdpair2</span></a> <span class="id" title="var">_</span>.<br/> - -<br/> -<span class="id" title="keyword">Hypotheses</span> (<a name="ExternalAction.FullExtension.coGA"><span class="id" title="variable">coGA</span></a> : <a class="idref" href="mathcomp.ssreflect.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a>) (<a name="ExternalAction.FullExtension.solG"><span class="id" title="variable">solG</span></a> : <a class="idref" href="mathcomp.solvable.nilpotent.html#solvable"><span class="id" title="definition">solvable</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.G"><span class="id" title="variable">G</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="external_action_im_coprime"><span class="id" title="lemma">external_action_im_coprime</span></a> : <a class="idref" href="mathcomp.ssreflect.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#G'"><span class="id" title="abbreviation">G'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#A'"><span class="id" title="abbreviation">A'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Let</span> <a name="ExternalAction.FullExtension.coGA'"><span class="id" title="variable">coGA'</span></a> := <a class="idref" href="mathcomp.solvable.hall.html#external_action_im_coprime"><span class="id" title="lemma">external_action_im_coprime</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Let</span> <a name="ExternalAction.FullExtension.solG'"><span class="id" title="variable">solG'</span></a> : <a class="idref" href="mathcomp.solvable.nilpotent.html#solvable"><span class="id" title="definition">solvable</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G'"><span class="id" title="abbreviation">G'</span></a> := <a class="idref" href="mathcomp.solvable.nilpotent.html#morphim_sol"><span class="id" title="lemma">morphim_sol</span></a> <span class="id" title="var">_</span> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.FullExtension.solG"><span class="id" title="variable">solG</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Let</span> <a name="ExternalAction.FullExtension.nGA'"><span class="id" title="variable">nGA'</span></a> := <a class="idref" href="mathcomp.fingroup.gproduct.html#im_sdpair_norm"><span class="id" title="lemma">im_sdpair_norm</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.to"><span class="id" title="variable">to</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="ext_coprime_Hall_exists"><span class="id" title="lemma">ext_coprime_Hall_exists</span></a> :<br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#59ba2b47d2814e66f8210a649ae6e6bc"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">H</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#59ba2b47d2814e66f8210a649ae6e6bc"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#59ba2b47d2814e66f8210a649ae6e6bc"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.pi"><span class="id" title="variable">pi</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">Hall</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#59ba2b47d2814e66f8210a649ae6e6bc"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">acts</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="ext_coprime_Hall_trans"><span class="id" title="lemma">ext_coprime_Hall_trans</span></a> (<span class="id" title="var">H1</span> <span class="id" title="var">H2</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) :<br/> - <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.pi"><span class="id" title="variable">pi</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">Hall</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H1"><span class="id" title="variable">H1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">acts</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H1"><span class="id" title="variable">H1</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.pi"><span class="id" title="variable">pi</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">Hall</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H2"><span class="id" title="variable">H2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">acts</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H2"><span class="id" title="variable">H2</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.hall.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.action.html#2ae6f5a80bf45b13993075049a02e31d"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#2ae6f5a80bf45b13993075049a02e31d"><span class="id" title="notation">C_</span></a><a class="idref" href="mathcomp.fingroup.action.html#2ae6f5a80bf45b13993075049a02e31d"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.action.html#2ae6f5a80bf45b13993075049a02e31d"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#2ae6f5a80bf45b13993075049a02e31d"><span class="id" title="notation">)(</span></a><a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#2ae6f5a80bf45b13993075049a02e31d"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H1"><span class="id" title="variable">H1</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#f0bbce9238fab3dd03626439080979a9"><span class="id" title="notation">:=:</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H2"><span class="id" title="variable">H2</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.hall.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="ext_norm_conj_cent"><span class="id" title="lemma">ext_norm_conj_cent</span></a> (<span class="id" title="var">H</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) <span class="id" title="var">x</span> :<br/> - <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.action.html#2ae6f5a80bf45b13993075049a02e31d"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#2ae6f5a80bf45b13993075049a02e31d"><span class="id" title="notation">C_</span></a><a class="idref" href="mathcomp.fingroup.action.html#2ae6f5a80bf45b13993075049a02e31d"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.action.html#2ae6f5a80bf45b13993075049a02e31d"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#2ae6f5a80bf45b13993075049a02e31d"><span class="id" title="notation">)(</span></a><a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#2ae6f5a80bf45b13993075049a02e31d"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">acts</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.hall.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">acts</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="ext_coprime_Hall_subset"><span class="id" title="lemma">ext_coprime_Hall_subset</span></a> (<span class="id" title="var">X</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) :<br/> - <a class="idref" href="mathcomp.solvable.hall.html#X"><span class="id" title="variable">X</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.pi"><span class="id" title="variable">pi</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#15605b2ce8a0bd336aafa96c5cc1afdc"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#15605b2ce8a0bd336aafa96c5cc1afdc"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#X"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">acts</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.hall.html#X"><span class="id" title="variable">X</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">[/\</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.pi"><span class="id" title="variable">pi</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">Hall</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#a4de5afc30e4046e35829de6f2bc75f3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">acts</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.hall.html#X"><span class="id" title="variable">X</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.FullExtension"><span class="id" title="section">FullExtension</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - We only prove a weaker form of the coprime group action centraliser - lemma, because it is more convenient in practice to make G the range - of the action, whence G both contains H and is stable under A. - However we do restrict the coprime/solvable assumptions to H, and - we do not require that G normalize H. -</div> -<div class="code"> -<span class="id" title="keyword">Lemma</span> <a name="ext_coprime_quotient_cent"><span class="id" title="lemma">ext_coprime_quotient_cent</span></a> (<span class="id" title="var">H</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) :<br/> - <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">acts</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.nilpotent.html#solvable"><span class="id" title="definition">solvable</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.fingroup.action.html#759306ed561fe32883e7922c4926d86c"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#759306ed561fe32883e7922c4926d86c"><span class="id" title="notation">C_</span></a><a class="idref" href="mathcomp.fingroup.action.html#759306ed561fe32883e7922c4926d86c"><span class="id" title="notation">(|</span></a><a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#759306ed561fe32883e7922c4926d86c"><span class="id" title="notation">)(</span></a><a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#759306ed561fe32883e7922c4926d86c"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#3e65ad3edf5f7fb3ea6bc63a878112a8"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.action.html#759306ed561fe32883e7922c4926d86c"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#759306ed561fe32883e7922c4926d86c"><span class="id" title="notation">C_</span></a><a class="idref" href="mathcomp.fingroup.action.html#759306ed561fe32883e7922c4926d86c"><span class="id" title="notation">(|</span></a><a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.fingroup.action.html#41672295fce40becd46688b39618a9e3"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.hall.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.action.html#759306ed561fe32883e7922c4926d86c"><span class="id" title="notation">)(</span></a><a class="idref" href="mathcomp.solvable.hall.html#ExternalAction.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#759306ed561fe32883e7922c4926d86c"><span class="id" title="notation">)</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.hall.html#ExternalAction"><span class="id" title="section">ExternalAction</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="SylowSolvableAct"><span class="id" title="section">SylowSolvableAct</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="SylowSolvableAct.gT"><span class="id" title="variable">gT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<a name="SylowSolvableAct.p"><span class="id" title="variable">p</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>).<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">A</span> <span class="id" title="var">B</span> <span class="id" title="var">G</span> <span class="id" title="var">X</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#SylowSolvableAct.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="sol_coprime_Sylow_exists"><span class="id" title="lemma">sol_coprime_Sylow_exists</span></a> <span class="id" title="var">A</span> <span class="id" title="var">G</span> :<br/> - <a class="idref" href="mathcomp.solvable.nilpotent.html#solvable"><span class="id" title="definition">solvable</span></a> <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#59ba2b47d2814e66f8210a649ae6e6bc"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">P</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#59ba2b47d2814e66f8210a649ae6e6bc"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#SylowSolvableAct.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#59ba2b47d2814e66f8210a649ae6e6bc"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.hall.html#SylowSolvableAct.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#081d3e80d093e95dd63e6bafc24fef78"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#081d3e80d093e95dd63e6bafc24fef78"><span class="id" title="notation">Sylow</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#081d3e80d093e95dd63e6bafc24fef78"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#081d3e80d093e95dd63e6bafc24fef78"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.hall.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#59ba2b47d2814e66f8210a649ae6e6bc"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#P"><span class="id" title="variable">P</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="sol_coprime_Sylow_trans"><span class="id" title="lemma">sol_coprime_Sylow_trans</span></a> <span class="id" title="var">A</span> <span class="id" title="var">G</span> :<br/> - <a class="idref" href="mathcomp.solvable.nilpotent.html#solvable"><span class="id" title="definition">solvable</span></a> <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">transitive</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#91816551bcea1b6f359ecf76f3595e38"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#91816551bcea1b6f359ecf76f3595e38"><span class="id" title="notation">set</span></a> <span class="id" title="var">P</span> <a class="idref" href="mathcomp.ssreflect.finset.html#91816551bcea1b6f359ecf76f3595e38"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.pgroup.html#2cfdfd6f05a28cf984c6e60aeed6378f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#2cfdfd6f05a28cf984c6e60aeed6378f"><span class="id" title="notation">Syl_p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#2cfdfd6f05a28cf984c6e60aeed6378f"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#2cfdfd6f05a28cf984c6e60aeed6378f"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#91816551bcea1b6f359ecf76f3595e38"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#P"><span class="id" title="variable">P</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#91816551bcea1b6f359ecf76f3595e38"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.action.html#9cb8ec4e4ed9f2067382df1e9eea44f5"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#9cb8ec4e4ed9f2067382df1e9eea44f5"><span class="id" title="notation">JG</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="sol_coprime_Sylow_subset"><span class="id" title="lemma">sol_coprime_Sylow_subset</span></a> <span class="id" title="var">A</span> <span class="id" title="var">G</span> <span class="id" title="var">X</span> :<br/> - <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.nilpotent.html#solvable"><span class="id" title="definition">solvable</span></a> <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.solvable.hall.html#X"><span class="id" title="variable">X</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#SylowSolvableAct.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#15605b2ce8a0bd336aafa96c5cc1afdc"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#15605b2ce8a0bd336aafa96c5cc1afdc"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#X"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#X"><span class="id" title="variable">X</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <span class="id" title="var">P</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.hall.html#SylowSolvableAct.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">[/\</span></a> <a class="idref" href="mathcomp.solvable.hall.html#SylowSolvableAct.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#081d3e80d093e95dd63e6bafc24fef78"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#081d3e80d093e95dd63e6bafc24fef78"><span class="id" title="notation">Sylow</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#081d3e80d093e95dd63e6bafc24fef78"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#081d3e80d093e95dd63e6bafc24fef78"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.hall.html#P"><span class="id" title="variable">P</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.hall.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.hall.html#P"><span class="id" title="variable">P</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.hall.html#X"><span class="id" title="variable">X</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.hall.html#P"><span class="id" title="variable">P</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.hall.html#SylowSolvableAct"><span class="id" title="section">SylowSolvableAct</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 |