<!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.commutator</title>
</head>

<body>

<div id="page">

<div id="header">
</div>

<div id="main">

<h1 class="libtitle">Library mathcomp.solvable.commutator</h1>

<div class="code">
<span class="comment">(*&nbsp;(c)&nbsp;Copyright&nbsp;2006-2016&nbsp;Microsoft&nbsp;Corporation&nbsp;and&nbsp;Inria.&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br/>
&nbsp;Distributed&nbsp;under&nbsp;the&nbsp;terms&nbsp;of&nbsp;CeCILL-B.&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;*)</span><br/>
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#"><span class="id" title="library">mathcomp.ssreflect.ssreflect</span></a>.<br/>

<br/>
</div>

<div class="doc">
   This files contains the proofs of several key properties of commutators, 
 including the Hall-Witt identity and the Three Subgroup Lemma.             
   The definition and notation for both pointwise and set wise commutators  
 ( [~x, y, ... ] and [~: A, B ,... ], respectively) are given in fingroup.v    
 This file defines the derived group series:                                
           G^`(0) ==  G                                                     
       G^`(n.+1) == [~: G^`(n), G^`(n) ]                                     
 as several classical results involve the (first) derived group G^`(1),     
 such as the equivalence H &lt;| G /\ G / H abelian &lt;-&gt; G^`(1) \subset H.      
 The connection between the derived series and solvable groups will only be 
 established in nilpotent.v, however.                                        
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Set Implicit Arguments</span>.<br/>

<br/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">GroupScope</span>.<br/>

