diff options
| author | Cyril Cohen | 2019-10-16 11:26:43 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2019-10-16 11:26:43 +0200 |
| commit | 6b59540a2460633df4e3d8347cb4dfe2fb3a3afb (patch) | |
| tree | 1239c1d5553d51a7d73f2f8b465f6a23178ff8a0 /docs/htmldoc/mathcomp.solvable.center.html | |
| parent | dd82aaeae7e9478efc178ce8430986649555b032 (diff) | |
removing everything but index which redirects to the new page
Diffstat (limited to 'docs/htmldoc/mathcomp.solvable.center.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.solvable.center.html | 527 |
1 files changed, 0 insertions, 527 deletions
diff --git a/docs/htmldoc/mathcomp.solvable.center.html b/docs/htmldoc/mathcomp.solvable.center.html deleted file mode 100644 index 1a276f1..0000000 --- a/docs/htmldoc/mathcomp.solvable.center.html +++ /dev/null @@ -1,527 +0,0 @@ -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" -"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> -<html xmlns="http://www.w3.org/1999/xhtml"> -<head> -<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> -<link href="coqdoc.css" rel="stylesheet" type="text/css" /> -<title>mathcomp.solvable.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">(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. <br/> - Distributed under the terms of CeCILL-B. *)</span><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 >-> rT} - and fK : {morphism K >-> 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#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><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#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>) := <a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">C_A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><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#04a5555c0db8685a27679a7e6af3f8c3"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.center.html#Defs.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.center.html#Defs.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a> :=<br/> - <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#f6996ff347e6cf832aa130837b06a848"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#f6996ff347e6cf832aa130837b06a848"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f6996ff347e6cf832aa130837b06a848"><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#f6996ff347e6cf832aa130837b06a848"><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="e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">"</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="8214bae0e5e0f19094855e75423d0dac"><span class="id" title="notation">"</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#c0205c751a17b7793ccdaf02cc4999e3"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#c0205c751a17b7793ccdaf02cc4999e3"><span class="id" title="notation">igFun</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#c0205c751a17b7793ccdaf02cc4999e3"><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#c0205c751a17b7793ccdaf02cc4999e3"><span class="id" title="notation">&</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#c0205c751a17b7793ccdaf02cc4999e3"><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#cecbde1597e0d77a491e8c4f94033af4"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#cecbde1597e0d77a491e8c4f94033af4"><span class="id" title="notation">gFun</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#cecbde1597e0d77a491e8c4f94033af4"><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#cecbde1597e0d77a491e8c4f94033af4"><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#f4a0ec7c18bd128b271d4428328fd43b"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#f4a0ec7c18bd128b271d4428328fd43b"><span class="id" title="notation">pgFun</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#f4a0ec7c18bd128b271d4428328fd43b"><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#f4a0ec7c18bd128b271d4428328fd43b"><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#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><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#d8708f36d374a98f4d683c7593d1ea6a"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.center.html#Center.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="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/V8.9.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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.center.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#ba2b0e492d2b4675a0acf3ea92aabadd"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">C_A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><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#04a5555c0db8685a27679a7e6af3f8c3"><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#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">C_A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><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#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#ee98cf35a816a182ecdf169a5f07c7f5"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ee98cf35a816a182ecdf169a5f07c7f5"><span class="id" title="notation">N_A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ee98cf35a816a182ecdf169a5f07c7f5"><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#ee98cf35a816a182ecdf169a5f07c7f5"><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#ee98cf35a816a182ecdf169a5f07c7f5"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ee98cf35a816a182ecdf169a5f07c7f5"><span class="id" title="notation">N_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ee98cf35a816a182ecdf169a5f07c7f5"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ee98cf35a816a182ecdf169a5f07c7f5"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><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#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7e8095b432e7aa5c3c22bb87584658b7"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#ee98cf35a816a182ecdf169a5f07c7f5"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ee98cf35a816a182ecdf169a5f07c7f5"><span class="id" title="notation">N_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ee98cf35a816a182ecdf169a5f07c7f5"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ee98cf35a816a182ecdf169a5f07c7f5"><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#d9dc63f0c53bc5e6f232c50d48c40709"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#d9dc63f0c53bc5e6f232c50d48c40709"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#d9dc63f0c53bc5e6f232c50d48c40709"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#d9dc63f0c53bc5e6f232c50d48c40709"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">C_H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#d9dc63f0c53bc5e6f232c50d48c40709"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#d9dc63f0c53bc5e6f232c50d48c40709"><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/V8.9.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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.center.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#ba2b0e492d2b4675a0acf3ea92aabadd"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">(</span></a>1<a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">=</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">:></span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><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#d8708f36d374a98f4d683c7593d1ea6a"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7e8095b432e7aa5c3c22bb87584658b7"><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="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#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.center.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7e8095b432e7aa5c3c22bb87584658b7"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.solvable.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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#d9dc63f0c53bc5e6f232c50d48c40709"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#d9dc63f0c53bc5e6f232c50d48c40709"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.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/> - <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><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#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.ssreflect.bigop.html#cd344b81961f1f1b59f55b98384ad290"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#cd344b81961f1f1b59f55b98384ad290"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#cd344b81961f1f1b59f55b98384ad290"><span class="id" title="notation">(</span></a><span class="id" title="var">xG</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#cd344b81961f1f1b59f55b98384ad290"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#1e993786ab46c6f2c0d488e43f629b71"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#1e993786ab46c6f2c0d488e43f629b71"><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#38a288b01c62a2a6a720c34fc1fffe2c"><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#1e993786ab46c6f2c0d488e43f629b71"><span class="id" title="notation">|</span></a> <span class="id" title="var">x</span> <a class="idref" href="mathcomp.ssreflect.finset.html#1e993786ab46c6f2c0d488e43f629b71"><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#160b1f5d5c3e3c6d274924649d717d8d"><span class="id" title="notation">:\:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#313ef60ac6c7566906fa5b28c1bbf405"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#313ef60ac6c7566906fa5b28c1bbf405"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#313ef60ac6c7566906fa5b28c1bbf405"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#313ef60ac6c7566906fa5b28c1bbf405"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#1e993786ab46c6f2c0d488e43f629b71"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#cd344b81961f1f1b59f55b98384ad290"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.center.html#xG"><span class="id" title="variable">xG</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a>.<br/> - -<br/> -<span class="id" title="keyword">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/V8.9.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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.center.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#ba2b0e492d2b4675a0acf3ea92aabadd"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">C_A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><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#bb1f7e576b21e943bdeacc0f6a28b245"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.center.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.center.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><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#bb1f7e576b21e943bdeacc0f6a28b245"><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#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><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#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.center.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.center.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><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#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.center.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><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#bb1f7e576b21e943bdeacc0f6a28b245"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.center.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#5e5825d099c952c2db2842c142cbde94"><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#5e5825d099c952c2db2842c142cbde94"><span class="id" title="notation">]></span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><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#bb1f7e576b21e943bdeacc0f6a28b245"><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#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><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#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#5e5825d099c952c2db2842c142cbde94"><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#5e5825d099c952c2db2842c142cbde94"><span class="id" title="notation">]></span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.center.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#5e5825d099c952c2db2842c142cbde94"><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#5e5825d099c952c2db2842c142cbde94"><span class="id" title="notation">]></span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7e8095b432e7aa5c3c22bb87584658b7"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><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#bb1f7e576b21e943bdeacc0f6a28b245"><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#3e65ad3edf5f7fb3ea6bc63a878112a8"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#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/> - <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#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.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#3e65ad3edf5f7fb3ea6bc63a878112a8"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.center.html#Center.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) (<a name="Center.Injm.f"><span class="id" title="variable">f</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><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#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">>-></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#efe2275bee4a5227161b40da886719a5"><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#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.solvable.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#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.center.html#Center.Injm.D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.center.html#Center.Injm.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#70b0a61e30f130888503421fd44e1802"><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#e90cc03a62af307fc4e121114703663b"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.center.html#aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">H</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.center.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) :<br/> - <a class="idref" href="mathcomp.solvable.center.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><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#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><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#d8708f36d374a98f4d683c7593d1ea6a"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.center.html#Product.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="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#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#313ef60ac6c7566906fa5b28c1bbf405"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#313ef60ac6c7566906fa5b28c1bbf405"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#313ef60ac6c7566906fa5b28c1bbf405"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#313ef60ac6c7566906fa5b28c1bbf405"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#8b8794efbfbae1b793d9cb62ce802285"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#8b8794efbfbae1b793d9cb62ce802285"><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#e90cc03a62af307fc4e121114703663b"><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#1c2e0971edf6e9b6c6dd4a5951d04f36"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#1c2e0971edf6e9b6c6dd4a5951d04f36"><span class="id" title="notation">\*</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><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#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>) <span class="id" title="var">G</span> :<br/> - <a class="idref" href="mathcomp.ssreflect.bigop.html#60e57ff387b8a0840e944d0d03f215e2"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#60e57ff387b8a0840e944d0d03f215e2"><span class="id" title="notation">big</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#60e57ff387b8a0840e944d0d03f215e2"><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#60e57ff387b8a0840e944d0d03f215e2"><span class="id" title="notation">/</span></a>1<a class="idref" href="mathcomp.ssreflect.bigop.html#60e57ff387b8a0840e944d0d03f215e2"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#60e57ff387b8a0840e944d0d03f215e2"><span class="id" title="notation">_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#60e57ff387b8a0840e944d0d03f215e2"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#60e57ff387b8a0840e944d0d03f215e2"><span class="id" title="notation"><-</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#60e57ff387b8a0840e944d0d03f215e2"><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#60e57ff387b8a0840e944d0d03f215e2"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.ssreflect.bigop.html#60e57ff387b8a0840e944d0d03f215e2"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#60e57ff387b8a0840e944d0d03f215e2"><span class="id" title="notation">big</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#60e57ff387b8a0840e944d0d03f215e2"><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#60e57ff387b8a0840e944d0d03f215e2"><span class="id" title="notation">/</span></a>1<a class="idref" href="mathcomp.ssreflect.bigop.html#60e57ff387b8a0840e944d0d03f215e2"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#60e57ff387b8a0840e944d0d03f215e2"><span class="id" title="notation">_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#60e57ff387b8a0840e944d0d03f215e2"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#60e57ff387b8a0840e944d0d03f215e2"><span class="id" title="notation"><-</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#60e57ff387b8a0840e944d0d03f215e2"><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#60e57ff387b8a0840e944d0d03f215e2"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><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#1c2e0971edf6e9b6c6dd4a5951d04f36"><span class="id" title="notation">\*</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.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#191b5570f070a51bd5c860222c206828"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.gproduct.html#191b5570f070a51bd5c860222c206828"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#191b5570f070a51bd5c860222c206828"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.gproduct.html#191b5570f070a51bd5c860222c206828"><span class="id" title="notation">x</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><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#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>) <span class="id" title="var">G</span> :<br/> - <a class="idref" href="mathcomp.ssreflect.bigop.html#60e57ff387b8a0840e944d0d03f215e2"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#60e57ff387b8a0840e944d0d03f215e2"><span class="id" title="notation">big</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#60e57ff387b8a0840e944d0d03f215e2"><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#60e57ff387b8a0840e944d0d03f215e2"><span class="id" title="notation">/</span></a>1<a class="idref" href="mathcomp.ssreflect.bigop.html#60e57ff387b8a0840e944d0d03f215e2"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#60e57ff387b8a0840e944d0d03f215e2"><span class="id" title="notation">_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#60e57ff387b8a0840e944d0d03f215e2"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#60e57ff387b8a0840e944d0d03f215e2"><span class="id" title="notation"><-</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#60e57ff387b8a0840e944d0d03f215e2"><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#60e57ff387b8a0840e944d0d03f215e2"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.ssreflect.bigop.html#60e57ff387b8a0840e944d0d03f215e2"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#60e57ff387b8a0840e944d0d03f215e2"><span class="id" title="notation">big</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#60e57ff387b8a0840e944d0d03f215e2"><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#60e57ff387b8a0840e944d0d03f215e2"><span class="id" title="notation">/</span></a>1<a class="idref" href="mathcomp.ssreflect.bigop.html#60e57ff387b8a0840e944d0d03f215e2"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#60e57ff387b8a0840e944d0d03f215e2"><span class="id" title="notation">_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#60e57ff387b8a0840e944d0d03f215e2"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#60e57ff387b8a0840e944d0d03f215e2"><span class="id" title="notation"><-</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#60e57ff387b8a0840e944d0d03f215e2"><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#60e57ff387b8a0840e944d0d03f215e2"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><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/> - <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#1c2e0971edf6e9b6c6dd4a5951d04f36"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.fingroup.action.html#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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.fingroup.action.html#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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.fingroup.action.html#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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.gTH"><span class="id" title="variable">gTH</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.gTK"><span class="id" title="variable">gTK</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><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#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><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="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><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/> - <a class="idref" href="mathcomp.ssreflect.finset.html#9e3f1d0cf47c39e3927b1f03a0797327"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#9e3f1d0cf47c39e3927b1f03a0797327"><span class="id" title="notation">set</span></a> <span class="id" title="var">xy</span> <a class="idref" href="mathcomp.ssreflect.finset.html#9e3f1d0cf47c39e3927b1f03a0797327"><span class="id" title="notation">|</span></a> <span class="id" title="keyword">let</span>: <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <span class="id" title="var">y</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><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/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">(</span></a><span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">&&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">(</span></a><span class="id" title="var">y</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#766fd55608aa0e125ed6f55c83bcc09a"><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#766fd55608aa0e125ed6f55c83bcc09a"><span class="id" title="notation">)^-1</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#9e3f1d0cf47c39e3927b1f03a0797327"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><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#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.solvable.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#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><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#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#d9dc63f0c53bc5e6f232c50d48c40709"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#d9dc63f0c53bc5e6f232c50d48c40709"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><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#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><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#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.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#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><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/V8.9.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#f6996ff347e6cf832aa130837b06a848"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#f6996ff347e6cf832aa130837b06a848"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f6996ff347e6cf832aa130837b06a848"><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#3e65ad3edf5f7fb3ea6bc63a878112a8"><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#f6996ff347e6cf832aa130837b06a848"><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/V8.9.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/V8.9.0/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/> - <span class="id" title="keyword">let</span>: <a class="idref" href="http://coq.inria.fr/distrib/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.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/> - <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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8b4742e3f67816503ce4ab2f3b81c27e"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8b4742e3f67816503ce4ab2f3b81c27e"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">&,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><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#8b8794efbfbae1b793d9cb62ce802285"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><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#7ef99623452370540bbc44fd30b0bc94"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#7ef99623452370540bbc44fd30b0bc94"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#fbc46ef185231593d182602cec4ac134"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#fbc46ef185231593d182602cec4ac134"><span class="id" title="notation">dom</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#fbc46ef185231593d182602cec4ac134"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8b4742e3f67816503ce4ab2f3b81c27e"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8b4742e3f67816503ce4ab2f3b81c27e"><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#fbc46ef185231593d182602cec4ac134"><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#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#fbc46ef185231593d182602cec4ac134"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#fbc46ef185231593d182602cec4ac134"><span class="id" title="notation">dom</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#fbc46ef185231593d182602cec4ac134"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8b4742e3f67816503ce4ab2f3b81c27e"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8b4742e3f67816503ce4ab2f3b81c27e"><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#fbc46ef185231593d182602cec4ac134"><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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.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#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.solvable.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#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.solvable.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#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#313ef60ac6c7566906fa5b28c1bbf405"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#313ef60ac6c7566906fa5b28c1bbf405"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#313ef60ac6c7566906fa5b28c1bbf405"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#CH"><span class="id" title="abbreviation">CH</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#313ef60ac6c7566906fa5b28c1bbf405"><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> : <span class="id" title="var">core</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#8b8794efbfbae1b793d9cb62ce802285"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#1c2e0971edf6e9b6c6dd4a5951d04f36"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8b4742e3f67816503ce4ab2f3b81c27e"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8b4742e3f67816503ce4ab2f3b81c27e"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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#b9596739b058766532fc6517a36fef9f"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><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#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><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#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><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#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><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#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">>-></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#efe2275bee4a5227161b40da886719a5"><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#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><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#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">>-></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#efe2275bee4a5227161b40da886719a5"><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#70b0a61e30f130888503421fd44e1802"><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#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#313ef60ac6c7566906fa5b28c1bbf405"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#313ef60ac6c7566906fa5b28c1bbf405"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#313ef60ac6c7566906fa5b28c1bbf405"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#CprodBy.ExtCprodm.fH"><span class="id" title="variable">fH</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><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#313ef60ac6c7566906fa5b28c1bbf405"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8b4742e3f67816503ce4ab2f3b81c27e"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8b4742e3f67816503ce4ab2f3b81c27e"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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#70b0a61e30f130888503421fd44e1802"><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#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#313ef60ac6c7566906fa5b28c1bbf405"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#313ef60ac6c7566906fa5b28c1bbf405"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#313ef60ac6c7566906fa5b28c1bbf405"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.center.html#CprodBy.ExtCprodm.gH"><span class="id" title="variable">gH</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><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#313ef60ac6c7566906fa5b28c1bbf405"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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#b9596739b058766532fc6517a36fef9f"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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#d22b43813ec744a6a8786f15c9267991"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#d22b43813ec744a6a8786f15c9267991"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#d22b43813ec744a6a8786f15c9267991"><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#d22b43813ec744a6a8786f15c9267991"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><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/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5f76d9959f82823e4253cd67e7dc0e96"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5f76d9959f82823e4253cd67e7dc0e96"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5f76d9959f82823e4253cd67e7dc0e96"><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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5f76d9959f82823e4253cd67e7dc0e96"><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#8b8794efbfbae1b793d9cb62ce802285"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#8b8794efbfbae1b793d9cb62ce802285"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5f76d9959f82823e4253cd67e7dc0e96"><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#70b0a61e30f130888503421fd44e1802"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#70b0a61e30f130888503421fd44e1802"><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#8b8794efbfbae1b793d9cb62ce802285"><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#70b0a61e30f130888503421fd44e1802"><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#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><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#70b0a61e30f130888503421fd44e1802"><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#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.ExtCprodm.fH"><span class="id" title="variable">fH</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><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#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><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#70b0a61e30f130888503421fd44e1802"><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#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.ExtCprodm.fK"><span class="id" title="variable">fK</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><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#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.solvable.center.html#xcprodm"><span class="id" title="definition">xcprodm</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.ExtCprodm.fH"><span class="id" title="variable">fH</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">&&</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.solvable.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/> - <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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.fingroup.action.html#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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.fingroup.action.html#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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.gTK"><span class="id" title="variable">gTK</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) :<br/> - <a class="idref" href="mathcomp.solvable.center.html#Y"><span class="id" title="variable">Y</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.center.html#CprodBy.gz"><span class="id" title="variable">gz</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.center.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><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#1c2e0971edf6e9b6c6dd4a5951d04f36"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#b9596739b058766532fc6517a36fef9f"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><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#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><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#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><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/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <span class="id" title="var">f</span> : <a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><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#efe2275bee4a5227161b40da886719a5"><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><a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">[/\</span></a> <a class="idref" href="mathcomp.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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><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#70b0a61e30f130888503421fd44e1802"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><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#70b0a61e30f130888503421fd44e1802"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><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#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.center.html#ExtCprod.gTH"><span class="id" title="variable">gTH</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.center.html#ExtCprod.gTK"><span class="id" title="variable">gTK</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>).<br/> - -<br/> -<span class="id" title="keyword">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/V8.9.0/stdlib//Coq.ssr.ssreflect.html#00a1a5b58aac8f1e3f1abff064a39f9d"><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/V8.9.0/stdlib//Coq.ssr.ssreflect.html#00a1a5b58aac8f1e3f1abff064a39f9d"><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/V8.9.0/stdlib//Coq.ssr.ssreflect.html#00a1a5b58aac8f1e3f1abff064a39f9d"><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/V8.9.0/stdlib//Coq.ssr.ssreflect.html#e415736924b98865ec80fc8682078da1"><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/V8.9.0/stdlib//Coq.ssr.ssreflect.html#e415736924b98865ec80fc8682078da1"><span class="id" title="notation">as</span></a> <span class="id" title="var">b'</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#e415736924b98865ec80fc8682078da1"><span class="id" title="notation">return</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#e415736924b98865ec80fc8682078da1"><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/V8.9.0/stdlib//Coq.ssr.ssreflect.html#e415736924b98865ec80fc8682078da1"><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/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#6556914db359db999889decec6a4a562"><span class="id" title="notation">{</span></a><span class="id" title="var">gz</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#6556914db359db999889decec6a4a562"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">>-></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#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#6556914db359db999889decec6a4a562"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><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/V8.9.0/stdlib//Coq.Init.Specif.html#6556914db359db999889decec6a4a562"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <span class="id" title="keyword">Prop</span> :=<br/> - <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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.center.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) :<br/> - <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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.solvable.center.html#GH"><span class="id" title="variable">GH</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#1c2e0971edf6e9b6c6dd4a5951d04f36"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.solvable.center.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d1cce020b4b43370087fd70de1477ab6"><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#d1cce020b4b43370087fd70de1477ab6"><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#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.center.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>).<br/> - -<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/> - <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#bda89d73ec4a8f23ae92b565ffb5aaa6"><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#e98634a3dc0445a0bdea71fc5975bb33"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#e98634a3dc0445a0bdea71fc5975bb33"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#e98634a3dc0445a0bdea71fc5975bb33"><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#e98634a3dc0445a0bdea71fc5975bb33"><span class="id" title="notation">]</span></a><br/> - <span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#2bd77263376cf9e19a7b9689cc638b8a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#2bd77263376cf9e19a7b9689cc638b8a"><span class="id" title="notation">finGroupType</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#2bd77263376cf9e19a7b9689cc638b8a"><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#8214bae0e5e0f19094855e75423d0dac"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#8214bae0e5e0f19094855e75423d0dac"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#8214bae0e5e0f19094855e75423d0dac"><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#8214bae0e5e0f19094855e75423d0dac"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#2bd77263376cf9e19a7b9689cc638b8a"><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/V8.9.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/V8.9.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#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><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#e98634a3dc0445a0bdea71fc5975bb33"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#e98634a3dc0445a0bdea71fc5975bb33"><span class="id" title="notation">set</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#e98634a3dc0445a0bdea71fc5975bb33"><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#e98634a3dc0445a0bdea71fc5975bb33"><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#bda89d73ec4a8f23ae92b565ffb5aaa6"><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#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><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/> - <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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.fingroup.action.html#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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><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#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><span class="id" title="notation">Z</span></a><a class="idref" href="mathcomp.solvable.center.html#e90cc03a62af307fc4e121114703663b"><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#e90cc03a62af307fc4e121114703663b"><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>
\ No newline at end of file |