diff options
| author | Enrico Tassi | 2018-04-20 10:54:22 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-04-20 10:54:22 +0200 |
| commit | ed05182cece6bb3706e09b2ce14af4a41a2e8141 (patch) | |
| tree | e850d7314b6372d0476cf2ffaf7d3830721db7b1 /docs/htmldoc/mathcomp.solvable.commutator.html | |
| parent | 3d196f44681fb3b23ff8a79fbd44e12308680531 (diff) | |
generate the documentation for 1.7
Diffstat (limited to 'docs/htmldoc/mathcomp.solvable.commutator.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.solvable.commutator.html | 359 |
1 files changed, 359 insertions, 0 deletions
diff --git a/docs/htmldoc/mathcomp.solvable.commutator.html b/docs/htmldoc/mathcomp.solvable.commutator.html new file mode 100644 index 0000000..9da2584 --- /dev/null +++ b/docs/htmldoc/mathcomp.solvable.commutator.html @@ -0,0 +1,359 @@ +<!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">(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. <br/> + Distributed under the terms of CeCILL-B. *)</span><br/> +<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#"><span class="id" title="library">mathcomp.ssreflect.ssreflect</span></a>.<br/> + +<br/> +</div> + +<div class="doc"> + This 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 <| G /\ G / H abelian <-> 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/> + <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">"</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">"</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/> + <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"><*></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"><*></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"><|</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"><*></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/> + <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">:&:</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/> + <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/> + <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/> + <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"><|</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/> + <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/> + <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">&</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">&</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/> + <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/> + <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"><[</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">]></span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#80208730563aa86aa7861f6fe1b846da"><span class="id" title="notation"><*></span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#30152704c0ab4066186d0284456667e8"><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#30152704c0ab4066186d0284456667e8"><span class="id" title="notation">]></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/> + <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"><[</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">]></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/> + <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 & 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/> + <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/> + <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"><|</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"><|</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">>-></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/> + <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">&</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/> + <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>
\ No newline at end of file |