<br/>
<span class="id" title="keyword">Definition</span> <a name="derived_at_rec"><span class="id" title="definition">derived_at_rec</span></a> <span class="id" title="var">n</span> (<span class="id" title="var">gT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<span class="id" title="var">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.commutator.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/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.ssrnat.html#iter"><span class="id" title="definition">iter</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#n"><span class="id" title="variable">n</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">B</span> ⇒ <a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">]</span></a>) <a class="idref" href="mathcomp.solvable.commutator.html#A"><span class="id" title="variable">A</span></a>.<br/>

<br/>
</div>

<div class="doc">
 Note: 'nosimpl' MUST be used outside of a section -- the end of section   
 "cooking" destroys it.                                                     
</div>
<div class="code">
<span class="id" title="keyword">Definition</span> <a name="derived_at"><span class="id" title="definition">derived_at</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#nosimpl"><span class="id" title="abbreviation">nosimpl</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#derived_at_rec"><span class="id" title="definition">derived_at_rec</span></a>.<br/>

<br/>
<span class="id" title="keyword">Notation</span> <a name="2af6d4df4fd579da0e206aeed0c82e74"><span class="id" title="notation">&quot;</span></a>G ^` ( n )" := (<a class="idref" href="mathcomp.solvable.commutator.html#derived_at"><span class="id" title="definition">derived_at</span></a> <span class="id" title="var">n</span> <span class="id" title="var">G</span>) : <span class="id" title="var">group_scope</span>.<br/>

<br/>
<span class="id" title="keyword">Section</span> <a name="DerivedBasics"><span class="id" title="section">DerivedBasics</span></a>.<br/>

<br/>
<span class="id" title="keyword">Variables</span> <a name="DerivedBasics.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">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.commutator.html#DerivedBasics.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/>
<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <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.commutator.html#DerivedBasics.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="derg0"><span class="id" title="lemma">derg0</span></a> <span class="id" title="var">A</span> : <a class="idref" href="mathcomp.solvable.commutator.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><span class="id" title="notation">^`(</span></a>0<a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><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.commutator.html#A"><span class="id" title="variable">A</span></a>.  <br/>
<span class="id" title="keyword">Lemma</span> <a name="derg1"><span class="id" title="lemma">derg1</span></a> <span class="id" title="var">A</span> : <a class="idref" href="mathcomp.solvable.commutator.html#A"><span class="id" title="variable">A</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="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#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">]</span></a>.  <br/>
<span class="id" title="keyword">Lemma</span> <a name="dergSn"><span class="id" title="lemma">dergSn</span></a> <span class="id" title="var">n</span> <span class="id" title="var">A</span> : <a class="idref" href="mathcomp.solvable.commutator.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><span class="id" title="notation">^`(</span></a><a class="idref" href="mathcomp.solvable.commutator.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><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#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><span class="id" title="notation">^`(</span></a><a class="idref" href="mathcomp.solvable.commutator.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><span class="id" title="notation">^`(</span></a><a class="idref" href="mathcomp.solvable.commutator.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">]</span></a>.  <br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="der_group_set"><span class="id" title="lemma">der_group_set</span></a> <span class="id" title="var">G</span> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#group_set"><span class="id" title="definition">group_set</span></a> <a class="idref" href="mathcomp.solvable.commutator.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><a class="idref" href="mathcomp.solvable.commutator.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Canonical</span> <span class="id" title="var">derived_at_group</span> <span class="id" title="var">G</span> <span class="id" title="var">n</span> := <a class="idref" href="mathcomp.fingroup.fingroup.html#Group"><span class="id" title="constructor">Group</span></a> (<a class="idref" href="mathcomp.solvable.commutator.html#der_group_set"><span class="id" title="lemma">der_group_set</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#n"><span class="id" title="variable">n</span></a>).<br/>

<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.commutator.html#DerivedBasics"><span class="id" title="section">DerivedBasics</span></a>.<br/>

<br/>
<span class="id" title="keyword">Notation</span> <a name="2bc0280463935f973ff018e802d37115"><span class="id" title="notation">&quot;</span></a>G ^` ( n )" := (<a class="idref" href="mathcomp.solvable.commutator.html#derived_at_group"><span class="id" title="definition">derived_at_group</span></a> <span class="id" title="var">G</span> <span class="id" title="var">n</span>) : <span class="id" title="var">Group_scope</span>.<br/>

<br/>
<span class="id" title="keyword">Section</span> <a name="Basic_commutator_properties"><span class="id" title="section">Basic_commutator_properties</span></a>.<br/>

<br/>
<span class="id" title="keyword">Variable</span> <a name="Basic_commutator_properties.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">x</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span> : <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.gT"><span class="id" title="variable">gT</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="conjg_mulR"><span class="id" title="lemma">conjg_mulR</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.solvable.commutator.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.commutator.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#x"><span class="id" title="variable">x</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#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">]</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="conjg_Rmul"><span class="id" title="lemma">conjg_Rmul</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.solvable.commutator.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.commutator.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a605acbeae7597f74f5a9b816ed8a717"><span class="id" title="notation">^-1</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><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.commutator.html#x"><span class="id" title="variable">x</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="commMgJ"><span class="id" title="lemma">commMgJ</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#z"><span class="id" title="variable">z</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><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#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#z"><span class="id" title="variable">z</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#808c6b8e35e792f23899f360a21e4638"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#y"><span class="id" title="variable">y</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#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#z"><span class="id" title="variable">z</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">]</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="commgMJ"><span class="id" title="lemma">commgMJ</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#z"><span class="id" title="variable">z</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><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#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#z"><span class="id" title="variable">z</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><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#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#808c6b8e35e792f23899f360a21e4638"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#z"><span class="id" title="variable">z</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="commMgR"><span class="id" title="lemma">commMgR</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#z"><span class="id" title="variable">z</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><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#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#z"><span class="id" title="variable">z</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><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#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#z"><span class="id" title="variable">z</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><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#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#z"><span class="id" title="variable">z</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">]</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="commgMR"><span class="id" title="lemma">commgMR</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#z"><span class="id" title="variable">z</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><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#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#z"><span class="id" title="variable">z</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><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#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><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#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#z"><span class="id" title="variable">z</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">]</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="Hall_Witt_identity"><span class="id" title="lemma">Hall_Witt_identity</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span> :<br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a605acbeae7597f74f5a9b816ed8a717"><span class="id" title="notation">^-1</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#z"><span class="id" title="variable">z</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#808c6b8e35e792f23899f360a21e4638"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#y"><span class="id" title="variable">y</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#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#z"><span class="id" title="variable">z</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a605acbeae7597f74f5a9b816ed8a717"><span class="id" title="notation">^-1</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#808c6b8e35e792f23899f360a21e4638"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#z"><span class="id" title="variable">z</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#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#z"><span class="id" title="variable">z</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a605acbeae7597f74f5a9b816ed8a717"><span class="id" title="notation">^-1</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#808c6b8e35e792f23899f360a21e4638"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#x"><span class="id" title="variable">x</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/>
</div>

<div class="doc">
 the following properties are useful for studying p-groups of class 2  
</div>
<div class="code">

<br/>
<span class="id" title="keyword">Section</span> <a name="Basic_commutator_properties.LeftComm"><span class="id" title="section">LeftComm</span></a>.<br/>

<br/>
<span class="id" title="keyword">Variables</span> (<a name="Basic_commutator_properties.LeftComm.i"><span class="id" title="variable">i</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="Basic_commutator_properties.LeftComm.x"><span class="id" title="variable">x</span></a> <a name="Basic_commutator_properties.LeftComm.y"><span class="id" title="variable">y</span></a> : <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.gT"><span class="id" title="variable">gT</span></a>).<br/>
<span class="id" title="keyword">Hypothesis</span> <a name="Basic_commutator_properties.LeftComm.cxz"><span class="id" title="variable">cxz</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#commute"><span class="id" title="definition">commute</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftComm.x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftComm.x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftComm.y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">]</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="commVg"><span class="id" title="lemma">commVg</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftComm.x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a605acbeae7597f74f5a9b816ed8a717"><span class="id" title="notation">^-1</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftComm.y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><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#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftComm.x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftComm.y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a605acbeae7597f74f5a9b816ed8a717"><span class="id" title="notation">^-1</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="commXg"><span class="id" title="lemma">commXg</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftComm.x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#86a04fb564fb97d388cad84a3a204260"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftComm.i"><span class="id" title="variable">i</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftComm.y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><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#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftComm.x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftComm.y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#86a04fb564fb97d388cad84a3a204260"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftComm.i"><span class="id" title="variable">i</span></a>.<br/>

<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftComm"><span class="id" title="section">LeftComm</span></a>.<br/>

<br/>
<span class="id" title="keyword">Section</span> <a name="Basic_commutator_properties.RightComm"><span class="id" title="section">RightComm</span></a>.<br/>

<br/>
<span class="id" title="keyword">Variables</span> (<a name="Basic_commutator_properties.RightComm.i"><span class="id" title="variable">i</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="Basic_commutator_properties.RightComm.x"><span class="id" title="variable">x</span></a> <a name="Basic_commutator_properties.RightComm.y"><span class="id" title="variable">y</span></a> : <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.gT"><span class="id" title="variable">gT</span></a>).<br/>
<span class="id" title="keyword">Hypothesis</span> <a name="Basic_commutator_properties.RightComm.cyz"><span class="id" title="variable">cyz</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#commute"><span class="id" title="definition">commute</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.RightComm.y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.RightComm.x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.RightComm.y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">]</span></a>.<br/>
<span class="id" title="keyword">Let</span> <a name="Basic_commutator_properties.RightComm.cyz'"><span class="id" title="variable">cyz'</span></a> := <a class="idref" href="mathcomp.fingroup.fingroup.html#commuteV"><span class="id" title="lemma">commuteV</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.RightComm.cyz"><span class="id" title="variable">cyz</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="commgV"><span class="id" title="lemma">commgV</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.RightComm.x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.RightComm.y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a605acbeae7597f74f5a9b816ed8a717"><span class="id" title="notation">^-1</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><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#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.RightComm.x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.RightComm.y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a605acbeae7597f74f5a9b816ed8a717"><span class="id" title="notation">^-1</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="commgX"><span class="id" title="lemma">commgX</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.RightComm.x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.RightComm.y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#86a04fb564fb97d388cad84a3a204260"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.RightComm.i"><span class="id" title="variable">i</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><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#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.RightComm.x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.RightComm.y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#86a04fb564fb97d388cad84a3a204260"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.RightComm.i"><span class="id" title="variable">i</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.RightComm"><span class="id" title="section">RightComm</span></a>.<br/>

<br/>
<span class="id" title="keyword">Section</span> <a name="Basic_commutator_properties.LeftRightComm"><span class="id" title="section">LeftRightComm</span></a>.<br/>

<br/>
<span class="id" title="keyword">Variables</span> (<a name="Basic_commutator_properties.LeftRightComm.i"><span class="id" title="variable">i</span></a> <a name="Basic_commutator_properties.LeftRightComm.j"><span class="id" title="variable">j</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="Basic_commutator_properties.LeftRightComm.x"><span class="id" title="variable">x</span></a> <a name="Basic_commutator_properties.LeftRightComm.y"><span class="id" title="variable">y</span></a> : <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.gT"><span class="id" title="variable">gT</span></a>).<br/>
<span class="id" title="keyword">Hypotheses</span> (<a name="Basic_commutator_properties.LeftRightComm.cxz"><span class="id" title="variable">cxz</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#commute"><span class="id" title="definition">commute</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftRightComm.x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftRightComm.x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftRightComm.y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">]</span></a>) (<a name="Basic_commutator_properties.LeftRightComm.cyz"><span class="id" title="variable">cyz</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#commute"><span class="id" title="definition">commute</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftRightComm.y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftRightComm.x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftRightComm.y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">]</span></a>).<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="commXXg"><span class="id" title="lemma">commXXg</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftRightComm.x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#86a04fb564fb97d388cad84a3a204260"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftRightComm.i"><span class="id" title="variable">i</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftRightComm.y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#86a04fb564fb97d388cad84a3a204260"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftRightComm.j"><span class="id" title="variable">j</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><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#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftRightComm.x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftRightComm.y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#86a04fb564fb97d388cad84a3a204260"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#86a04fb564fb97d388cad84a3a204260"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftRightComm.i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftRightComm.j"><span class="id" title="variable">j</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#86a04fb564fb97d388cad84a3a204260"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="expMg_Rmul"><span class="id" title="lemma">expMg_Rmul</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#86a04fb564fb97d388cad84a3a204260"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftRightComm.y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftRightComm.x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#86a04fb564fb97d388cad84a3a204260"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#86a04fb564fb97d388cad84a3a204260"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftRightComm.i"><span class="id" title="variable">i</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.commutator.html#Basic_commutator_properties.LeftRightComm.y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#86a04fb564fb97d388cad84a3a204260"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftRightComm.i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftRightComm.x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#86a04fb564fb97d388cad84a3a204260"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftRightComm.i"><span class="id" title="variable">i</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#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftRightComm.x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftRightComm.y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#86a04fb564fb97d388cad84a3a204260"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftRightComm.i"><span class="id" title="variable">i</span></a><a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">,</span></a> 2<a class="idref" href="mathcomp.ssreflect.binomial.html#f55f24aacb42fe0283014d29bcccb8c2"><span class="id" title="notation">)</span></a>.<br/>

<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties.LeftRightComm"><span class="id" title="section">LeftRightComm</span></a>.<br/>

<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.commutator.html#Basic_commutator_properties"><span class="id" title="section">Basic_commutator_properties</span></a>.<br/>

<br/>
</div>

<div class="doc">
 Set theoretic commutators **** 
</div>
<div class="code">
<span class="id" title="keyword">Section</span> <a name="Commutator_properties"><span class="id" title="section">Commutator_properties</span></a>.<br/>

<br/>
<span class="id" title="keyword">Variable</span> <a name="Commutator_properties.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">rT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<span class="id" title="var">A</span> <span class="id" title="var">B</span> <span class="id" title="var">C</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.commutator.html#Commutator_properties.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>) (<span class="id" title="var">D</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.commutator.html#Commutator_properties.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="commG1"><span class="id" title="lemma">commG1</span></a> <span class="id" title="var">A</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> 1<a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><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">Lemma</span> <a name="comm1G"><span class="id" title="lemma">comm1G</span></a> <span class="id" title="var">A</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> 1<a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><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">Lemma</span> <a name="commg_sub"><span class="id" title="lemma">commg_sub</span></a> <span class="id" title="var">A</span> <span class="id" title="var">B</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><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.commutator.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#80208730563aa86aa7861f6fe1b846da"><span class="id" title="notation">&lt;*&gt;</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#B"><span class="id" title="variable">B</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="commg_norml"><span class="id" title="lemma">commg_norml</span></a> <span class="id" title="var">G</span> <span class="id" title="var">A</span> : <a class="idref" href="mathcomp.solvable.commutator.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.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">)</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="commg_normr"><span class="id" title="lemma">commg_normr</span></a> <span class="id" title="var">G</span> <span class="id" title="var">A</span> : <a class="idref" href="mathcomp.solvable.commutator.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.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="commg_norm"><span class="id" title="lemma">commg_norm</span></a> <span class="id" title="var">G</span> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.solvable.commutator.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#80208730563aa86aa7861f6fe1b846da"><span class="id" title="notation">&lt;*&gt;</span></a> <a class="idref" href="mathcomp.solvable.commutator.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#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.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="commg_normal"><span class="id" title="lemma">commg_normal</span></a> <span class="id" title="var">G</span> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#c27c638e534bbb5b7de2d4b4aa0a3e82"><span class="id" title="notation">&lt;|</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#80208730563aa86aa7861f6fe1b846da"><span class="id" title="notation">&lt;*&gt;</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#H"><span class="id" title="variable">H</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="normsRl"><span class="id" title="lemma">normsRl</span></a> <span class="id" title="var">A</span> <span class="id" title="var">G</span> <span class="id" title="var">B</span> : <a class="idref" href="mathcomp.solvable.commutator.html#A"><span class="id" title="variable">A</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.commutator.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.commutator.html#A"><span class="id" title="variable">A</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.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="normsRr"><span class="id" title="lemma">normsRr</span></a> <span class="id" title="var">A</span> <span class="id" title="var">G</span> <span class="id" title="var">B</span> : <a class="idref" href="mathcomp.solvable.commutator.html#A"><span class="id" title="variable">A</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.commutator.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.commutator.html#A"><span class="id" title="variable">A</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.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="commg_subr"><span class="id" title="lemma">commg_subr</span></a> <span class="id" title="var">G</span> <span class="id" title="var">H</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.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><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.commutator.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#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.commutator.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.commutator.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#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="commg_subl"><span class="id" title="lemma">commg_subl</span></a> <span class="id" title="var">G</span> <span class="id" title="var">H</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.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><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.commutator.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#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.commutator.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#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.commutator.html#G"><span class="id" title="variable">G</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#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="commg_subI"><span class="id" title="lemma">commg_subI</span></a> <span class="id" title="var">A</span> <span class="id" title="var">B</span> <span class="id" title="var">G</span> <span class="id" title="var">H</span> :<br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.commutator.html#A"><span class="id" title="variable">A</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#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.commutator.html#H"><span class="id" title="variable">H</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#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#B"><span class="id" title="variable">B</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#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.commutator.html#G"><span class="id" title="variable">G</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#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><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.commutator.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#cb41714a5a23482f7a48a98975fa8c59"><span class="id" title="notation">:&amp;:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#H"><span class="id" title="variable">H</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="quotient_cents2"><span class="id" title="lemma">quotient_cents2</span></a> <span class="id" title="var">A</span> <span class="id" title="var">B</span> <span class="id" title="var">K</span> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.commutator.html#A"><span class="id" title="variable">A</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.commutator.html#K"><span class="id" title="variable">K</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.solvable.commutator.html#B"><span class="id" title="variable">B</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.commutator.html#K"><span class="id" title="variable">K</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><br/>
&nbsp;&nbsp;<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.commutator.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#c7768147d2d560601601fbf95706ddcc"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.commutator.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.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.commutator.html#B"><span class="id" title="variable">B</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#c7768147d2d560601601fbf95706ddcc"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.commutator.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><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.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><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.commutator.html#K"><span class="id" title="variable">K</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="quotient_cents2r"><span class="id" title="lemma">quotient_cents2r</span></a> <span class="id" title="var">A</span> <span class="id" title="var">B</span> <span class="id" title="var">K</span> :<br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><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.commutator.html#K"><span class="id" title="variable">K</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#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.commutator.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#c7768147d2d560601601fbf95706ddcc"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.commutator.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">\</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.commutator.html#B"><span class="id" title="variable">B</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#c7768147d2d560601601fbf95706ddcc"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.commutator.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="sub_der1_norm"><span class="id" title="lemma">sub_der1_norm</span></a> <span class="id" title="var">G</span> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.solvable.commutator.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.commutator.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.commutator.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.commutator.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.commutator.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.commutator.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>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="sub_der1_normal"><span class="id" title="lemma">sub_der1_normal</span></a> <span class="id" title="var">G</span> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.solvable.commutator.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.commutator.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.commutator.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.commutator.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.commutator.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#c27c638e534bbb5b7de2d4b4aa0a3e82"><span class="id" title="notation">&lt;|</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#G"><span class="id" title="variable">G</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="sub_der1_abelian"><span class="id" title="lemma">sub_der1_abelian</span></a> <span class="id" title="var">G</span> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.solvable.commutator.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.commutator.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.fingroup.fingroup.html#abelian"><span class="id" title="definition">abelian</span></a> (<a class="idref" href="mathcomp.solvable.commutator.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#c7768147d2d560601601fbf95706ddcc"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#H"><span class="id" title="variable">H</span></a>).<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="der1_min"><span class="id" title="lemma">der1_min</span></a> <span class="id" title="var">G</span> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.solvable.commutator.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.commutator.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.fingroup.fingroup.html#abelian"><span class="id" title="definition">abelian</span></a> (<a class="idref" href="mathcomp.solvable.commutator.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#c7768147d2d560601601fbf95706ddcc"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.commutator.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.commutator.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.commutator.html#H"><span class="id" title="variable">H</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="der_abelian"><span class="id" title="lemma">der_abelian</span></a> <span class="id" title="var">n</span> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#abelian"><span class="id" title="definition">abelian</span></a> (<a class="idref" href="mathcomp.solvable.commutator.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><a class="idref" href="mathcomp.solvable.commutator.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#c7768147d2d560601601fbf95706ddcc"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.commutator.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><a class="idref" href="mathcomp.solvable.commutator.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><span class="id" title="notation">)</span></a>).<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="commg_normSl"><span class="id" title="lemma">commg_normSl</span></a> <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.solvable.commutator.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.commutator.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.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><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.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.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="commg_normSr"><span class="id" title="lemma">commg_normSr</span></a> <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.solvable.commutator.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.commutator.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.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><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.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.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="commMGr"><span class="id" title="lemma">commMGr</span></a> <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#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><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#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><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.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#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.solvable.commutator.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">]</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="commMG"><span class="id" title="lemma">commMG</span></a> <span class="id" title="var">G</span> <span class="id" title="var">H</span> <span class="id" title="var">K</span> :<br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.commutator.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#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.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">]</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.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#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.solvable.commutator.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><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#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><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#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">]</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="comm3G1P"><span class="id" title="lemma">comm3G1P</span></a> <span class="id" title="var">A</span> <span class="id" title="var">B</span> <span class="id" title="var">C</span> :<br/>
&nbsp;&nbsp;<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.ssr.ssrbool.html#772b6700b45aee6e187203386123c8a7"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#772b6700b45aee6e187203386123c8a7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#772b6700b45aee6e187203386123c8a7"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#B"><span class="id" title="variable">B</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#772b6700b45aee6e187203386123c8a7"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#C"><span class="id" title="variable">C</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#772b6700b45aee6e187203386123c8a7"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">h</span> <span class="id" title="var">k</span> <span class="id" title="var">l</span>, <a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#h"><span class="id" title="variable">h</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#k"><span class="id" title="variable">k</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#l"><span class="id" title="variable">l</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><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.ssr.ssrbool.html#772b6700b45aee6e187203386123c8a7"><span class="id" title="notation">}</span></a> (<a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#C"><span class="id" title="variable">C</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#24f47bb7b1a372904563d2bdb8a213a4"><span class="id" title="notation">:==:</span></a> 1).<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="three_subgroup"><span class="id" title="lemma">three_subgroup</span></a> <span class="id" title="var">G</span> <span class="id" title="var">H</span> <span class="id" title="var">K</span> :<br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#67291ec55239f54fa5aa0b0bb974446c"><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.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#67291ec55239f54fa5aa0b0bb974446c"><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.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">]</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="der1_joing_cycles"><span class="id" title="lemma">der1_joing_cycles</span></a> (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.solvable.commutator.html#Commutator_properties.gT"><span class="id" title="variable">gT</span></a>) : <br/>
&nbsp;&nbsp;<span class="id" title="keyword">let</span> <span class="id" title="var">XY</span> := <a class="idref" href="mathcomp.fingroup.fingroup.html#30152704c0ab4066186d0284456667e8"><span class="id" title="notation">&lt;[</span></a><a class="idref" href="mathcomp.solvable.commutator.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#30152704c0ab4066186d0284456667e8"><span class="id" title="notation">]&gt;</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#80208730563aa86aa7861f6fe1b846da"><span class="id" title="notation">&lt;*&gt;</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#30152704c0ab4066186d0284456667e8"><span class="id" title="notation">&lt;[</span></a><a class="idref" href="mathcomp.solvable.commutator.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#30152704c0ab4066186d0284456667e8"><span class="id" title="notation">]&gt;</span></a> <span class="id" title="tactic">in</span> <span class="id" title="keyword">let</span> <span class="id" title="var">xy</span> := <a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">]</span></a> <span class="id" title="tactic">in</span><br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.commutator.html#xy"><span class="id" title="variable">xy</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.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.commutator.html#XY"><span class="id" title="variable">XY</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#67c26168baa7671aab03da2a0fb7dafa"><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.commutator.html#XY"><span class="id" title="variable">XY</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="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#30152704c0ab4066186d0284456667e8"><span class="id" title="notation">&lt;[</span></a><a class="idref" href="mathcomp.solvable.commutator.html#xy"><span class="id" title="variable">xy</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#30152704c0ab4066186d0284456667e8"><span class="id" title="notation">]&gt;</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="commgAC"><span class="id" title="lemma">commgAC</span></a> <span class="id" title="var">G</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span> : <a class="idref" href="mathcomp.solvable.commutator.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.commutator.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.commutator.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.commutator.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.commutator.html#z"><span class="id" title="variable">z</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.commutator.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.fingroup.html#commute"><span class="id" title="definition">commute</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#z"><span class="id" title="variable">z</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#abelian"><span class="id" title="definition">abelian</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#b08e42f5c9c65aa9346e7b6dc26e3b5a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#b08e42f5c9c65aa9346e7b6dc26e3b5a"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#b08e42f5c9c65aa9346e7b6dc26e3b5a"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><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.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#z"><span class="id" title="variable">z</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><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#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#z"><span class="id" title="variable">z</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">]</span></a>.<br/>

<br/>
</div>

<div class="doc">
 Aschbacher, exercise 3.6 (used in proofs of Aschbacher 24.7 and B &amp; G 1.10  
</div>
<div class="code">
<span class="id" title="keyword">Lemma</span> <a name="comm_norm_cent_cent"><span class="id" title="lemma">comm_norm_cent_cent</span></a> <span class="id" title="var">H</span> <span class="id" title="var">G</span> <span class="id" title="var">K</span> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.commutator.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#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.commutator.html#G"><span class="id" title="variable">G</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.solvable.commutator.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.commutator.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> <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.commutator.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.commutator.html#K"><span class="id" title="variable">K</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><br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><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.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.commutator.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="charR"><span class="id" title="lemma">charR</span></a> <span class="id" title="var">H</span> <span class="id" title="var">K</span> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.solvable.commutator.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#004858100bfba9714bde1cdbce60358b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#004858100bfba9714bde1cdbce60358b"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.solvable.commutator.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.commutator.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#004858100bfba9714bde1cdbce60358b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#004858100bfba9714bde1cdbce60358b"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.solvable.commutator.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#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#004858100bfba9714bde1cdbce60358b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#004858100bfba9714bde1cdbce60358b"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#G"><span class="id" title="variable">G</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="der_char"><span class="id" title="lemma">der_char</span></a> <span class="id" title="var">n</span> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.solvable.commutator.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><a class="idref" href="mathcomp.solvable.commutator.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#004858100bfba9714bde1cdbce60358b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#004858100bfba9714bde1cdbce60358b"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#G"><span class="id" title="variable">G</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="der_sub"><span class="id" title="lemma">der_sub</span></a> <span class="id" title="var">n</span> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.solvable.commutator.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><a class="idref" href="mathcomp.solvable.commutator.html#n"><span class="id" title="variable">n</span></a><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.commutator.html#G"><span class="id" title="variable">G</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="der_norm"><span class="id" title="lemma">der_norm</span></a> <span class="id" title="var">n</span> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.solvable.commutator.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.commutator.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><a class="idref" href="mathcomp.solvable.commutator.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="der_normal"><span class="id" title="lemma">der_normal</span></a> <span class="id" title="var">n</span> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.solvable.commutator.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><a class="idref" href="mathcomp.solvable.commutator.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#c27c638e534bbb5b7de2d4b4aa0a3e82"><span class="id" title="notation">&lt;|</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#G"><span class="id" title="variable">G</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="der_subS"><span class="id" title="lemma">der_subS</span></a> <span class="id" title="var">n</span> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.solvable.commutator.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><a class="idref" href="mathcomp.solvable.commutator.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.solvable.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.commutator.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><a class="idref" href="mathcomp.solvable.commutator.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="der_normalS"><span class="id" title="lemma">der_normalS</span></a> <span class="id" title="var">n</span> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.solvable.commutator.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><a class="idref" href="mathcomp.solvable.commutator.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#c27c638e534bbb5b7de2d4b4aa0a3e82"><span class="id" title="notation">&lt;|</span></a> <a class="idref" href="mathcomp.solvable.commutator.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><a class="idref" href="mathcomp.solvable.commutator.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="morphim_der"><span class="id" title="lemma">morphim_der</span></a> <span class="id" title="var">rT</span> <span class="id" title="var">D</span> (<span class="id" title="var">f</span> : <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.commutator.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.commutator.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>) <span class="id" title="var">n</span> <span class="id" title="var">G</span> :<br/>
&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.commutator.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.solvable.commutator.html#D"><span class="id" title="variable">D</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.commutator.html#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.commutator.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><a class="idref" href="mathcomp.solvable.commutator.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><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.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.commutator.html#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.commutator.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><a class="idref" href="mathcomp.solvable.commutator.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><span class="id" title="notation">)</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="dergS"><span class="id" title="lemma">dergS</span></a> <span class="id" title="var">n</span> <span class="id" title="var">G</span> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.solvable.commutator.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.solvable.commutator.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.commutator.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><a class="idref" href="mathcomp.solvable.commutator.html#n"><span class="id" title="variable">n</span></a><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.commutator.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><span class="id" title="notation">^`(</span></a><a class="idref" href="mathcomp.solvable.commutator.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="quotient_der"><span class="id" title="lemma">quotient_der</span></a> <span class="id" title="var">n</span> <span class="id" title="var">G</span> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.solvable.commutator.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.commutator.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.solvable.commutator.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><a class="idref" href="mathcomp.solvable.commutator.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#c7768147d2d560601601fbf95706ddcc"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.commutator.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#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.commutator.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#c7768147d2d560601601fbf95706ddcc"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><span class="id" title="notation">)^`(</span></a><a class="idref" href="mathcomp.solvable.commutator.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="derJ"><span class="id" title="lemma">derJ</span></a> <span class="id" title="var">G</span> <span class="id" title="var">n</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.commutator.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1deb3845cf16de446ae6619879e9d6db"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><span class="id" title="notation">)^`(</span></a><a class="idref" href="mathcomp.solvable.commutator.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><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.commutator.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><a class="idref" href="mathcomp.solvable.commutator.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1deb3845cf16de446ae6619879e9d6db"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#x"><span class="id" title="variable">x</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="derG1P"><span class="id" title="lemma">derG1P</span></a> <span class="id" title="var">G</span> : <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="mathcomp.solvable.commutator.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="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="mathcomp.fingroup.fingroup.html#abelian"><span class="id" title="definition">abelian</span></a> <a class="idref" href="mathcomp.solvable.commutator.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.commutator.html#Commutator_properties"><span class="id" title="section">Commutator_properties</span></a>.<br/>

<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="der_cont"><span class="id" title="lemma">der_cont</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.continuous"><span class="id" title="definition">GFunctor.continuous</span></a> (<a class="idref" href="mathcomp.solvable.commutator.html#derived_at"><span class="id" title="definition">derived_at</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#n"><span class="id" title="variable">n</span></a>).<br/>
 
<br/>
<span class="id" title="keyword">Canonical</span> <span class="id" title="var">der_igFun</span> <span class="id" title="var">n</span> := <a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">igFun</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#der_sub"><span class="id" title="lemma">der_sub</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#8f28bbd804547edd8de802d63ef85617"><span class="id" title="notation">^~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#der_cont"><span class="id" title="lemma">der_cont</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">]</span></a>.<br/>
<span class="id" title="keyword">Canonical</span> <span class="id" title="var">der_gFun</span> <span class="id" title="var">n</span> := <a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">gFun</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#der_cont"><span class="id" title="lemma">der_cont</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">]</span></a>.<br/>
<span class="id" title="keyword">Canonical</span> <span class="id" title="var">der_mgFun</span> <span class="id" title="var">n</span> := <a class="idref" href="mathcomp.solvable.gfunctor.html#34d675edff20d6d91e43f305650662d9"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#34d675edff20d6d91e43f305650662d9"><span class="id" title="notation">mgFun</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#34d675edff20d6d91e43f305650662d9"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#dergS"><span class="id" title="lemma">dergS</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#8f28bbd804547edd8de802d63ef85617"><span class="id" title="notation">^~</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#34d675edff20d6d91e43f305650662d9"><span class="id" title="notation">]</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="isog_der"><span class="id" title="lemma">isog_der</span></a> (<span class="id" title="var">aT</span> <span class="id" title="var">rT</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">n</span> (<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.commutator.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>) (<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.commutator.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/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.commutator.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.commutator.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.commutator.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><a class="idref" href="mathcomp.solvable.commutator.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.commutator.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><span class="id" title="notation">^`(</span></a><a class="idref" href="mathcomp.solvable.commutator.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.commutator.html#2af6d4df4fd579da0e206aeed0c82e74"><span class="id" title="notation">)</span></a>.<br/>
 </div>
</div>

<div id="footer">
<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
</div>

</div>

</body>
</html>