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

<body>

<div id="page">

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

<div id="main">

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

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

<br/>
</div>

<div class="doc">
 Definition of the center of a group and of external central products:      
           'Z(G) == the center of the group G, i.e., 'C_G(G).               
   cprod_by isoZ == the finGroupType for the central product of H and K     
                    with centers identified by the isomorphism gz on 'Z(H); 
                    here isoZ : isom 'Z(H) 'Z(K) gz. Note that the actual   
                    central product is [set: cprod_by isoZ].                
    cpairg1 isoZ == the isomorphism from H to cprod_by isoZ, isoZ as above. 
    cpair1g isoZ == the isomorphism from K to cprod_by isoZ, isoZ as above. 
      xcprod H K == the finGroupType for the external central product of H  
                    and K with identified centers, provided the dynamically 
                    tested condition 'Z(H) \isog 'Z(K) holds.               
      ncprod H n == the finGroupType for the central product of n copies of 
                    H with their centers identified; [set: ncprod H 0] is   
                    isomorphic to 'Z(H).                                    
  xcprodm cf eqf == the morphism induced on cprod_by isoZ, where as above   
                    isoZ : isom 'Z(H) 'Z(K) gz, by fH : {morphism H &gt;-&gt; rT} 
                    and fK : {morphism K &gt;-&gt; rT}, given both                
                    cf : fH @* H \subset 'C(fK @* K) and                    
                    eqf : {in 'Z(H), fH =1 fK \o gz}.                       
   Following Aschbacher, we only provide external central products with     
 identified centers, as these are well defined provided the local center    
 isomorphism group of one of the subgroups is full. Nevertheless the        
 entire construction could be carried out under the weaker assumption that  
 gz is an isomorphism between subgroups of 'Z(H) and 'Z(K), and even the    
 uniqueness theorem holds under the weaker assumption that gz map 'Z(H) to  
 a characteristic subgroup of 'Z(K) not isomorphic to any other subgroup of 
 'Z(K), a condition that holds for example when K is cyclic, as in the      
 structure theorem for p-groups of symplectic type.                          
</div>
<div class="code">

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

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

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

<br/>
<span class="id" title="keyword">Variable</span> <a name="Defs.gT"><span class="id" title="variable">gT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>.<br/>

<br/>
<span class="id" title="keyword">Definition</span> <a name="center"><span class="id" title="definition">center</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.center.html#Defs.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>) := <a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">C_A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">)</span></a>.<br/>

<br/>
<span class="id" title="keyword">Canonical</span> <span class="id" title="var">center_group</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.center.html#Defs.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) : <a class="idref" href="mathcomp.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.center.html#Defs.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/>
&nbsp;&nbsp;<span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#ccb763a84253e971fd106aeeb9cd3cb0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ccb763a84253e971fd106aeeb9cd3cb0"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#ccb763a84253e971fd106aeeb9cd3cb0"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.center.html#center"><span class="id" title="definition">center</span></a> <a class="idref" href="mathcomp.solvable.center.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ccb763a84253e971fd106aeeb9cd3cb0"><span class="id" title="notation">]</span></a>.<br/>

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

<br/>
<span class="id" title="keyword">Notation</span> <a name="07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">&quot;</span></a>''Z' ( A )" := (<a class="idref" href="mathcomp.solvable.center.html#center"><span class="id" title="definition">center</span></a> <span class="id" title="var">A</span>) : <span class="id" title="var">group_scope</span>.<br/>
<span class="id" title="keyword">Notation</span> <a name="9990242b7e6de5c04ea1d8d95f316d83"><span class="id" title="notation">&quot;</span></a>''Z' ( H )" := (<a class="idref" href="mathcomp.solvable.center.html#center_group"><span class="id" title="definition">center_group</span></a> <span class="id" title="var">H</span>) : <span class="id" title="var">Group_scope</span>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="morphim_center"><span class="id" title="lemma">morphim_center</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pcontinuous"><span class="id" title="definition">GFunctor.pcontinuous</span></a> <a class="idref" href="mathcomp.solvable.center.html#center"><span class="id" title="definition">center</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Canonical</span> <span class="id" title="var">center_igFun</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> <span class="id" title="keyword">fun</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> ⇒ <a class="idref" href="mathcomp.ssreflect.finset.html#subsetIl"><span class="id" title="lemma">subsetIl</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.solvable.center.html#morphim_center"><span class="id" title="lemma">morphim_center</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">center_gFun</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.center.html#morphim_center"><span class="id" title="lemma">morphim_center</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">center_pgFun</span> := <a class="idref" href="mathcomp.solvable.gfunctor.html#75f5bf98333ce9930f3fc4415f01e6a0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#75f5bf98333ce9930f3fc4415f01e6a0"><span class="id" title="notation">pgFun</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#75f5bf98333ce9930f3fc4415f01e6a0"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.solvable.center.html#morphim_center"><span class="id" title="lemma">morphim_center</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#75f5bf98333ce9930f3fc4415f01e6a0"><span class="id" title="notation">]</span></a>.<br/>

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

<br/>
<span class="id" title="keyword">Variables</span> <a name="Center.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>.<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> : <a class="idref" href="mathcomp.solvable.center.html#Center.gT"><span class="id" title="variable">gT</span></a>) (<span class="id" title="var">A</span> <span class="id" title="var">B</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.center.html#Center.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">G</span> <span class="id" title="var">H</span> <span class="id" title="var">K</span> <span class="id" title="var">D</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.center.html#Center.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="subcentP"><span class="id" title="lemma">subcentP</span></a> <span class="id" title="var">A</span> <span class="id" title="var">B</span> <span class="id" title="var">x</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.center.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.center.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#centralises"><span class="id" title="definition">centralises</span></a> <a class="idref" href="mathcomp.solvable.center.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.solvable.center.html#B"><span class="id" title="variable">B</span></a>) (<a class="idref" href="mathcomp.solvable.center.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.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">C_A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">)</span></a>).<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="subcent_sub"><span class="id" title="lemma">subcent_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#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">C_A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><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#7193b23d12b4f3c2146b0e77ee974b2b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#7193b23d12b4f3c2146b0e77ee974b2b"><span class="id" title="notation">N_A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#7193b23d12b4f3c2146b0e77ee974b2b"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#7193b23d12b4f3c2146b0e77ee974b2b"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="subcent_norm"><span class="id" title="lemma">subcent_norm</span></a> <span class="id" title="var">G</span> <span class="id" title="var">B</span> : <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.center.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#7193b23d12b4f3c2146b0e77ee974b2b"><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#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><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="subcent_normal"><span class="id" title="lemma">subcent_normal</span></a> <span class="id" title="var">G</span> <span class="id" title="var">B</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#c27c638e534bbb5b7de2d4b4aa0a3e82"><span class="id" title="notation">&lt;|</span></a> <a class="idref" href="mathcomp.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.center.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#7193b23d12b4f3c2146b0e77ee974b2b"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="subcent_char"><span class="id" title="lemma">subcent_char</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.center.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.center.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.center.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.center.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#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">C_H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><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.center.html#G"><span class="id" title="variable">G</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="centerP"><span class="id" title="lemma">centerP</span></a> <span class="id" title="var">A</span> <span class="id" title="var">x</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.center.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.center.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#centralises"><span class="id" title="definition">centralises</span></a> <a class="idref" href="mathcomp.solvable.center.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.solvable.center.html#A"><span class="id" title="variable">A</span></a>) (<a class="idref" href="mathcomp.solvable.center.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.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a>).<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="center_sub"><span class="id" title="lemma">center_sub</span></a> <span class="id" title="var">A</span> : <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.center.html#A"><span class="id" title="variable">A</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="center1"><span class="id" title="lemma">center1</span></a> : <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a>1<a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#8f9364556521ebb498093f28eea2240f"><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#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:&gt;</span></a> <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.center.html#Center.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/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="centerC"><span class="id" title="lemma">centerC</span></a> <span class="id" title="var">A</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.center.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#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#centralised"><span class="id" title="definition">centralised</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="center_normal"><span class="id" title="lemma">center_normal</span></a> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#c27c638e534bbb5b7de2d4b4aa0a3e82"><span class="id" title="notation">&lt;|</span></a> <a class="idref" href="mathcomp.solvable.center.html#G"><span class="id" title="variable">G</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="sub_center_normal"><span class="id" title="lemma">sub_center_normal</span></a> <span class="id" title="var">H</span> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.solvable.center.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.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.center.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#c27c638e534bbb5b7de2d4b4aa0a3e82"><span class="id" title="notation">&lt;|</span></a> <a class="idref" href="mathcomp.solvable.center.html#G"><span class="id" title="variable">G</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="center_abelian"><span class="id" title="lemma">center_abelian</span></a> <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.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="center_char"><span class="id" title="lemma">center_char</span></a> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.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.center.html#G"><span class="id" title="variable">G</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="center_idP"><span class="id" title="lemma">center_idP</span></a> <span class="id" title="var">A</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.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#A"><span class="id" title="variable">A</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.center.html#A"><span class="id" title="variable">A</span></a>).<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="center_class_formula"><span class="id" title="lemma">center_class_formula</span></a> <span class="id" title="var">G</span> :<br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.center.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#b3eea360671e1b32b18a26e15b3aace3"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.ssreflect.bigop.html#537ae7c18e428d4642a9dfb8520f03ee"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#537ae7c18e428d4642a9dfb8520f03ee"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#537ae7c18e428d4642a9dfb8520f03ee"><span class="id" title="notation">(</span></a><span class="id" title="var">xG</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#537ae7c18e428d4642a9dfb8520f03ee"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#c4eb68ed64baca4028c54e8eaca3672a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#c4eb68ed64baca4028c54e8eaca3672a"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.center.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#30988ee242f08216f4b40cf90b42b816"><span class="id" title="notation">^:</span></a> <a class="idref" href="mathcomp.solvable.center.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#c4eb68ed64baca4028c54e8eaca3672a"><span class="id" title="notation">|</span></a> <span class="id" title="var">x</span> <a class="idref" href="mathcomp.ssreflect.finset.html#c4eb68ed64baca4028c54e8eaca3672a"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.center.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#1db838ba797020f3b39c07ed7167bc93"><span class="id" title="notation">:\:</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.center.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#67c26168baa7671aab03da2a0fb7dafa"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#c4eb68ed64baca4028c54e8eaca3672a"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#537ae7c18e428d4642a9dfb8520f03ee"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.center.html#xG"><span class="id" title="variable">xG</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="subcent1P"><span class="id" title="lemma">subcent1P</span></a> <span class="id" title="var">A</span> <span class="id" title="var">x</span> <span class="id" title="var">y</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.center.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.center.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</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.center.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.solvable.center.html#y"><span class="id" title="variable">y</span></a>) (<a class="idref" href="mathcomp.solvable.center.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.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">C_A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.center.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">]</span></a>).<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="subcent1_id"><span class="id" title="lemma">subcent1_id</span></a> <span class="id" title="var">x</span> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.solvable.center.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.center.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.center.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.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.center.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">]</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="subcent1_sub"><span class="id" title="lemma">subcent1_sub</span></a> <span class="id" title="var">x</span> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.center.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.center.html#G"><span class="id" title="variable">G</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="subcent1C"><span class="id" title="lemma">subcent1C</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.solvable.center.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.center.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.center.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.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.center.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><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.center.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.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.center.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">]</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="subcent1_cycle_sub"><span class="id" title="lemma">subcent1_cycle_sub</span></a> <span class="id" title="var">x</span> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.solvable.center.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.center.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#30152704c0ab4066186d0284456667e8"><span class="id" title="notation">&lt;[</span></a><a class="idref" href="mathcomp.solvable.center.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#30152704c0ab4066186d0284456667e8"><span class="id" title="notation">]&gt;</span></a> <a class="idref" href="mathcomp.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#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.center.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">]</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="subcent1_cycle_norm"><span class="id" title="lemma">subcent1_cycle_norm</span></a> <span class="id" title="var">x</span> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.center.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><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#30152704c0ab4066186d0284456667e8"><span class="id" title="notation">&lt;[</span></a><a class="idref" href="mathcomp.solvable.center.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#30152704c0ab4066186d0284456667e8"><span class="id" title="notation">]&gt;</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="subcent1_cycle_normal"><span class="id" title="lemma">subcent1_cycle_normal</span></a> <span class="id" title="var">x</span> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.solvable.center.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.center.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#30152704c0ab4066186d0284456667e8"><span class="id" title="notation">&lt;[</span></a><a class="idref" href="mathcomp.solvable.center.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#30152704c0ab4066186d0284456667e8"><span class="id" title="notation">]&gt;</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#c27c638e534bbb5b7de2d4b4aa0a3e82"><span class="id" title="notation">&lt;|</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.center.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">]</span></a>.<br/>

<br/>
</div>

<div class="doc">
 Gorenstein. 1.3.4  
</div>
<div class="code">
<span class="id" title="keyword">Lemma</span> <a name="cyclic_center_factor_abelian"><span class="id" title="lemma">cyclic_center_factor_abelian</span></a> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.solvable.cyclic.html#cyclic"><span class="id" title="definition">cyclic</span></a> (<a class="idref" href="mathcomp.solvable.center.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.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#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.center.html#G"><span class="id" title="variable">G</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="cyclic_factor_abelian"><span class="id" title="lemma">cyclic_factor_abelian</span></a> <span class="id" title="var">H</span> <span class="id" title="var">G</span> :<br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.center.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.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.cyclic.html#cyclic"><span class="id" title="definition">cyclic</span></a> (<a class="idref" href="mathcomp.solvable.center.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.center.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.center.html#G"><span class="id" title="variable">G</span></a>.<br/>

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

<br/>
<span class="id" title="keyword">Variables</span> (<a name="Center.Injm.rT"><span class="id" title="variable">rT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<a name="Center.Injm.D"><span class="id" title="variable">D</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.center.html#Center.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<a name="Center.Injm.f"><span class="id" title="variable">f</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.solvable.center.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.center.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">}</span></a>).<br/>

<br/>
<span class="id" title="keyword">Hypothesis</span> <a name="Center.Injm.injf"><span class="id" title="variable">injf</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#14bfb149f00fa839cfb11397f4fe629f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#14bfb149f00fa839cfb11397f4fe629f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.solvable.center.html#Center.Injm.f"><span class="id" title="variable">f</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="injm_center"><span class="id" title="lemma">injm_center</span></a> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.solvable.center.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.center.html#Center.Injm.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.center.html#Center.Injm.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.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#Center.Injm.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.center.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.center.html#Center.Injm"><span class="id" title="section">Injm</span></a>.<br/>

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

<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="isog_center"><span class="id" title="lemma">isog_center</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">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.center.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.center.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) :<br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.center.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.center.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.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.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.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Section</span> <a name="Product"><span class="id" title="section">Product</span></a>.<br/>

<br/>
<span class="id" title="keyword">Variable</span> <a name="Product.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">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.center.html#Product.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">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.center.html#Product.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="center_prod"><span class="id" title="lemma">center_prod</span></a> <span class="id" title="var">H</span> <span class="id" title="var">K</span> : <a class="idref" href="mathcomp.solvable.center.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.center.html#H"><span class="id" title="variable">H</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.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><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.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.solvable.center.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="center_cprod"><span class="id" title="lemma">center_cprod</span></a> <span class="id" title="var">A</span> <span class="id" title="var">B</span> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.solvable.center.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#9607c0b7b0a7e59f4327b220d5a93330"><span class="id" title="notation">\*</span></a> <a class="idref" href="mathcomp.solvable.center.html#B"><span class="id" title="variable">B</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#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.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#9607c0b7b0a7e59f4327b220d5a93330"><span class="id" title="notation">\*</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="center_bigcprod"><span class="id" title="lemma">center_bigcprod</span></a> <span class="id" title="var">I</span> <span class="id" title="var">r</span> <span class="id" title="var">P</span> (<span class="id" title="var">F</span> : <a class="idref" href="mathcomp.solvable.center.html#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#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <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.center.html#Product.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">G</span> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">big</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.gproduct.html#cprod"><span class="id" title="abbreviation">cprod</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">/</span></a>1<a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="mathcomp.solvable.center.html#r"><span class="id" title="variable">r</span></a> <a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.center.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.solvable.center.html#i"><span class="id" title="variable">i</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.center.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.center.html#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.center.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">big</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.gproduct.html#cprod"><span class="id" title="abbreviation">cprod</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">/</span></a>1<a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="mathcomp.solvable.center.html#r"><span class="id" title="variable">r</span></a> <a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.center.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.solvable.center.html#i"><span class="id" title="variable">i</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.center.html#i"><span class="id" title="variable">i</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="cprod_center_id"><span class="id" title="lemma">cprod_center_id</span></a> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.solvable.center.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#9607c0b7b0a7e59f4327b220d5a93330"><span class="id" title="notation">\*</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#G"><span class="id" title="variable">G</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="center_dprod"><span class="id" title="lemma">center_dprod</span></a> <span class="id" title="var">A</span> <span class="id" title="var">B</span> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.solvable.center.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#3733c0e43956ad2062ab5f1e57ceb9a8"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.gproduct.html#3733c0e43956ad2062ab5f1e57ceb9a8"><span class="id" title="notation">x</span></a> <a class="idref" href="mathcomp.solvable.center.html#B"><span class="id" title="variable">B</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#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.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#3733c0e43956ad2062ab5f1e57ceb9a8"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.gproduct.html#3733c0e43956ad2062ab5f1e57ceb9a8"><span class="id" title="notation">x</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="center_bigdprod"><span class="id" title="lemma">center_bigdprod</span></a> <span class="id" title="var">I</span> <span class="id" title="var">r</span> <span class="id" title="var">P</span> (<span class="id" title="var">F</span>: <a class="idref" href="mathcomp.solvable.center.html#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#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <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.center.html#Product.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">G</span> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">big</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.gproduct.html#dprod"><span class="id" title="abbreviation">dprod</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">/</span></a>1<a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="mathcomp.solvable.center.html#r"><span class="id" title="variable">r</span></a> <a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.center.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.solvable.center.html#i"><span class="id" title="variable">i</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.center.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.center.html#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.center.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">big</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.gproduct.html#dprod"><span class="id" title="abbreviation">dprod</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">/</span></a>1<a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="mathcomp.solvable.center.html#r"><span class="id" title="variable">r</span></a> <a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.center.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.solvable.center.html#i"><span class="id" title="variable">i</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#52c4d552b36d01307b4a33177122d4d1"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.center.html#i"><span class="id" title="variable">i</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="Aut_cprod_full"><span class="id" title="lemma">Aut_cprod_full</span></a> <span class="id" title="var">G</span> <span class="id" title="var">H</span> <span class="id" title="var">K</span> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.center.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#9607c0b7b0a7e59f4327b220d5a93330"><span class="id" title="notation">\*</span></a> <a class="idref" href="mathcomp.solvable.center.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> <a class="idref" href="mathcomp.solvable.center.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.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.action.html#Aut_in"><span class="id" title="definition">Aut_in</span></a> (<a class="idref" href="mathcomp.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.solvable.center.html#H"><span class="id" title="variable">H</span></a>) <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><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.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.action.html#Aut_in"><span class="id" title="definition">Aut_in</span></a> (<a class="idref" href="mathcomp.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.solvable.center.html#K"><span class="id" title="variable">K</span></a>) <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><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.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.action.html#Aut_in"><span class="id" title="definition">Aut_in</span></a> (<a class="idref" href="mathcomp.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.solvable.center.html#G"><span class="id" title="variable">G</span></a>) <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.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.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a>.<br/>

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

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

<br/>
<span class="id" title="keyword">Variables</span> <a name="CprodBy.gTH"><span class="id" title="variable">gTH</span></a> <a name="CprodBy.gTK"><span class="id" title="variable">gTK</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>.<br/>
<span class="id" title="keyword">Variables</span> (<a name="CprodBy.H"><span class="id" title="variable">H</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.gTH"><span class="id" title="variable">gTH</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<a name="CprodBy.K"><span class="id" title="variable">K</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.gTK"><span class="id" title="variable">gTK</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<a name="CprodBy.gz"><span class="id" title="variable">gz</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.gTK"><span class="id" title="variable">gTK</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">}</span></a>).<br/>

<br/>
<span class="id" title="keyword">Definition</span> <a name="ker_cprod_by"><span class="id" title="definition">ker_cprod_by</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.fingroup.morphism.html#isom"><span class="id" title="definition">isom</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#CprodBy.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#CprodBy.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.gz"><span class="id" title="variable">gz</span></a> :=<br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.ssreflect.finset.html#20dd00d77a881552893c96be95088d1a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#20dd00d77a881552893c96be95088d1a"><span class="id" title="notation">set</span></a> <span class="id" title="var">xy</span> <a class="idref" href="mathcomp.ssreflect.finset.html#20dd00d77a881552893c96be95088d1a"><span class="id" title="notation">|</span></a> <span class="id" title="keyword">let</span>: <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <span class="id" title="var">y</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a> := <a class="idref" href="mathcomp.solvable.center.html#xy"><span class="id" title="variable">xy</span></a> <span class="id" title="tactic">in</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">(</span></a><span class="id" title="var">x</span> <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.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#CprodBy.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">&amp;&amp;</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">(</span></a><span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#a605acbeae7597f74f5a9b816ed8a717"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#CprodBy.gz"><span class="id" title="variable">gz</span></a> <span class="id" title="var">x</span><a class="idref" href="mathcomp.fingroup.fingroup.html#a605acbeae7597f74f5a9b816ed8a717"><span class="id" title="notation">)^-1</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#20dd00d77a881552893c96be95088d1a"><span class="id" title="notation">]</span></a>.<br/>

<br/>
<span class="id" title="keyword">Hypothesis</span> <a name="CprodBy.isoZ"><span class="id" title="variable">isoZ</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#isom"><span class="id" title="definition">isom</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#CprodBy.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#CprodBy.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.gz"><span class="id" title="variable">gz</span></a>.<br/>
<span class="id" title="keyword">Let</span> <a name="CprodBy.kerHK"><span class="id" title="variable">kerHK</span></a> := <a class="idref" href="mathcomp.solvable.center.html#ker_cprod_by"><span class="id" title="definition">ker_cprod_by</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.isoZ"><span class="id" title="variable">isoZ</span></a>.<br/>

<br/>
<span class="id" title="keyword">Let</span> <a name="CprodBy.injgz"><span class="id" title="variable">injgz</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#14bfb149f00fa839cfb11397f4fe629f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#14bfb149f00fa839cfb11397f4fe629f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.gz"><span class="id" title="variable">gz</span></a>.  <br/>
<span class="id" title="keyword">Let</span> <a name="CprodBy.gzZ"><span class="id" title="variable">gzZ</span></a> : <a class="idref" href="mathcomp.solvable.center.html#CprodBy.gz"><span class="id" title="variable">gz</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#CprodBy.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#CprodBy.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a>.  <br/>
<span class="id" title="keyword">Let</span> <a name="CprodBy.gzZchar"><span class="id" title="variable">gzZchar</span></a> : <a class="idref" href="mathcomp.solvable.center.html#CprodBy.gz"><span class="id" title="variable">gz</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#CprodBy.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><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.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#CprodBy.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a>.  <br/>
<span class="id" title="keyword">Let</span> <a name="CprodBy.sgzZZ"><span class="id" title="variable">sgzZZ</span></a> : <a class="idref" href="mathcomp.solvable.center.html#CprodBy.gz"><span class="id" title="variable">gz</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#CprodBy.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#CprodBy.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> := <a class="idref" href="mathcomp.fingroup.automorphism.html#char_sub"><span class="id" title="lemma">char_sub</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.gzZchar"><span class="id" title="variable">gzZchar</span></a>.<br/>
<span class="id" title="keyword">Let</span> <a name="CprodBy.sZH"><span class="id" title="variable">sZH</span></a> := <a class="idref" href="mathcomp.solvable.center.html#center_sub"><span class="id" title="lemma">center_sub</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.H"><span class="id" title="variable">H</span></a>.<br/>
<span class="id" title="keyword">Let</span> <a name="CprodBy.sZK"><span class="id" title="variable">sZK</span></a> := <a class="idref" href="mathcomp.solvable.center.html#center_sub"><span class="id" title="lemma">center_sub</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.K"><span class="id" title="variable">K</span></a>.<br/>
<span class="id" title="keyword">Let</span> <a name="CprodBy.sgzZG"><span class="id" title="variable">sgzZG</span></a> : <a class="idref" href="mathcomp.solvable.center.html#CprodBy.gz"><span class="id" title="variable">gz</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#CprodBy.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.K"><span class="id" title="variable">K</span></a> := <a class="idref" href="mathcomp.ssreflect.fintype.html#subset_trans"><span class="id" title="lemma">subset_trans</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.sgzZZ"><span class="id" title="variable">sgzZZ</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.sZK"><span class="id" title="variable">sZK</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="ker_cprod_by_is_group"><span class="id" title="lemma">ker_cprod_by_is_group</span></a> : <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.center.html#CprodBy.kerHK"><span class="id" title="variable">kerHK</span></a>.<br/>
<span class="id" title="keyword">Canonical</span> <span class="id" title="var">ker_cprod_by_group</span> := <a class="idref" href="mathcomp.fingroup.fingroup.html#Group"><span class="id" title="constructor">Group</span></a> <a class="idref" href="mathcomp.solvable.center.html#ker_cprod_by_is_group"><span class="id" title="lemma">ker_cprod_by_is_group</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="ker_cprod_by_central"><span class="id" title="lemma">ker_cprod_by_central</span></a> : <a class="idref" href="mathcomp.solvable.center.html#CprodBy.kerHK"><span class="id" title="variable">kerHK</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#setX"><span class="id" title="definition">setX</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a>.<br/>

<br/>
<span class="id" title="keyword">Fact</span> <a name="cprod_by_key"><span class="id" title="lemma">cprod_by_key</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a>.  <br/>
<span class="id" title="keyword">Definition</span> <a name="cprod_by_def"><span class="id" title="definition">cprod_by_def</span></a> := <a class="idref" href="mathcomp.fingroup.fingroup.html#subFinGroupType"><span class="id" title="definition">subFinGroupType</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#ccb763a84253e971fd106aeeb9cd3cb0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ccb763a84253e971fd106aeeb9cd3cb0"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#ccb763a84253e971fd106aeeb9cd3cb0"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#setX"><span class="id" title="definition">setX</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#c7768147d2d560601601fbf95706ddcc"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.kerHK"><span class="id" title="variable">kerHK</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ccb763a84253e971fd106aeeb9cd3cb0"><span class="id" title="notation">]</span></a>.<br/>
<span class="id" title="keyword">Definition</span> <a name="cprod_by"><span class="id" title="definition">cprod_by</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#locked_with"><span class="id" title="definition">locked_with</span></a> <a class="idref" href="mathcomp.solvable.center.html#cprod_by_key"><span class="id" title="lemma">cprod_by_key</span></a> <a class="idref" href="mathcomp.solvable.center.html#cprod_by_def"><span class="id" title="definition">cprod_by_def</span></a>.<br/>

<br/>
<span class="id" title="keyword">Definition</span> <a name="in_cprod"><span class="id" title="definition">in_cprod</span></a> : <a class="idref" href="mathcomp.solvable.center.html#CprodBy.gTH"><span class="id" title="variable">gTH</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#d19c7eafd0e2d195d10df94b392087b5"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.gTK"><span class="id" title="variable">gTK</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.center.html#cprod_by"><span class="id" title="definition">cprod_by</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">let</span>: <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#tt"><span class="id" title="constructor">tt</span></a> <span class="id" title="keyword">as</span> <span class="id" title="var">k</span> := <a class="idref" href="mathcomp.solvable.center.html#cprod_by_key"><span class="id" title="lemma">cprod_by_key</span></a> <span class="id" title="keyword">return</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#locked_with"><span class="id" title="definition">locked_with</span></a> <a class="idref" href="mathcomp.solvable.center.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.solvable.center.html#cprod_by_def"><span class="id" title="definition">cprod_by_def</span></a> <span class="id" title="tactic">in</span><br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.fingroup.html#subg"><span class="id" title="definition">subg</span></a> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#1b4394c5c1740ef3dc9e4224084970bb"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#1b4394c5c1740ef3dc9e4224084970bb"><span class="id" title="notation">o</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#coset"><span class="id" title="definition">coset</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.kerHK"><span class="id" title="variable">kerHK</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="in_cprodM"><span class="id" title="lemma">in_cprodM</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#setX"><span class="id" title="definition">setX</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.K"><span class="id" title="variable">K</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">&amp;,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.solvable.center.html#in_cprod"><span class="id" title="definition">in_cprod</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">:</span></a> <span class="id" title="var">u</span> <span class="id" title="var">v</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.center.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.solvable.center.html#v"><span class="id" title="variable">v</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">}</span></a>.<br/>
<span class="id" title="keyword">Canonical</span> <span class="id" title="var">in_cprod_morphism</span> := <a class="idref" href="mathcomp.fingroup.morphism.html#Morphism"><span class="id" title="constructor">Morphism</span></a> <a class="idref" href="mathcomp.solvable.center.html#in_cprodM"><span class="id" title="lemma">in_cprodM</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="ker_in_cprod"><span class="id" title="lemma">ker_in_cprod</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#034cc0eb573e9a86d9574eaed7b27a13"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#034cc0eb573e9a86d9574eaed7b27a13"><span class="id" title="notation">ker</span></a> <a class="idref" href="mathcomp.solvable.center.html#in_cprod"><span class="id" title="definition">in_cprod</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.kerHK"><span class="id" title="variable">kerHK</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="cpairg1_dom"><span class="id" title="lemma">cpairg1_dom</span></a> : <a class="idref" href="mathcomp.solvable.center.html#CprodBy.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.morphism.html#f47bac414ebbcaae273350b5c84ff313"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#f47bac414ebbcaae273350b5c84ff313"><span class="id" title="notation">dom</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#f47bac414ebbcaae273350b5c84ff313"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#in_cprod"><span class="id" title="definition">in_cprod</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#1b4394c5c1740ef3dc9e4224084970bb"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#1b4394c5c1740ef3dc9e4224084970bb"><span class="id" title="notation">o</span></a> @<a class="idref" href="mathcomp.fingroup.gproduct.html#pairg1"><span class="id" title="definition">pairg1</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.gTH"><span class="id" title="variable">gTH</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.gTK"><span class="id" title="variable">gTK</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#f47bac414ebbcaae273350b5c84ff313"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="cpair1g_dom"><span class="id" title="lemma">cpair1g_dom</span></a> : <a class="idref" href="mathcomp.solvable.center.html#CprodBy.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.morphism.html#f47bac414ebbcaae273350b5c84ff313"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#f47bac414ebbcaae273350b5c84ff313"><span class="id" title="notation">dom</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#f47bac414ebbcaae273350b5c84ff313"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#in_cprod"><span class="id" title="definition">in_cprod</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#1b4394c5c1740ef3dc9e4224084970bb"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#1b4394c5c1740ef3dc9e4224084970bb"><span class="id" title="notation">o</span></a> @<a class="idref" href="mathcomp.fingroup.gproduct.html#pair1g"><span class="id" title="definition">pair1g</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.gTH"><span class="id" title="variable">gTH</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.gTK"><span class="id" title="variable">gTK</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#f47bac414ebbcaae273350b5c84ff313"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Definition</span> <a name="cpairg1"><span class="id" title="definition">cpairg1</span></a> := <a class="idref" href="mathcomp.ssreflect.eqtype.html#tag"><span class="id" title="definition">tag</span></a> (<a class="idref" href="mathcomp.fingroup.morphism.html#restrmP"><span class="id" title="lemma">restrmP</span></a> <span class="id" title="var">_</span> <a class="idref" href="mathcomp.solvable.center.html#cpairg1_dom"><span class="id" title="lemma">cpairg1_dom</span></a>).<br/>
<span class="id" title="keyword">Definition</span> <a name="cpair1g"><span class="id" title="definition">cpair1g</span></a> := <a class="idref" href="mathcomp.ssreflect.eqtype.html#tag"><span class="id" title="definition">tag</span></a> (<a class="idref" href="mathcomp.fingroup.morphism.html#restrmP"><span class="id" title="lemma">restrmP</span></a> <span class="id" title="var">_</span> <a class="idref" href="mathcomp.solvable.center.html#cpair1g_dom"><span class="id" title="lemma">cpair1g_dom</span></a>).<br/>

<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="injm_cpairg1"><span class="id" title="lemma">injm_cpairg1</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#14bfb149f00fa839cfb11397f4fe629f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#14bfb149f00fa839cfb11397f4fe629f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.solvable.center.html#cpairg1"><span class="id" title="definition">cpairg1</span></a>.<br/>
<span class="id" title="keyword">Let</span> <a name="CprodBy.injH"><span class="id" title="variable">injH</span></a> := <a class="idref" href="mathcomp.solvable.center.html#injm_cpairg1"><span class="id" title="lemma">injm_cpairg1</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="injm_cpair1g"><span class="id" title="lemma">injm_cpair1g</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#14bfb149f00fa839cfb11397f4fe629f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#14bfb149f00fa839cfb11397f4fe629f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.solvable.center.html#cpair1g"><span class="id" title="definition">cpair1g</span></a>.<br/>
<span class="id" title="keyword">Let</span> <a name="CprodBy.injK"><span class="id" title="variable">injK</span></a> := <a class="idref" href="mathcomp.solvable.center.html#injm_cpair1g"><span class="id" title="lemma">injm_cpair1g</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="im_cpair_cent"><span class="id" title="lemma">im_cpair_cent</span></a> : <a class="idref" href="mathcomp.solvable.center.html#CK"><span class="id" title="abbreviation">CK</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.center.html#CH"><span class="id" title="abbreviation">CH</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#67c26168baa7671aab03da2a0fb7dafa"><span class="id" title="notation">)</span></a>.<br/>
<span class="id" title="keyword">Hint Resolve</span> <span class="id" title="var">im_cpair_cent</span>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="im_cpair"><span class="id" title="lemma">im_cpair</span></a> : <a class="idref" href="mathcomp.solvable.center.html#CH"><span class="id" title="abbreviation">CH</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.solvable.center.html#CK"><span class="id" title="abbreviation">CK</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#C"><span class="id" title="abbreviation">C</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="im_cpair_cprod"><span class="id" title="lemma">im_cpair_cprod</span></a> : <a class="idref" href="mathcomp.solvable.center.html#CH"><span class="id" title="abbreviation">CH</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#9607c0b7b0a7e59f4327b220d5a93330"><span class="id" title="notation">\*</span></a> <a class="idref" href="mathcomp.solvable.center.html#CK"><span class="id" title="abbreviation">CK</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#C"><span class="id" title="abbreviation">C</span></a>.  <br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="eq_cpairZ"><span class="id" title="lemma">eq_cpairZ</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#CprodBy.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.center.html#cpairg1"><span class="id" title="definition">cpairg1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.solvable.center.html#cpair1g"><span class="id" title="definition">cpair1g</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#1b4394c5c1740ef3dc9e4224084970bb"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#1b4394c5c1740ef3dc9e4224084970bb"><span class="id" title="notation">o</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.gz"><span class="id" title="variable">gz</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="setI_im_cpair"><span class="id" title="lemma">setI_im_cpair</span></a> : <a class="idref" href="mathcomp.solvable.center.html#CH"><span class="id" title="abbreviation">CH</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#cb41714a5a23482f7a48a98975fa8c59"><span class="id" title="notation">:&amp;:</span></a> <a class="idref" href="mathcomp.solvable.center.html#CK"><span class="id" title="abbreviation">CK</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#CH"><span class="id" title="abbreviation">CH</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="cpair1g_center"><span class="id" title="lemma">cpair1g_center</span></a> : <a class="idref" href="mathcomp.solvable.center.html#cpair1g"><span class="id" title="definition">cpair1g</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#CprodBy.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#C"><span class="id" title="abbreviation">C</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a>.<br/>

<br/>
</div>

<div class="doc">
 Uses gzZ.  
</div>
<div class="code">
<span class="id" title="keyword">Lemma</span> <a name="cpair_center_id"><span class="id" title="lemma">cpair_center_id</span></a> : <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#CH"><span class="id" title="abbreviation">CH</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#CK"><span class="id" title="abbreviation">CK</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a>.<br/>

<br/>
</div>

<div class="doc">
 Uses gzZ.  
</div>
<div class="code">
<span class="id" title="keyword">Lemma</span> <a name="cpairg1_center"><span class="id" title="lemma">cpairg1_center</span></a> : <a class="idref" href="mathcomp.solvable.center.html#cpairg1"><span class="id" title="definition">cpairg1</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#CprodBy.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#C"><span class="id" title="abbreviation">C</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Section</span> <a name="CprodBy.ExtCprodm"><span class="id" title="section">ExtCprodm</span></a>.<br/>

<br/>
<span class="id" title="keyword">Variable</span> <a name="CprodBy.ExtCprodm.rT"><span class="id" title="variable">rT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>.<br/>
<span class="id" title="keyword">Variables</span> (<a name="CprodBy.ExtCprodm.fH"><span class="id" title="variable">fH</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.ExtCprodm.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>) (<a name="CprodBy.ExtCprodm.fK"><span class="id" title="variable">fK</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.ExtCprodm.rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">}</span></a>).<br/>
<span class="id" title="keyword">Hypothesis</span> <a name="CprodBy.ExtCprodm.cfHK"><span class="id" title="variable">cfHK</span></a> : <a class="idref" href="mathcomp.solvable.center.html#CprodBy.ExtCprodm.fK"><span class="id" title="variable">fK</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.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.center.html#CprodBy.ExtCprodm.fH"><span class="id" title="variable">fH</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#67c26168baa7671aab03da2a0fb7dafa"><span class="id" title="notation">)</span></a>.<br/>
<span class="id" title="keyword">Hypothesis</span> <a name="CprodBy.ExtCprodm.eq_fHK"><span class="id" title="variable">eq_fHK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#CprodBy.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.ExtCprodm.fH"><span class="id" title="variable">fH</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.ExtCprodm.fK"><span class="id" title="variable">fK</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#1b4394c5c1740ef3dc9e4224084970bb"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#1b4394c5c1740ef3dc9e4224084970bb"><span class="id" title="notation">o</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.gz"><span class="id" title="variable">gz</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</span></a>.<br/>

<br/>
<span class="id" title="keyword">Let</span> <a name="CprodBy.ExtCprodm.gH"><span class="id" title="variable">gH</span></a> := <a class="idref" href="mathcomp.fingroup.morphism.html#ifactm"><span class="id" title="definition">ifactm</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.ExtCprodm.fH"><span class="id" title="variable">fH</span></a> <a class="idref" href="mathcomp.solvable.center.html#injm_cpairg1"><span class="id" title="lemma">injm_cpairg1</span></a>.<br/>
<span class="id" title="keyword">Let</span> <a name="CprodBy.ExtCprodm.gK"><span class="id" title="variable">gK</span></a> := <a class="idref" href="mathcomp.fingroup.morphism.html#ifactm"><span class="id" title="definition">ifactm</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.ExtCprodm.fK"><span class="id" title="variable">fK</span></a> <a class="idref" href="mathcomp.solvable.center.html#injm_cpair1g"><span class="id" title="lemma">injm_cpair1g</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="xcprodm_cent"><span class="id" title="lemma">xcprodm_cent</span></a> : <a class="idref" href="mathcomp.solvable.center.html#CprodBy.ExtCprodm.gK"><span class="id" title="variable">gK</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.center.html#CK"><span class="id" title="abbreviation">CK</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.center.html#CprodBy.ExtCprodm.gH"><span class="id" title="variable">gH</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.center.html#CH"><span class="id" title="abbreviation">CH</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="xcprodmI"><span class="id" title="lemma">xcprodmI</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.center.html#CH"><span class="id" title="abbreviation">CH</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#cb41714a5a23482f7a48a98975fa8c59"><span class="id" title="notation">:&amp;:</span></a> <a class="idref" href="mathcomp.solvable.center.html#CK"><span class="id" title="abbreviation">CK</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.ExtCprodm.gH"><span class="id" title="variable">gH</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.ExtCprodm.gK"><span class="id" title="variable">gK</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</span></a>.<br/>

<br/>
<span class="id" title="keyword">Definition</span> <a name="xcprodm"><span class="id" title="definition">xcprodm</span></a> := <a class="idref" href="mathcomp.fingroup.gproduct.html#cprodm"><span class="id" title="definition">cprodm</span></a> <a class="idref" href="mathcomp.solvable.center.html#im_cpair_cprod"><span class="id" title="lemma">im_cpair_cprod</span></a> <a class="idref" href="mathcomp.solvable.center.html#xcprodm_cent"><span class="id" title="lemma">xcprodm_cent</span></a> <a class="idref" href="mathcomp.solvable.center.html#xcprodmI"><span class="id" title="lemma">xcprodmI</span></a>.<br/>
<span class="id" title="keyword">Canonical</span> <span class="id" title="var">xcprod_morphism</span> := <a class="idref" href="mathcomp.fingroup.morphism.html#4638420a8c497f6fdfbc01376756a30a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#4638420a8c497f6fdfbc01376756a30a"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#4638420a8c497f6fdfbc01376756a30a"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.center.html#xcprodm"><span class="id" title="definition">xcprodm</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#4638420a8c497f6fdfbc01376756a30a"><span class="id" title="notation">]</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="xcprodmEl"><span class="id" title="lemma">xcprodmEl</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.H"><span class="id" title="variable">H</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.solvable.center.html#xcprodm"><span class="id" title="definition">xcprodm</span></a> (<a class="idref" href="mathcomp.solvable.center.html#cpairg1"><span class="id" title="definition">cpairg1</span></a> <a class="idref" href="mathcomp.solvable.center.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> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.ExtCprodm.fH"><span class="id" title="variable">fH</span></a> <a class="idref" href="mathcomp.solvable.center.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#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="xcprodmEr"><span class="id" title="lemma">xcprodmEr</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.K"><span class="id" title="variable">K</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">y</span>, <a class="idref" href="mathcomp.solvable.center.html#xcprodm"><span class="id" title="definition">xcprodm</span></a> (<a class="idref" href="mathcomp.solvable.center.html#cpair1g"><span class="id" title="definition">cpair1g</span></a> <a class="idref" href="mathcomp.solvable.center.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.center.html#CprodBy.ExtCprodm.fK"><span class="id" title="variable">fK</span></a> <a class="idref" href="mathcomp.solvable.center.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#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="xcprodmE"><span class="id" title="lemma">xcprodmE</span></a> :<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#208bc995000a6307bdbc043c43919d97"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#208bc995000a6307bdbc043c43919d97"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#208bc995000a6307bdbc043c43919d97"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.K"><span class="id" title="variable">K</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#208bc995000a6307bdbc043c43919d97"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>, <a class="idref" href="mathcomp.solvable.center.html#xcprodm"><span class="id" title="definition">xcprodm</span></a> (<a class="idref" href="mathcomp.solvable.center.html#cpairg1"><span class="id" title="definition">cpairg1</span></a> <a class="idref" href="mathcomp.solvable.center.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.center.html#cpair1g"><span class="id" title="definition">cpair1g</span></a> <a class="idref" href="mathcomp.solvable.center.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.center.html#CprodBy.ExtCprodm.fH"><span class="id" title="variable">fH</span></a> <a class="idref" href="mathcomp.solvable.center.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.center.html#CprodBy.ExtCprodm.fK"><span class="id" title="variable">fK</span></a> <a class="idref" href="mathcomp.solvable.center.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#208bc995000a6307bdbc043c43919d97"><span class="id" title="notation">}</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="im_xcprodm"><span class="id" title="lemma">im_xcprodm</span></a> : <a class="idref" href="mathcomp.solvable.center.html#xcprodm"><span class="id" title="definition">xcprodm</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.center.html#C"><span class="id" title="abbreviation">C</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.ExtCprodm.fH"><span class="id" title="variable">fH</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.ExtCprodm.fK"><span class="id" title="variable">fK</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.K"><span class="id" title="variable">K</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="im_xcprodml"><span class="id" title="lemma">im_xcprodml</span></a> <span class="id" title="var">A</span> : <a class="idref" href="mathcomp.solvable.center.html#xcprodm"><span class="id" title="definition">xcprodm</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#cpairg1"><span class="id" title="definition">cpairg1</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.center.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><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.center.html#CprodBy.ExtCprodm.fH"><span class="id" title="variable">fH</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.center.html#A"><span class="id" title="variable">A</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="im_xcprodmr"><span class="id" title="lemma">im_xcprodmr</span></a> <span class="id" title="var">A</span> : <a class="idref" href="mathcomp.solvable.center.html#xcprodm"><span class="id" title="definition">xcprodm</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#cpair1g"><span class="id" title="definition">cpair1g</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.center.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><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.center.html#CprodBy.ExtCprodm.fK"><span class="id" title="variable">fK</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.center.html#A"><span class="id" title="variable">A</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="injm_xcprodm"><span class="id" title="lemma">injm_xcprodm</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#14bfb149f00fa839cfb11397f4fe629f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#14bfb149f00fa839cfb11397f4fe629f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.solvable.center.html#xcprodm"><span class="id" title="definition">xcprodm</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.morphism.html#14bfb149f00fa839cfb11397f4fe629f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#14bfb149f00fa839cfb11397f4fe629f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.ExtCprodm.fH"><span class="id" title="variable">fH</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">&amp;&amp;</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#14bfb149f00fa839cfb11397f4fe629f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#14bfb149f00fa839cfb11397f4fe629f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.ExtCprodm.fK"><span class="id" title="variable">fK</span></a>.<br/>

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

<br/>
</div>

<div class="doc">
 Uses gzZchar.  
</div>
<div class="code">
<span class="id" title="keyword">Lemma</span> <a name="Aut_cprod_by_full"><span class="id" title="lemma">Aut_cprod_by_full</span></a> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.action.html#Aut_in"><span class="id" title="definition">Aut_in</span></a> (<a class="idref" href="mathcomp.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.H"><span class="id" title="variable">H</span></a>) <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#CprodBy.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><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.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#CprodBy.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.action.html#Aut_in"><span class="id" title="definition">Aut_in</span></a> (<a class="idref" href="mathcomp.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.K"><span class="id" title="variable">K</span></a>) <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#CprodBy.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><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.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#CprodBy.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.action.html#Aut_in"><span class="id" title="definition">Aut_in</span></a> (<a class="idref" href="mathcomp.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.solvable.center.html#C"><span class="id" title="abbreviation">C</span></a>) <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#C"><span class="id" title="abbreviation">C</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><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.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#C"><span class="id" title="abbreviation">C</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a>.<br/>

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

<br/>
<span class="id" title="keyword">Let</span> <a name="CprodBy.Isomorphism.gzZ_lone"><span class="id" title="variable">gzZ_lone</span></a> (<span class="id" title="var">Y</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.center.html#CprodBy.gTK"><span class="id" title="variable">gTK</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) :<br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.center.html#Y"><span class="id" title="variable">Y</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#CprodBy.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.gz"><span class="id" title="variable">gz</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#CprodBy.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><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.center.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#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.gz"><span class="id" title="variable">gz</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#CprodBy.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#Y"><span class="id" title="variable">Y</span></a>.<br/>

<br/>
<span class="id" title="keyword">Variables</span> (<a name="CprodBy.Isomorphism.rT"><span class="id" title="variable">rT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<a name="CprodBy.Isomorphism.GH"><span class="id" title="variable">GH</span></a> <a name="CprodBy.Isomorphism.GK"><span class="id" title="variable">GK</span></a> <a name="CprodBy.Isomorphism.G"><span class="id" title="variable">G</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.center.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>).<br/>
<span class="id" title="keyword">Hypotheses</span> (<a name="CprodBy.Isomorphism.defG"><span class="id" title="variable">defG</span></a> : <a class="idref" href="mathcomp.solvable.center.html#CprodBy.Isomorphism.GH"><span class="id" title="variable">GH</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#9607c0b7b0a7e59f4327b220d5a93330"><span class="id" title="notation">\*</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.Isomorphism.GK"><span class="id" title="variable">GK</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.Isomorphism.G"><span class="id" title="variable">G</span></a>) (<a name="CprodBy.Isomorphism.ziGHK"><span class="id" title="variable">ziGHK</span></a> : <a class="idref" href="mathcomp.solvable.center.html#CprodBy.Isomorphism.GH"><span class="id" title="variable">GH</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#cb41714a5a23482f7a48a98975fa8c59"><span class="id" title="notation">:&amp;:</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.Isomorphism.GK"><span class="id" title="variable">GK</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#CprodBy.Isomorphism.GH"><span class="id" title="variable">GH</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a>).<br/>
<span class="id" title="keyword">Hypothesis</span> <a name="CprodBy.Isomorphism.AutZHfull"><span class="id" title="variable">AutZHfull</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#Aut_in"><span class="id" title="definition">Aut_in</span></a> (<a class="idref" href="mathcomp.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.H"><span class="id" title="variable">H</span></a>) <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#CprodBy.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><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.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#CprodBy.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a>.<br/>
<span class="id" title="keyword">Hypotheses</span> (<a name="CprodBy.Isomorphism.isoGH"><span class="id" title="variable">isoGH</span></a> : <a class="idref" href="mathcomp.solvable.center.html#CprodBy.Isomorphism.GH"><span class="id" title="variable">GH</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.center.html#CprodBy.H"><span class="id" title="variable">H</span></a>) (<a name="CprodBy.Isomorphism.isoGK"><span class="id" title="variable">isoGK</span></a> : <a class="idref" href="mathcomp.solvable.center.html#CprodBy.Isomorphism.GK"><span class="id" title="variable">GK</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.center.html#CprodBy.K"><span class="id" title="variable">K</span></a>).<br/>

<br/>
</div>

<div class="doc">
 Uses gzZ_lone  
</div>
<div class="code">
<span class="id" title="keyword">Lemma</span> <a name="cprod_by_uniq"><span class="id" title="lemma">cprod_by_uniq</span></a> :<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">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.center.html#CprodBy.Isomorphism.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.center.html#cprod_by"><span class="id" title="definition">cprod_by</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">[/\</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#isom"><span class="id" title="definition">isom</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.Isomorphism.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.center.html#C"><span class="id" title="abbreviation">C</span></a> <a class="idref" href="mathcomp.solvable.center.html#f"><span class="id" title="variable">f</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.center.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.center.html#CprodBy.Isomorphism.GH"><span class="id" title="variable">GH</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#CH"><span class="id" title="abbreviation">CH</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.solvable.center.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.center.html#CprodBy.Isomorphism.GK"><span class="id" title="variable">GK</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#CK"><span class="id" title="abbreviation">CK</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">]</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="isog_cprod_by"><span class="id" title="lemma">isog_cprod_by</span></a> : <a class="idref" href="mathcomp.solvable.center.html#CprodBy.Isomorphism.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.center.html#C"><span class="id" title="abbreviation">C</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.Isomorphism"><span class="id" title="section">Isomorphism</span></a>.<br/>

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

<br/>
<span class="id" title="keyword">Section</span> <a name="ExtCprod"><span class="id" title="section">ExtCprod</span></a>.<br/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">finfun</span>.<br/>

<br/>
<span class="id" title="keyword">Variables</span> <a name="ExtCprod.gTH"><span class="id" title="variable">gTH</span></a> <a name="ExtCprod.gTK"><span class="id" title="variable">gTK</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>.<br/>
<span class="id" title="keyword">Variables</span> (<a name="ExtCprod.H"><span class="id" title="variable">H</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.center.html#ExtCprod.gTH"><span class="id" title="variable">gTH</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<a name="ExtCprod.K"><span class="id" title="variable">K</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.center.html#ExtCprod.gTK"><span class="id" title="variable">gTK</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">Let</span> <a name="ExtCprod.gt_"><span class="id" title="variable">gt_</span></a> <span class="id" title="var">b</span> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.solvable.center.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.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">then</span></a> <a class="idref" href="mathcomp.solvable.center.html#ExtCprod.gTK"><span class="id" title="variable">gTK</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">else</span></a> <a class="idref" href="mathcomp.solvable.center.html#ExtCprod.gTH"><span class="id" title="variable">gTH</span></a>.<br/>
<span class="id" title="keyword">Let</span> <a name="ExtCprod.G_"><span class="id" title="variable">G_</span></a> <span class="id" title="var">b</span> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#f2de61384776e923a9c502554d1079cb"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.solvable.center.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.ssreflect.html#f2de61384776e923a9c502554d1079cb"><span class="id" title="notation">as</span></a> <span class="id" title="var">b'</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#f2de61384776e923a9c502554d1079cb"><span class="id" title="notation">return</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.center.html#ExtCprod.gt_"><span class="id" title="variable">gt_</span></a> <a class="idref" href="mathcomp.solvable.center.html#b'"><span class="id" title="variable">b'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#f2de61384776e923a9c502554d1079cb"><span class="id" title="notation">then</span></a> <a class="idref" href="mathcomp.solvable.center.html#ExtCprod.K"><span class="id" title="variable">K</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#f2de61384776e923a9c502554d1079cb"><span class="id" title="notation">else</span></a> <a class="idref" href="mathcomp.solvable.center.html#ExtCprod.H"><span class="id" title="variable">H</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="xcprod_subproof"><span class="id" title="lemma">xcprod_subproof</span></a> :<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">{</span></a><span class="id" title="var">gz</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.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.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#ExtCprod.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.center.html#ExtCprod.gt_"><span class="id" title="variable">gt_</span></a> <a class="idref" href="mathcomp.solvable.center.html#isob"><span class="id" title="abbreviation">isob</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#isom"><span class="id" title="definition">isom</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#ExtCprod.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#ExtCprod.G_"><span class="id" title="variable">G_</span></a> <a class="idref" href="mathcomp.solvable.center.html#isob"><span class="id" title="abbreviation">isob</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.center.html#gz"><span class="id" title="variable">gz</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#72ca3fac4636a1b19c963b12162882cf"><span class="id" title="notation">}</span></a>.<br/>

<br/>
<span class="id" title="keyword">Definition</span> <a name="xcprod"><span class="id" title="definition">xcprod</span></a> := <a class="idref" href="mathcomp.solvable.center.html#cprod_by"><span class="id" title="definition">cprod_by</span></a> (<a class="idref" href="mathcomp.ssreflect.eqtype.html#svalP"><span class="id" title="lemma">svalP</span></a> <a class="idref" href="mathcomp.solvable.center.html#xcprod_subproof"><span class="id" title="lemma">xcprod_subproof</span></a>).<br/>

<br/>
<span class="id" title="keyword">Inductive</span> <a name="xcprod_spec"><span class="id" title="inductive">xcprod_spec</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;<a name="XcprodSpec"><span class="id" title="constructor">XcprodSpec</span></a> <span class="id" title="var">gz</span> <span class="id" title="var">isoZ</span> : <a class="idref" href="mathcomp.solvable.center.html#xcprod_spec"><span class="id" title="inductive">xcprod_spec</span></a> (@<a class="idref" href="mathcomp.solvable.center.html#cprod_by"><span class="id" title="definition">cprod_by</span></a> <a class="idref" href="mathcomp.solvable.center.html#ExtCprod.gTH"><span class="id" title="variable">gTH</span></a> <a class="idref" href="mathcomp.solvable.center.html#ExtCprod.gTK"><span class="id" title="variable">gTK</span></a> <a class="idref" href="mathcomp.solvable.center.html#ExtCprod.H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.center.html#ExtCprod.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.center.html#gz"><span class="id" title="variable">gz</span></a> <a class="idref" href="mathcomp.solvable.center.html#isoZ"><span class="id" title="variable">isoZ</span></a>).<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="xcprodP"><span class="id" title="lemma">xcprodP</span></a> : <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#ExtCprod.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><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.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#ExtCprod.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.center.html#xcprod_spec"><span class="id" title="inductive">xcprod_spec</span></a> <a class="idref" href="mathcomp.solvable.center.html#xcprod"><span class="id" title="definition">xcprod</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="isog_xcprod"><span class="id" title="lemma">isog_xcprod</span></a> (<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">GH</span> <span class="id" title="var">GK</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.center.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.action.html#Aut_in"><span class="id" title="definition">Aut_in</span></a> (<a class="idref" href="mathcomp.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.solvable.center.html#ExtCprod.H"><span class="id" title="variable">H</span></a>) <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#ExtCprod.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><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.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#ExtCprod.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.center.html#GH"><span class="id" title="variable">GH</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.center.html#ExtCprod.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.center.html#GK"><span class="id" title="variable">GK</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.center.html#ExtCprod.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.solvable.center.html#GH"><span class="id" title="variable">GH</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#9607c0b7b0a7e59f4327b220d5a93330"><span class="id" title="notation">\*</span></a> <a class="idref" href="mathcomp.solvable.center.html#GK"><span class="id" title="variable">GK</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#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.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#GH"><span class="id" title="variable">GH</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#GK"><span class="id" title="variable">GK</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.center.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.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.center.html#xcprod"><span class="id" title="definition">xcprod</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#26c09fa7b21f5311d68f07b2527cd1eb"><span class="id" title="notation">]</span></a>.<br/>

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

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

<br/>
<span class="id" title="keyword">Variables</span> (<a name="IterCprod.gT"><span class="id" title="variable">gT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<a name="IterCprod.G"><span class="id" title="variable">G</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.center.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>).<br/>

<br/>
<span class="id" title="keyword">Fixpoint</span> <a name="ncprod_def"><span class="id" title="definition">ncprod_def</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.solvable.center.html#n"><span class="id" title="variable">n</span></a> <span class="id" title="keyword">is</span> <span class="id" title="var">n'</span><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> <span class="id" title="keyword">then</span> <a class="idref" href="mathcomp.solvable.center.html#xcprod"><span class="id" title="definition">xcprod</span></a> <a class="idref" href="mathcomp.solvable.center.html#IterCprod.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.center.html#ncprod_def"><span class="id" title="definition">ncprod_def</span></a> <span class="id" title="var">n'</span><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">]</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#db944dcc0a08a3bc9a79ca11eb10ad09"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#db944dcc0a08a3bc9a79ca11eb10ad09"><span class="id" title="notation">finGroupType</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#db944dcc0a08a3bc9a79ca11eb10ad09"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#subg_of"><span class="id" title="inductive">subg_of</span></a> <a class="idref" href="mathcomp.solvable.center.html#9990242b7e6de5c04ea1d8d95f316d83"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#9990242b7e6de5c04ea1d8d95f316d83"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#9990242b7e6de5c04ea1d8d95f316d83"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#IterCprod.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.center.html#9990242b7e6de5c04ea1d8d95f316d83"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#db944dcc0a08a3bc9a79ca11eb10ad09"><span class="id" title="notation">]</span></a>.<br/>
<span class="id" title="keyword">Fact</span> <a name="ncprod_key"><span class="id" title="lemma">ncprod_key</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a>.  <br/>
<span class="id" title="keyword">Definition</span> <a name="ncprod"><span class="id" title="definition">ncprod</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#locked_with"><span class="id" title="definition">locked_with</span></a> <a class="idref" href="mathcomp.solvable.center.html#ncprod_key"><span class="id" title="lemma">ncprod_key</span></a> <a class="idref" href="mathcomp.solvable.center.html#ncprod_def"><span class="id" title="definition">ncprod_def</span></a>.<br/>

<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="ncprod0"><span class="id" title="lemma">ncprod0</span></a> : <a class="idref" href="mathcomp.solvable.center.html#G_"><span class="id" title="abbreviation">G_</span></a> 0 <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.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#IterCprod.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a>.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="center_ncprod0"><span class="id" title="lemma">center_ncprod0</span></a> : <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#G_"><span class="id" title="abbreviation">G_</span></a> 0<a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#G_"><span class="id" title="abbreviation">G_</span></a> 0.<br/>
 
<br/>
<span class="id" title="keyword">Lemma</span> <a name="center_ncprod"><span class="id" title="lemma">center_ncprod</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#G_"><span class="id" title="abbreviation">G_</span></a> <a class="idref" href="mathcomp.solvable.center.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><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.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#IterCprod.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="ncprodS"><span class="id" title="lemma">ncprodS</span></a> <span class="id" title="var">n</span> : <a class="idref" href="mathcomp.solvable.center.html#xcprod_spec"><span class="id" title="inductive">xcprod_spec</span></a> <a class="idref" href="mathcomp.solvable.center.html#IterCprod.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.center.html#ncprod"><span class="id" title="definition">ncprod</span></a> <a class="idref" href="mathcomp.solvable.center.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a9a62cd128c968b470b51a9773e2f64a"><span class="id" title="notation">]</span></a> (<a class="idref" href="mathcomp.solvable.center.html#ncprod"><span class="id" title="definition">ncprod</span></a> <a class="idref" href="mathcomp.solvable.center.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a>).<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="ncprod1"><span class="id" title="lemma">ncprod1</span></a> : <a class="idref" href="mathcomp.solvable.center.html#G_"><span class="id" title="abbreviation">G_</span></a> 1 <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.center.html#IterCprod.G"><span class="id" title="variable">G</span></a>.<br/>

<br/>
<span class="id" title="keyword">Lemma</span> <a name="Aut_ncprod_full"><span class="id" title="lemma">Aut_ncprod_full</span></a> <span class="id" title="var">n</span> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.action.html#Aut_in"><span class="id" title="definition">Aut_in</span></a> (<a class="idref" href="mathcomp.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.solvable.center.html#IterCprod.G"><span class="id" title="variable">G</span></a>) <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#IterCprod.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.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.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#IterCprod.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.action.html#Aut_in"><span class="id" title="definition">Aut_in</span></a> (<a class="idref" href="mathcomp.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> (<a class="idref" href="mathcomp.solvable.center.html#G_"><span class="id" title="abbreviation">G_</span></a> <a class="idref" href="mathcomp.solvable.center.html#n"><span class="id" title="variable">n</span></a>)) <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#G_"><span class="id" title="abbreviation">G_</span></a> <a class="idref" href="mathcomp.solvable.center.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><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.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#G_"><span class="id" title="abbreviation">G_</span></a> <a class="idref" href="mathcomp.solvable.center.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.center.html#07d637974acf808c1caadc3b5bdfa6d3"><span class="id" title="notation">)</span></a>.<br/>

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

<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>