diff options
| author | Enrico Tassi | 2018-04-20 10:54:22 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-04-20 10:54:22 +0200 |
| commit | ed05182cece6bb3706e09b2ce14af4a41a2e8141 (patch) | |
| tree | e850d7314b6372d0476cf2ffaf7d3830721db7b1 /docs/htmldoc/mathcomp.solvable.sylow.html | |
| parent | 3d196f44681fb3b23ff8a79fbd44e12308680531 (diff) | |
generate the documentation for 1.7
Diffstat (limited to 'docs/htmldoc/mathcomp.solvable.sylow.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.solvable.sylow.html | 326 |
1 files changed, 326 insertions, 0 deletions
diff --git a/docs/htmldoc/mathcomp.solvable.sylow.html b/docs/htmldoc/mathcomp.solvable.sylow.html new file mode 100644 index 0000000..151cabb --- /dev/null +++ b/docs/htmldoc/mathcomp.solvable.sylow.html @@ -0,0 +1,326 @@ +<!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.sylow</title> +</head> + +<body> + +<div id="page"> + +<div id="header"> +</div> + +<div id="main"> + +<h1 class="libtitle">Library mathcomp.solvable.sylow</h1> + +<div class="code"> +<span class="comment">(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. <br/> + Distributed under the terms of CeCILL-B. *)</span><br/> +<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#"><span class="id" title="library">mathcomp.ssreflect.ssreflect</span></a>.<br/> + +<br/> +</div> + +<div class="doc"> + The Sylow theorem and its consequences, including the Frattini argument, + the nilpotence of p-groups, and the Baer-Suzuki theorem. + This file also defines: + Zgroup G == G is a Z-group, i.e., has only cyclic Sylow p-subgroups. +</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/> +</div> + +<div class="doc"> + The mod p lemma for the action of p-groups. +</div> +<div class="code"> +<span class="id" title="keyword">Section</span> <a name="ModP"><span class="id" title="section">ModP</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variable</span> (<a name="ModP.aT"><span class="id" title="variable">aT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<a name="ModP.sT"><span class="id" title="variable">sT</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) (<a name="ModP.D"><span class="id" title="variable">D</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>).<br/> +<span class="id" title="keyword">Variable</span> <a name="ModP.to"><span class="id" title="variable">to</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#action"><span class="id" title="record">action</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#ModP.D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#ModP.sT"><span class="id" title="variable">sT</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="pgroup_fix_mod"><span class="id" title="lemma">pgroup_fix_mod</span></a> (<span class="id" title="var">p</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#ModP.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">S</span> : <a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#ModP.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a>) :<br/> + <a class="idref" href="mathcomp.solvable.sylow.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">acts</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#ModP.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.sylow.html#S"><span class="id" title="variable">S</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#20229f50700a74daa1cbc50e0281abb6"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.fingroup.action.html#35fe9120fe28e031e47d4f6cccd1bd3b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#35fe9120fe28e031e47d4f6cccd1bd3b"><span class="id" title="notation">Fix_</span></a><a class="idref" href="mathcomp.fingroup.action.html#35fe9120fe28e031e47d4f6cccd1bd3b"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.action.html#35fe9120fe28e031e47d4f6cccd1bd3b"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#ModP.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#35fe9120fe28e031e47d4f6cccd1bd3b"><span class="id" title="notation">)(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.action.html#35fe9120fe28e031e47d4f6cccd1bd3b"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#20229f50700a74daa1cbc50e0281abb6"><span class="id" title="notation">%[</span></a><a class="idref" href="mathcomp.ssreflect.div.html#20229f50700a74daa1cbc50e0281abb6"><span class="id" title="notation">mod</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.ssreflect.div.html#20229f50700a74daa1cbc50e0281abb6"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.sylow.html#ModP"><span class="id" title="section">ModP</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="ModularGroupAction"><span class="id" title="section">ModularGroupAction</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="ModularGroupAction.aT"><span class="id" title="variable">aT</span></a> <a name="ModularGroupAction.rT"><span class="id" title="variable">rT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<a name="ModularGroupAction.D"><span class="id" title="variable">D</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<a name="ModularGroupAction.R"><span class="id" title="variable">R</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>).<br/> +<span class="id" title="keyword">Variables</span> (<a name="ModularGroupAction.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.sylow.html#ModularGroupAction.D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#ModularGroupAction.R"><span class="id" title="variable">R</span></a>) (<a name="ModularGroupAction.p"><span class="id" title="variable">p</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>).<br/> +<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">G</span> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#ModularGroupAction.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">M</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#ModularGroupAction.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="nontrivial_gacent_pgroup"><span class="id" title="lemma">nontrivial_gacent_pgroup</span></a> <span class="id" title="var">G</span> <span class="id" title="var">M</span> :<br/> + <a class="idref" href="mathcomp.solvable.sylow.html#ModularGroupAction.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#ModularGroupAction.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#942d78c074baecb495cbc019394dd5b3"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.action.html#942d78c074baecb495cbc019394dd5b3"><span class="id" title="notation">acts</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.action.html#942d78c074baecb495cbc019394dd5b3"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#942d78c074baecb495cbc019394dd5b3"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.fingroup.action.html#942d78c074baecb495cbc019394dd5b3"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.fingroup.action.html#942d78c074baecb495cbc019394dd5b3"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#ModularGroupAction.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#942d78c074baecb495cbc019394dd5b3"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.solvable.sylow.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#36625695d37b6869c156bfcdf13834f7"><span class="id" title="notation">:!=:</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#80a58c159fbe61cbb7996107e4e1da9b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#80a58c159fbe61cbb7996107e4e1da9b"><span class="id" title="notation">C_</span></a><a class="idref" href="mathcomp.fingroup.action.html#80a58c159fbe61cbb7996107e4e1da9b"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.fingroup.action.html#80a58c159fbe61cbb7996107e4e1da9b"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#ModularGroupAction.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#80a58c159fbe61cbb7996107e4e1da9b"><span class="id" title="notation">)(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.action.html#80a58c159fbe61cbb7996107e4e1da9b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#36625695d37b6869c156bfcdf13834f7"><span class="id" title="notation">:!=:</span></a> 1.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="pcore_sub_astab_irr"><span class="id" title="lemma">pcore_sub_astab_irr</span></a> <span class="id" title="var">G</span> <span class="id" title="var">M</span> :<br/> + <a class="idref" href="mathcomp.solvable.sylow.html#ModularGroupAction.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#ModularGroupAction.R"><span class="id" title="variable">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#acts_irreducibly"><span class="id" title="definition">acts_irreducibly</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#ModularGroupAction.to"><span class="id" title="variable">to</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.solvable.pgroup.html#5a60f5e4463d132504644978fbcd8502"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5a60f5e4463d132504644978fbcd8502"><span class="id" title="notation">O_p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5a60f5e4463d132504644978fbcd8502"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5a60f5e4463d132504644978fbcd8502"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.action.html#652d6cc67746e5361142d90686607781"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#652d6cc67746e5361142d90686607781"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.action.html#652d6cc67746e5361142d90686607781"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.fingroup.action.html#652d6cc67746e5361142d90686607781"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#ModularGroupAction.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#652d6cc67746e5361142d90686607781"><span class="id" title="notation">)</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="pcore_faithful_irr_act"><span class="id" title="lemma">pcore_faithful_irr_act</span></a> <span class="id" title="var">G</span> <span class="id" title="var">M</span> :<br/> + <a class="idref" href="mathcomp.solvable.sylow.html#ModularGroupAction.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#ModularGroupAction.R"><span class="id" title="variable">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#acts_irreducibly"><span class="id" title="definition">acts_irreducibly</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#ModularGroupAction.to"><span class="id" title="variable">to</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.fingroup.action.html#6e1bf5287bfc6397badc2a71c227e8d0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#6e1bf5287bfc6397badc2a71c227e8d0"><span class="id" title="notation">faithful</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.action.html#6e1bf5287bfc6397badc2a71c227e8d0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#6e1bf5287bfc6397badc2a71c227e8d0"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.fingroup.action.html#6e1bf5287bfc6397badc2a71c227e8d0"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#ModularGroupAction.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#6e1bf5287bfc6397badc2a71c227e8d0"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.solvable.pgroup.html#5a60f5e4463d132504644978fbcd8502"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5a60f5e4463d132504644978fbcd8502"><span class="id" title="notation">O_p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5a60f5e4463d132504644978fbcd8502"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5a60f5e4463d132504644978fbcd8502"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 1.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.sylow.html#ModularGroupAction"><span class="id" title="section">ModularGroupAction</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="Sylow"><span class="id" title="section">Sylow</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="Sylow.p"><span class="id" title="variable">p</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a name="Sylow.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="Sylow.G"><span class="id" title="variable">G</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>).<br/> +<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">P</span> <span class="id" title="var">Q</span> <span class="id" title="var">H</span> <span class="id" title="var">K</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Sylow.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Theorem</span> <a name="Sylow's_theorem"><span class="id" title="lemma">Sylow's_theorem</span></a> :<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ca13a32469ebe56c9f4cc99d00e8eeba"><span class="id" title="notation">[/\</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">P</span>, <a class="idref" href="mathcomp.fingroup.fingroup.html#037a06093aea0e31650c64484aec1c53"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#037a06093aea0e31650c64484aec1c53"><span class="id" title="notation">max</span></a> <span class="id" title="var">P</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#037a06093aea0e31650c64484aec1c53"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Sylow.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#3a9af5e9c8e28731812c4cca2f61ee29"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#3a9af5e9c8e28731812c4cca2f61ee29"><span class="id" title="notation">subgroup</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#3a9af5e9c8e28731812c4cca2f61ee29"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#Sylow.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#3a9af5e9c8e28731812c4cca2f61ee29"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#037a06093aea0e31650c64484aec1c53"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Sylow.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">Sylow</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#Sylow.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ca13a32469ebe56c9f4cc99d00e8eeba"><span class="id" title="notation">,</span></a><br/> + <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">transitive</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Sylow.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.pgroup.html#8a27e24770f969db823c8b5e38beee12"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#8a27e24770f969db823c8b5e38beee12"><span class="id" title="notation">Syl_p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#8a27e24770f969db823c8b5e38beee12"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#Sylow.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#8a27e24770f969db823c8b5e38beee12"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.action.html#cdd023ccc2efe92dd3cc3bafec9e78af"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#cdd023ccc2efe92dd3cc3bafec9e78af"><span class="id" title="notation">JG</span></a><a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ca13a32469ebe56c9f4cc99d00e8eeba"><span class="id" title="notation">,</span></a><br/> + <span class="id" title="keyword">∀</span> <span class="id" title="var">P</span>, <a class="idref" href="mathcomp.solvable.sylow.html#Sylow.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">Sylow</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#Sylow.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#8a27e24770f969db823c8b5e38beee12"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#8a27e24770f969db823c8b5e38beee12"><span class="id" title="notation">Syl_p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#8a27e24770f969db823c8b5e38beee12"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#Sylow.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#8a27e24770f969db823c8b5e38beee12"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.sylow.html#Sylow.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7193b23d12b4f3c2146b0e77ee974b2b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#7193b23d12b4f3c2146b0e77ee974b2b"><span class="id" title="notation">N_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#7193b23d12b4f3c2146b0e77ee974b2b"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#7193b23d12b4f3c2146b0e77ee974b2b"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">|</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ca13a32469ebe56c9f4cc99d00e8eeba"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.ssreflect.prime.html#prime"><span class="id" title="definition">prime</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Sylow.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#8a27e24770f969db823c8b5e38beee12"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#8a27e24770f969db823c8b5e38beee12"><span class="id" title="notation">Syl_p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#8a27e24770f969db823c8b5e38beee12"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#Sylow.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#8a27e24770f969db823c8b5e38beee12"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#2179ac53e82aa7c0b2f2f5a16b5510ea"><span class="id" title="notation">%%</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Sylow.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 1%<span class="id" title="var">N</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ca13a32469ebe56c9f4cc99d00e8eeba"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="max_pgroup_Sylow"><span class="id" title="lemma">max_pgroup_Sylow</span></a> <span class="id" title="var">P</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#037a06093aea0e31650c64484aec1c53"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#037a06093aea0e31650c64484aec1c53"><span class="id" title="notation">max</span></a> <span class="id" title="var">P</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#037a06093aea0e31650c64484aec1c53"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Sylow.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#3a9af5e9c8e28731812c4cca2f61ee29"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#3a9af5e9c8e28731812c4cca2f61ee29"><span class="id" title="notation">subgroup</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#3a9af5e9c8e28731812c4cca2f61ee29"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#Sylow.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#3a9af5e9c8e28731812c4cca2f61ee29"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#037a06093aea0e31650c64484aec1c53"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Sylow.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">Sylow</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#Sylow.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Sylow_superset"><span class="id" title="lemma">Sylow_superset</span></a> <span class="id" title="var">Q</span> :<br/> + <a class="idref" href="mathcomp.solvable.sylow.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Sylow.G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Sylow.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">{</span></a><span class="id" title="var">P</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Sylow.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Sylow.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">Sylow</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#Sylow.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#602b9943a639fb973abed6e2c7854421"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Sylow_exists"><span class="id" title="lemma">Sylow_exists</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">{</span></a><span class="id" title="var">P</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Sylow.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Sylow.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">Sylow</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#Sylow.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Syl_trans"><span class="id" title="lemma">Syl_trans</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">transitive</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Sylow.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.pgroup.html#8a27e24770f969db823c8b5e38beee12"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#8a27e24770f969db823c8b5e38beee12"><span class="id" title="notation">Syl_p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#8a27e24770f969db823c8b5e38beee12"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#Sylow.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#8a27e24770f969db823c8b5e38beee12"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.action.html#cdd023ccc2efe92dd3cc3bafec9e78af"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#cdd023ccc2efe92dd3cc3bafec9e78af"><span class="id" title="notation">JG</span></a><a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Sylow_trans"><span class="id" title="lemma">Sylow_trans</span></a> <span class="id" title="var">P</span> <span class="id" title="var">Q</span> :<br/> + <a class="idref" href="mathcomp.solvable.sylow.html#Sylow.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">Sylow</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#Sylow.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Sylow.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">Sylow</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#Sylow.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Sylow.G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#67291ec55239f54fa5aa0b0bb974446c"><span class="id" title="notation">:=:</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1deb3845cf16de446ae6619879e9d6db"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Sylow_subJ"><span class="id" title="lemma">Sylow_subJ</span></a> <span class="id" title="var">P</span> <span class="id" title="var">Q</span> :<br/> + <a class="idref" href="mathcomp.solvable.sylow.html#Sylow.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">Sylow</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#Sylow.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Sylow.G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Sylow.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Sylow.G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1deb3845cf16de446ae6619879e9d6db"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Sylow_Jsub"><span class="id" title="lemma">Sylow_Jsub</span></a> <span class="id" title="var">P</span> <span class="id" title="var">Q</span> :<br/> + <a class="idref" href="mathcomp.solvable.sylow.html#Sylow.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">Sylow</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#Sylow.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Sylow.G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Sylow.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Sylow.G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1deb3845cf16de446ae6619879e9d6db"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="card_Syl"><span class="id" title="lemma">card_Syl</span></a> <span class="id" title="var">P</span> : <a class="idref" href="mathcomp.solvable.sylow.html#Sylow.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">Sylow</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#Sylow.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#8a27e24770f969db823c8b5e38beee12"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#8a27e24770f969db823c8b5e38beee12"><span class="id" title="notation">Syl_p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#8a27e24770f969db823c8b5e38beee12"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#Sylow.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#8a27e24770f969db823c8b5e38beee12"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.sylow.html#Sylow.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7193b23d12b4f3c2146b0e77ee974b2b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#7193b23d12b4f3c2146b0e77ee974b2b"><span class="id" title="notation">N_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#7193b23d12b4f3c2146b0e77ee974b2b"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#7193b23d12b4f3c2146b0e77ee974b2b"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">|</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="card_Syl_dvd"><span class="id" title="lemma">card_Syl_dvd</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#8a27e24770f969db823c8b5e38beee12"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#8a27e24770f969db823c8b5e38beee12"><span class="id" title="notation">Syl_p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#8a27e24770f969db823c8b5e38beee12"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#Sylow.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#8a27e24770f969db823c8b5e38beee12"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#aa34fd1c61c5cf0a3356b624a5d2afed"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.sylow.html#Sylow.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="card_Syl_mod"><span class="id" title="lemma">card_Syl_mod</span></a> : <a class="idref" href="mathcomp.ssreflect.prime.html#prime"><span class="id" title="definition">prime</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Sylow.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#8a27e24770f969db823c8b5e38beee12"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#8a27e24770f969db823c8b5e38beee12"><span class="id" title="notation">Syl_p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#8a27e24770f969db823c8b5e38beee12"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#Sylow.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#8a27e24770f969db823c8b5e38beee12"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#2179ac53e82aa7c0b2f2f5a16b5510ea"><span class="id" title="notation">%%</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Sylow.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 1%<span class="id" title="var">N</span>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Frattini_arg"><span class="id" title="lemma">Frattini_arg</span></a> <span class="id" title="var">H</span> <span class="id" title="var">P</span> : <a class="idref" href="mathcomp.solvable.sylow.html#Sylow.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#c27c638e534bbb5b7de2d4b4aa0a3e82"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Sylow.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">Sylow</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#Sylow.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Sylow.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7193b23d12b4f3c2146b0e77ee974b2b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#7193b23d12b4f3c2146b0e77ee974b2b"><span class="id" title="notation">N_H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#7193b23d12b4f3c2146b0e77ee974b2b"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#7193b23d12b4f3c2146b0e77ee974b2b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#H"><span class="id" title="variable">H</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.sylow.html#Sylow"><span class="id" title="section">Sylow</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="MoreSylow"><span class="id" title="section">MoreSylow</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="MoreSylow.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="MoreSylow.p"><span class="id" title="variable">p</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>).<br/> +<span class="id" title="keyword">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">P</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#MoreSylow.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Sylow_setI_normal"><span class="id" title="lemma">Sylow_setI_normal</span></a> <span class="id" title="var">G</span> <span class="id" title="var">H</span> <span class="id" title="var">P</span> :<br/> + <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#c27c638e534bbb5b7de2d4b4aa0a3e82"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#MoreSylow.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">Sylow</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#MoreSylow.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">Sylow</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">)</span></a> (<a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#cb41714a5a23482f7a48a98975fa8c59"><span class="id" title="notation">:&:</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="normal_sylowP"><span class="id" title="lemma">normal_sylowP</span></a> <span class="id" title="var">G</span> :<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#fe60c20831f772c0c3c288abf68cc42a"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">P</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#fe60c20831f772c0c3c288abf68cc42a"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#MoreSylow.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#fe60c20831f772c0c3c288abf68cc42a"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#MoreSylow.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">Sylow</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#fe60c20831f772c0c3c288abf68cc42a"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#c27c638e534bbb5b7de2d4b4aa0a3e82"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a>)<br/> + (<a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#8a27e24770f969db823c8b5e38beee12"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#8a27e24770f969db823c8b5e38beee12"><span class="id" title="notation">Syl_p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#8a27e24770f969db823c8b5e38beee12"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#8a27e24770f969db823c8b5e38beee12"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> 1%<span class="id" title="var">N</span>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="trivg_center_pgroup"><span class="id" title="lemma">trivg_center_pgroup</span></a> <span class="id" title="var">P</span> : <a class="idref" href="mathcomp.solvable.sylow.html#MoreSylow.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#67291ec55239f54fa5aa0b0bb974446c"><span class="id" title="notation">:=:</span></a> 1.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="p2group_abelian"><span class="id" title="lemma">p2group_abelian</span></a> <span class="id" title="var">P</span> : <a class="idref" href="mathcomp.solvable.sylow.html#MoreSylow.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.prime.html#logn"><span class="id" title="definition">logn</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#MoreSylow.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9b077c369e19739ef880736ba34623ff"><span class="id" title="notation">≤</span></a> 2 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#abelian"><span class="id" title="definition">abelian</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="card_p2group_abelian"><span class="id" title="lemma">card_p2group_abelian</span></a> <span class="id" title="var">P</span> : <a class="idref" href="mathcomp.ssreflect.prime.html#prime"><span class="id" title="definition">prime</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#MoreSylow.p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="mathcomp.solvable.sylow.html#MoreSylow.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> 2)%<span class="id" title="var">N</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#abelian"><span class="id" title="definition">abelian</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Sylow_transversal_gen"><span class="id" title="lemma">Sylow_transversal_gen</span></a> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#MoreSylow.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a>) <span class="id" title="var">G</span> :<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a><span class="id" title="keyword">∀</span> <span class="id" title="var">P</span>, <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a><span class="id" title="keyword">∀</span> <span class="id" title="var">p</span>, <a class="idref" href="mathcomp.solvable.sylow.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.prime.html#041d58b37e83f44180445b7edc4ecdfd"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#041d58b37e83f44180445b7edc4ecdfd"><span class="id" title="notation">pi</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#041d58b37e83f44180445b7edc4ecdfd"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#041d58b37e83f44180445b7edc4ecdfd"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">P</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">Sylow</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.fingroup.fingroup.html#d2263119ac2870c795428c0a326d9d52"><span class="id" title="notation"><<</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#a0ae9f9e02e9c4d0ab32386f734fed5a"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#a0ae9f9e02e9c4d0ab32386f734fed5a"><span class="id" title="notation">bigcup_</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#a0ae9f9e02e9c4d0ab32386f734fed5a"><span class="id" title="notation">(</span></a><span class="id" title="var">P</span> <a class="idref" href="mathcomp.ssreflect.finset.html#a0ae9f9e02e9c4d0ab32386f734fed5a"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#a0ae9f9e02e9c4d0ab32386f734fed5a"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#d2263119ac2870c795428c0a326d9d52"><span class="id" title="notation">>></span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Sylow_gen"><span class="id" title="lemma">Sylow_gen</span></a> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#d2263119ac2870c795428c0a326d9d52"><span class="id" title="notation"><<</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#42a3c58c295a1e2bb6c61df38939e388"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#42a3c58c295a1e2bb6c61df38939e388"><span class="id" title="notation">bigcup_</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#42a3c58c295a1e2bb6c61df38939e388"><span class="id" title="notation">(</span></a><span class="id" title="var">P</span> <a class="idref" href="mathcomp.ssreflect.finset.html#42a3c58c295a1e2bb6c61df38939e388"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#MoreSylow.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#42a3c58c295a1e2bb6c61df38939e388"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.pgroup.html#Sylow"><span class="id" title="definition">Sylow</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#42a3c58c295a1e2bb6c61df38939e388"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d2263119ac2870c795428c0a326d9d52"><span class="id" title="notation">>></span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.sylow.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.sylow.html#MoreSylow"><span class="id" title="section">MoreSylow</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="SomeHall"><span class="id" title="section">SomeHall</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variable</span> <a name="SomeHall.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">p</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<span class="id" title="var">pi</span> : <a class="idref" href="mathcomp.ssreflect.prime.html#nat_pred"><span class="id" title="definition">nat_pred</span></a>) (<span class="id" title="var">G</span> <span class="id" title="var">H</span> <span class="id" title="var">K</span> <span class="id" title="var">P</span> <span class="id" title="var">R</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#SomeHall.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Hall_pJsub"><span class="id" title="lemma">Hall_pJsub</span></a> <span class="id" title="var">p</span> <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">P</span> :<br/> + <a class="idref" href="mathcomp.solvable.sylow.html#pi"><span class="id" title="variable">pi</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#d5534ad0d60aaeab355c10fe84cd2504"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#d5534ad0d60aaeab355c10fe84cd2504"><span class="id" title="notation">Hall</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#d5534ad0d60aaeab355c10fe84cd2504"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#d5534ad0d60aaeab355c10fe84cd2504"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#pi"><span class="id" title="variable">pi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1deb3845cf16de446ae6619879e9d6db"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#H"><span class="id" title="variable">H</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Hall_psubJ"><span class="id" title="lemma">Hall_psubJ</span></a> <span class="id" title="var">p</span> <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">P</span> :<br/> + <a class="idref" href="mathcomp.solvable.sylow.html#pi"><span class="id" title="variable">pi</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#d5534ad0d60aaeab355c10fe84cd2504"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#d5534ad0d60aaeab355c10fe84cd2504"><span class="id" title="notation">Hall</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#d5534ad0d60aaeab355c10fe84cd2504"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#d5534ad0d60aaeab355c10fe84cd2504"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#pi"><span class="id" title="variable">pi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1deb3845cf16de446ae6619879e9d6db"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Hall_setI_normal"><span class="id" title="lemma">Hall_setI_normal</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> :<br/> + <a class="idref" href="mathcomp.solvable.sylow.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#c27c638e534bbb5b7de2d4b4aa0a3e82"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#pi"><span class="id" title="variable">pi</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#d5534ad0d60aaeab355c10fe84cd2504"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#d5534ad0d60aaeab355c10fe84cd2504"><span class="id" title="notation">Hall</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#d5534ad0d60aaeab355c10fe84cd2504"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#d5534ad0d60aaeab355c10fe84cd2504"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#pi"><span class="id" title="variable">pi</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#d5534ad0d60aaeab355c10fe84cd2504"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#d5534ad0d60aaeab355c10fe84cd2504"><span class="id" title="notation">Hall</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#d5534ad0d60aaeab355c10fe84cd2504"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#d5534ad0d60aaeab355c10fe84cd2504"><span class="id" title="notation">)</span></a> (<a class="idref" href="mathcomp.solvable.sylow.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#cb41714a5a23482f7a48a98975fa8c59"><span class="id" title="notation">:&:</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#K"><span class="id" title="variable">K</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="coprime_mulG_setI_norm"><span class="id" title="lemma">coprime_mulG_setI_norm</span></a> <span class="id" title="var">H</span> <span class="id" title="var">G</span> <span class="id" title="var">K</span> <span class="id" title="var">R</span> :<br/> + <a class="idref" href="mathcomp.solvable.sylow.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#R"><span class="id" title="variable">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <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#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.sylow.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.sylow.html#R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#cb41714a5a23482f7a48a98975fa8c59"><span class="id" title="notation">:&:</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#R"><span class="id" title="variable">R</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#cb41714a5a23482f7a48a98975fa8c59"><span class="id" title="notation">:&:</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#cb41714a5a23482f7a48a98975fa8c59"><span class="id" title="notation">:&:</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#H"><span class="id" title="variable">H</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.sylow.html#SomeHall"><span class="id" title="section">SomeHall</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="Nilpotent"><span class="id" title="section">Nilpotent</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variable</span> <a name="Nilpotent.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">P</span> <span class="id" title="var">L</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Nilpotent.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">p</span> <span class="id" title="var">q</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="pgroup_nil"><span class="id" title="lemma">pgroup_nil</span></a> <span class="id" title="var">p</span> <span class="id" title="var">P</span> : <a class="idref" href="mathcomp.solvable.sylow.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.nilpotent.html#nilpotent"><span class="id" title="definition">nilpotent</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="pgroup_sol"><span class="id" title="lemma">pgroup_sol</span></a> <span class="id" title="var">p</span> <span class="id" title="var">P</span> : <a class="idref" href="mathcomp.solvable.sylow.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.nilpotent.html#solvable"><span class="id" title="definition">solvable</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="small_nil_class"><span class="id" title="lemma">small_nil_class</span></a> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.solvable.nilpotent.html#nil_class"><span class="id" title="definition">nil_class</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9b077c369e19739ef880736ba34623ff"><span class="id" title="notation">≤</span></a> 5 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.nilpotent.html#nilpotent"><span class="id" title="definition">nilpotent</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="nil_class2"><span class="id" title="lemma">nil_class2</span></a> <span class="id" title="var">G</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.nilpotent.html#nil_class"><span class="id" title="definition">nil_class</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9b077c369e19739ef880736ba34623ff"><span class="id" title="notation">≤</span></a> 2<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><span class="id" title="notation">^`(</span></a>1<a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="nil_class3"><span class="id" title="lemma">nil_class3</span></a> <span class="id" title="var">G</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.nilpotent.html#nil_class"><span class="id" title="definition">nil_class</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9b077c369e19739ef880736ba34623ff"><span class="id" title="notation">≤</span></a> 3<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.nilpotent.html#5687e496745f33fbd379209c74c3e54b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.nilpotent.html#5687e496745f33fbd379209c74c3e54b"><span class="id" title="notation">L_3</span></a><a class="idref" href="mathcomp.solvable.nilpotent.html#5687e496745f33fbd379209c74c3e54b"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.nilpotent.html#5687e496745f33fbd379209c74c3e54b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="nilpotent_maxp_normal"><span class="id" title="lemma">nilpotent_maxp_normal</span></a> <span class="id" title="var">pi</span> <span class="id" title="var">G</span> <span class="id" title="var">H</span> :<br/> + <a class="idref" href="mathcomp.solvable.nilpotent.html#nilpotent"><span class="id" title="definition">nilpotent</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#037a06093aea0e31650c64484aec1c53"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#037a06093aea0e31650c64484aec1c53"><span class="id" title="notation">max</span></a> <span class="id" title="var">H</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#037a06093aea0e31650c64484aec1c53"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#pi"><span class="id" title="variable">pi</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#3a9af5e9c8e28731812c4cca2f61ee29"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#3a9af5e9c8e28731812c4cca2f61ee29"><span class="id" title="notation">subgroup</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#3a9af5e9c8e28731812c4cca2f61ee29"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#3a9af5e9c8e28731812c4cca2f61ee29"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#037a06093aea0e31650c64484aec1c53"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#c27c638e534bbb5b7de2d4b4aa0a3e82"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="nilpotent_Hall_pcore"><span class="id" title="lemma">nilpotent_Hall_pcore</span></a> <span class="id" title="var">pi</span> <span class="id" title="var">G</span> <span class="id" title="var">H</span> :<br/> + <a class="idref" href="mathcomp.solvable.nilpotent.html#nilpotent"><span class="id" title="definition">nilpotent</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#pi"><span class="id" title="variable">pi</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#d5534ad0d60aaeab355c10fe84cd2504"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#d5534ad0d60aaeab355c10fe84cd2504"><span class="id" title="notation">Hall</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#d5534ad0d60aaeab355c10fe84cd2504"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#d5534ad0d60aaeab355c10fe84cd2504"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#67291ec55239f54fa5aa0b0bb974446c"><span class="id" title="notation">:=:</span></a> <a class="idref" href="mathcomp.solvable.pgroup.html#5a60f5e4463d132504644978fbcd8502"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5a60f5e4463d132504644978fbcd8502"><span class="id" title="notation">O_pi</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5a60f5e4463d132504644978fbcd8502"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5a60f5e4463d132504644978fbcd8502"><span class="id" title="notation">)</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="nilpotent_pcore_Hall"><span class="id" title="lemma">nilpotent_pcore_Hall</span></a> <span class="id" title="var">pi</span> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.solvable.nilpotent.html#nilpotent"><span class="id" title="definition">nilpotent</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#pi"><span class="id" title="variable">pi</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#d5534ad0d60aaeab355c10fe84cd2504"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#d5534ad0d60aaeab355c10fe84cd2504"><span class="id" title="notation">Hall</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#d5534ad0d60aaeab355c10fe84cd2504"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#d5534ad0d60aaeab355c10fe84cd2504"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.pgroup.html#5a60f5e4463d132504644978fbcd8502"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5a60f5e4463d132504644978fbcd8502"><span class="id" title="notation">O_pi</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5a60f5e4463d132504644978fbcd8502"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5a60f5e4463d132504644978fbcd8502"><span class="id" title="notation">)</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="nilpotent_pcoreC"><span class="id" title="lemma">nilpotent_pcoreC</span></a> <span class="id" title="var">pi</span> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.solvable.nilpotent.html#nilpotent"><span class="id" title="definition">nilpotent</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.pgroup.html#5a60f5e4463d132504644978fbcd8502"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5a60f5e4463d132504644978fbcd8502"><span class="id" title="notation">O_pi</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5a60f5e4463d132504644978fbcd8502"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5a60f5e4463d132504644978fbcd8502"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#3733c0e43956ad2062ab5f1e57ceb9a8"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.gproduct.html#3733c0e43956ad2062ab5f1e57ceb9a8"><span class="id" title="notation">x</span></a> <a class="idref" href="mathcomp.solvable.pgroup.html#5a60f5e4463d132504644978fbcd8502"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5a60f5e4463d132504644978fbcd8502"><span class="id" title="notation">O_pi</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#233366c70a33ee49ba3eedb41626d66a"><span class="id" title="notation">^'</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5a60f5e4463d132504644978fbcd8502"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5a60f5e4463d132504644978fbcd8502"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="sub_nilpotent_cent2"><span class="id" title="lemma">sub_nilpotent_cent2</span></a> <span class="id" title="var">H</span> <span class="id" title="var">K</span> <span class="id" title="var">G</span> :<br/> + <a class="idref" href="mathcomp.solvable.nilpotent.html#nilpotent"><span class="id" title="definition">nilpotent</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.sylow.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.sylow.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.solvable.sylow.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#67c26168baa7671aab03da2a0fb7dafa"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#67c26168baa7671aab03da2a0fb7dafa"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#67c26168baa7671aab03da2a0fb7dafa"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#67c26168baa7671aab03da2a0fb7dafa"><span class="id" title="notation">)</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="pi_center_nilpotent"><span class="id" title="lemma">pi_center_nilpotent</span></a> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.solvable.nilpotent.html#nilpotent"><span class="id" title="definition">nilpotent</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.prime.html#041d58b37e83f44180445b7edc4ecdfd"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#041d58b37e83f44180445b7edc4ecdfd"><span class="id" title="notation">pi</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#041d58b37e83f44180445b7edc4ecdfd"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#041d58b37e83f44180445b7edc4ecdfd"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.prime.html#041d58b37e83f44180445b7edc4ecdfd"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#041d58b37e83f44180445b7edc4ecdfd"><span class="id" title="notation">pi</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#041d58b37e83f44180445b7edc4ecdfd"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#041d58b37e83f44180445b7edc4ecdfd"><span class="id" title="notation">)</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Sylow_subnorm"><span class="id" title="lemma">Sylow_subnorm</span></a> <span class="id" title="var">p</span> <span class="id" title="var">G</span> <span class="id" title="var">P</span> : <a class="idref" href="mathcomp.solvable.sylow.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">Sylow</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#7193b23d12b4f3c2146b0e77ee974b2b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#7193b23d12b4f3c2146b0e77ee974b2b"><span class="id" title="notation">N_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#7193b23d12b4f3c2146b0e77ee974b2b"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#7193b23d12b4f3c2146b0e77ee974b2b"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">Sylow</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#43f075314fcfccdaa8a5813debe2d9ed"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.sylow.html#Nilpotent"><span class="id" title="section">Nilpotent</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="nil_class_pgroup"><span class="id" title="lemma">nil_class_pgroup</span></a> (<span class="id" title="var">gT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<span class="id" title="var">p</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<span class="id" title="var">P</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) :<br/> + <a class="idref" href="mathcomp.solvable.sylow.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.nilpotent.html#nil_class"><span class="id" title="definition">nil_class</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9b077c369e19739ef880736ba34623ff"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#maxn"><span class="id" title="definition">maxn</span></a> 1 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#logn"><span class="id" title="definition">logn</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><span class="id" title="notation">).-1</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="Zgroup"><span class="id" title="definition">Zgroup</span></a> (<span class="id" title="var">gT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<span class="id" title="var">A</span> : <a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a>) :=<br/> + <a class="idref" href="mathcomp.ssreflect.fintype.html#fba75b5bf7a054f7244152ab0a960e30"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#fba75b5bf7a054f7244152ab0a960e30"><span class="id" title="notation">∀</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#fba75b5bf7a054f7244152ab0a960e30"><span class="id" title="notation">(</span></a><span class="id" title="var">V</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#fba75b5bf7a054f7244152ab0a960e30"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#fba75b5bf7a054f7244152ab0a960e30"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.pgroup.html#Sylow"><span class="id" title="definition">Sylow</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#V"><span class="id" title="variable">V</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#fba75b5bf7a054f7244152ab0a960e30"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#46e5a4123d46e6b126f7788a77176785"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.cyclic.html#cyclic"><span class="id" title="definition">cyclic</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#V"><span class="id" title="variable">V</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#fba75b5bf7a054f7244152ab0a960e30"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="Zgroups"><span class="id" title="section">Zgroups</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="Zgroups.gT"><span class="id" title="variable">gT</span></a> <a name="Zgroups.rT"><span class="id" title="variable">rT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<a name="Zgroups.D"><span class="id" title="variable">D</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<a name="Zgroups.f"><span class="id" title="variable">f</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.solvable.sylow.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">}</span></a>).<br/> +<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">G</span> <span class="id" title="var">H</span> <span class="id" title="var">K</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Zgroups.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="ZgroupS"><span class="id" title="lemma">ZgroupS</span></a> <span class="id" title="var">G</span> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.solvable.sylow.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Zgroup"><span class="id" title="definition">Zgroup</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Zgroup"><span class="id" title="definition">Zgroup</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#H"><span class="id" title="variable">H</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="morphim_Zgroup"><span class="id" title="lemma">morphim_Zgroup</span></a> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.solvable.sylow.html#Zgroup"><span class="id" title="definition">Zgroup</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Zgroup"><span class="id" title="definition">Zgroup</span></a> (<a class="idref" href="mathcomp.solvable.sylow.html#Zgroups.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="nil_Zgroup_cyclic"><span class="id" title="lemma">nil_Zgroup_cyclic</span></a> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.solvable.sylow.html#Zgroup"><span class="id" title="definition">Zgroup</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.nilpotent.html#nilpotent"><span class="id" title="definition">nilpotent</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.cyclic.html#cyclic"><span class="id" title="definition">cyclic</span></a> <a class="idref" href="mathcomp.solvable.sylow.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.sylow.html#Zgroups"><span class="id" title="section">Zgroups</span></a>.<br/> + +<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="NilPGroups"><span class="id" title="section">NilPGroups</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="NilPGroups.p"><span class="id" title="variable">p</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a name="NilPGroups.gT"><span class="id" title="variable">gT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>).<br/> +<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Type</span> <span class="id" title="var">G</span> <span class="id" title="var">P</span> <span class="id" title="var">N</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#NilPGroups.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +</div> + +<div class="doc"> + B & G 1.22 p.9 +</div> +<div class="code"> +<span class="id" title="keyword">Lemma</span> <a name="normal_pgroup"><span class="id" title="lemma">normal_pgroup</span></a> <span class="id" title="var">r</span> <span class="id" title="var">P</span> <span class="id" title="var">N</span> :<br/> + <a class="idref" href="mathcomp.solvable.sylow.html#NilPGroups.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#N"><span class="id" title="variable">N</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#c27c638e534bbb5b7de2d4b4aa0a3e82"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#r"><span class="id" title="variable">r</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9b077c369e19739ef880736ba34623ff"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.ssreflect.prime.html#logn"><span class="id" title="definition">logn</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#NilPGroups.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.sylow.html#N"><span class="id" title="variable">N</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">Q</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#NilPGroups.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">[/\</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#N"><span class="id" title="variable">N</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#c27c638e534bbb5b7de2d4b4aa0a3e82"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.sylow.html#Q"><span class="id" title="variable">Q</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="mathcomp.solvable.sylow.html#NilPGroups.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#r"><span class="id" title="variable">r</span></a>)%<span class="id" title="var">N</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Theorem</span> <a name="Baer_Suzuki"><span class="id" title="lemma">Baer_Suzuki</span></a> <span class="id" title="var">x</span> <span class="id" title="var">G</span> :<br/> + <a class="idref" href="mathcomp.solvable.sylow.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a><span class="id" title="keyword">∀</span> <span class="id" title="var">y</span>, <a class="idref" href="mathcomp.solvable.sylow.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#NilPGroups.p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5b9c9ef075a2fca9df30ee4ac4a1af18"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#d2263119ac2870c795428c0a326d9d52"><span class="id" title="notation"><<</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d251cae482ceced9589c8a2b3df261e7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d251cae482ceced9589c8a2b3df261e7"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d251cae482ceced9589c8a2b3df261e7"><span class="id" title="notation">;</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#808c6b8e35e792f23899f360a21e4638"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.solvable.sylow.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d251cae482ceced9589c8a2b3df261e7"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d2263119ac2870c795428c0a326d9d52"><span class="id" title="notation">>></span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.solvable.sylow.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.pgroup.html#5a60f5e4463d132504644978fbcd8502"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5a60f5e4463d132504644978fbcd8502"><span class="id" title="notation">O_p</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5a60f5e4463d132504644978fbcd8502"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.sylow.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.pgroup.html#5a60f5e4463d132504644978fbcd8502"><span class="id" title="notation">)</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.sylow.html#NilPGroups"><span class="id" title="section">NilPGroups</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 |