htmldoc regenerated

author: Enrico Tassi 2019-05-22 13:43:08 +0200
committer: Enrico Tassi 2019-05-22 15:34:14 +0200
commit: 748d716efb2f2f75946c8386e441ce1789806a39 (patch)
tree: fe7bb1c5235550410c64e968f4a4d69b7f10a047 /docs/htmldoc/mathcomp.solvable.gfunctor.html
parent: 415be3b908daadabf178a292c885db78e5b2c9a4 (diff)
1 files changed, 86 insertions, 87 deletions
diff --git a/docs/htmldoc/mathcomp.solvable.gfunctor.html b/docs/htmldoc/mathcomp.solvable.gfunctor.html
index 871ba2b..c5f3789 100644
--- a/docs/htmldoc/mathcomp.solvable.gfunctor.html
+++ b/docs/htmldoc/mathcomp.solvable.gfunctor.html
@@ -21,7 +21,6 @@
 <div class="code">
 <span class="comment">(*&nbsp;(c)&nbsp;Copyright&nbsp;2006-2016&nbsp;Microsoft&nbsp;Corporation&nbsp;and&nbsp;Inria.&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br/>
 &nbsp;Distributed&nbsp;under&nbsp;the&nbsp;terms&nbsp;of&nbsp;CeCILL-B.&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;*)</span><br/>
-<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#"><span class="id" title="library">mathcomp.ssreflect.ssreflect</span></a>.<br/>
 
 <br/>
 </div>
@@ -117,7 +116,7 @@
 <span class="id" title="keyword">Module</span> <a name="GFunctor"><span class="id" title="module">GFunctor</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Definition</span> <a name="GFunctor.object_map"><span class="id" title="definition">object_map</span></a> := <span class="id" title="keyword">∀</span> <span class="id" title="var">gT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>, <a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="GFunctor.object_map"><span class="id" title="definition">object_map</span></a> := <span class="id" title="keyword">∀</span> <span class="id" title="var">gT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>, <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.gfunctor.html#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="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.gfunctor.html#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/>
 
@@ -137,7 +136,7 @@
  Group closure.  
 </div>
 <div class="code">
-<span class="id" title="keyword">Definition</span> <a name="GFunctor.group_valued"><span class="id" title="definition">group_valued</span></a> := <span class="id" title="keyword">∀</span> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>), <a class="idref" href="mathcomp.fingroup.fingroup.html#group_set"><span class="id" title="definition">group_set</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>).<br/>
+<span class="id" title="keyword">Definition</span> <a name="GFunctor.group_valued"><span class="id" title="definition">group_valued</span></a> := <span class="id" title="keyword">∀</span> <span class="id" title="var">gT</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.gfunctor.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>), <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.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>).<br/>
 
 <br/>
 </div>
@@ -146,7 +145,7 @@
  Subgroup closure.  
 </div>
 <div class="code">
-<span class="id" title="keyword">Definition</span> <a name="GFunctor.closed"><span class="id" title="definition">closed</span></a> := <span class="id" title="keyword">∀</span> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>), <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="GFunctor.closed"><span class="id" title="definition">closed</span></a> := <span class="id" title="keyword">∀</span> <span class="id" title="var">gT</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.gfunctor.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>), <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.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.gfunctor.html#G"><span class="id" title="variable">G</span></a>.<br/>
 
 <br/>
 </div>
@@ -156,8 +155,8 @@
 </div>
 <div class="code">
 <span class="id" title="keyword">Definition</span> <a name="GFunctor.continuous"><span class="id" title="definition">continuous</span></a> :=<br/>
-&nbsp;&nbsp;<span class="id" title="keyword">∀</span> <span class="id" title="var">gT</span> <span class="id" title="var">hT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">phi</span> : <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#hT"><span class="id" title="variable">hT</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">}</span></a>),<br/>
-&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.gfunctor.html#phi"><span class="id" title="variable">phi</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#phi"><span class="id" title="variable">phi</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>).<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">∀</span> <span class="id" title="var">gT</span> <span class="id" title="var">hT</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.gfunctor.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>) (<span class="id" title="var">phi</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.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#hT"><span class="id" title="variable">hT</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">}</span></a>),<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.gfunctor.html#phi"><span class="id" title="variable">phi</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.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.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#phi"><span class="id" title="variable">phi</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>).<br/>
 
 <br/>
 </div>
@@ -167,11 +166,11 @@
 </div>
 <div class="code">
 <span class="id" title="keyword">Definition</span> <a name="GFunctor.iso_continuous"><span class="id" title="definition">iso_continuous</span></a> :=<br/>
-&nbsp;&nbsp;<span class="id" title="keyword">∀</span> <span class="id" title="var">gT</span> <span class="id" title="var">hT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">phi</span> : <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#hT"><span class="id" title="variable">hT</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">}</span></a>),<br/>
-&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.morphism.html#14bfb149f00fa839cfb11397f4fe629f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#14bfb149f00fa839cfb11397f4fe629f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#phi"><span class="id" title="variable">phi</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#phi"><span class="id" title="variable">phi</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#phi"><span class="id" title="variable">phi</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>).<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">∀</span> <span class="id" title="var">gT</span> <span class="id" title="var">hT</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.gfunctor.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>) (<span class="id" title="var">phi</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.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#hT"><span class="id" title="variable">hT</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">}</span></a>),<br/>
+&nbsp;&nbsp;&nbsp;<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.gfunctor.html#phi"><span class="id" title="variable">phi</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.gfunctor.html#phi"><span class="id" title="variable">phi</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.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.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#phi"><span class="id" title="variable">phi</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>).<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="GFunctor.continuous_is_iso_continuous"><span class="id" title="lemma">continuous_is_iso_continuous</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.continuous"><span class="id" title="definition">continuous</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.iso_continuous"><span class="id" title="definition">iso_continuous</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="GFunctor.continuous_is_iso_continuous"><span class="id" title="lemma">continuous_is_iso_continuous</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.continuous"><span class="id" title="definition">continuous</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.gfunctor.html#GFunctor.iso_continuous"><span class="id" title="definition">iso_continuous</span></a>.<br/>
  
 <br/>
 </div>
@@ -181,11 +180,11 @@
 </div>
 <div class="code">
 <span class="id" title="keyword">Definition</span> <a name="GFunctor.pcontinuous"><span class="id" title="definition">pcontinuous</span></a> :=<br/>
-&nbsp;&nbsp;<span class="id" title="keyword">∀</span> <span class="id" title="var">gT</span> <span class="id" title="var">hT</span> (<span class="id" title="var">G</span> <span class="id" title="var">D</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">phi</span> : <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#hT"><span class="id" title="variable">hT</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">}</span></a>),<br/>
-&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.gfunctor.html#phi"><span class="id" title="variable">phi</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#phi"><span class="id" title="variable">phi</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>).<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">∀</span> <span class="id" title="var">gT</span> <span class="id" title="var">hT</span> (<span class="id" title="var">G</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.gfunctor.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>) (<span class="id" title="var">phi</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.gfunctor.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#hT"><span class="id" title="variable">hT</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">}</span></a>),<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.gfunctor.html#phi"><span class="id" title="variable">phi</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.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.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#phi"><span class="id" title="variable">phi</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>).<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="GFunctor.pcontinuous_is_continuous"><span class="id" title="lemma">pcontinuous_is_continuous</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pcontinuous"><span class="id" title="definition">pcontinuous</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.continuous"><span class="id" title="definition">continuous</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="GFunctor.pcontinuous_is_continuous"><span class="id" title="lemma">pcontinuous_is_continuous</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pcontinuous"><span class="id" title="definition">pcontinuous</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.gfunctor.html#GFunctor.continuous"><span class="id" title="definition">continuous</span></a>.<br/>
  
 <br/>
 </div>
@@ -195,10 +194,10 @@
 </div>
 <div class="code">
 <span class="id" title="keyword">Definition</span> <a name="GFunctor.hereditary"><span class="id" title="definition">hereditary</span></a> :=<br/>
-&nbsp;&nbsp;<span class="id" title="keyword">∀</span> <span class="id" title="var">gT</span> (<span class="id" title="var">H</span> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>), <a class="idref" href="mathcomp.solvable.gfunctor.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#cb41714a5a23482f7a48a98975fa8c59"><span class="id" title="notation">:&amp;:</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#H"><span class="id" title="variable">H</span></a>.<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">∀</span> <span class="id" title="var">gT</span> (<span class="id" title="var">H</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.gfunctor.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>), <a class="idref" href="mathcomp.solvable.gfunctor.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.gfunctor.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.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#b9596739b058766532fc6517a36fef9f"><span class="id" title="notation">:&amp;:</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.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.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#H"><span class="id" title="variable">H</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="GFunctor.pcontinuous_is_hereditary"><span class="id" title="lemma">pcontinuous_is_hereditary</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pcontinuous"><span class="id" title="definition">pcontinuous</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.hereditary"><span class="id" title="definition">hereditary</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="GFunctor.pcontinuous_is_hereditary"><span class="id" title="lemma">pcontinuous_is_hereditary</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pcontinuous"><span class="id" title="definition">pcontinuous</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.gfunctor.html#GFunctor.hereditary"><span class="id" title="definition">hereditary</span></a>.<br/>
 
 <br/>
 </div>
@@ -208,7 +207,7 @@
 </div>
 <div class="code">
 <span class="id" title="keyword">Definition</span> <a name="GFunctor.monotonic"><span class="id" title="definition">monotonic</span></a> :=<br/>
-&nbsp;&nbsp;<span class="id" title="keyword">∀</span> <span class="id" title="var">gT</span> (<span class="id" title="var">H</span> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>), <a class="idref" href="mathcomp.solvable.gfunctor.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>.<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">∀</span> <span class="id" title="var">gT</span> (<span class="id" title="var">H</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.gfunctor.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>), <a class="idref" href="mathcomp.solvable.gfunctor.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.gfunctor.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.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.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.gfunctor.html#GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>.<br/>
 
 <br/>
 </div>
@@ -219,14 +218,14 @@
 <div class="code">
 
 <br/>
-<span class="id" title="keyword">Variables</span> (<a name="GFunctor.Definitions.k"><span class="id" title="variable">k</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a>) (<a name="GFunctor.Definitions.F1"><span class="id" title="variable">F1</span></a> <a name="GFunctor.Definitions.F2"><span class="id" title="variable">F2</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.object_map"><span class="id" title="definition">object_map</span></a>).<br/>
+<span class="id" title="keyword">Variables</span> (<a name="GFunctor.Definitions.k"><span class="id" title="variable">k</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>) (<a name="GFunctor.Definitions.F1"><span class="id" title="variable">F1</span></a> <a name="GFunctor.Definitions.F2"><span class="id" title="variable">F2</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.object_map"><span class="id" title="definition">object_map</span></a>).<br/>
 
 <br/>
-<span class="id" title="keyword">Definition</span> <a name="GFunctor.comp_head"><span class="id" title="definition">comp_head</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.object_map"><span class="id" title="definition">object_map</span></a> := <span class="id" title="keyword">fun</span> <span class="id" title="var">gT</span> <span class="id" title="var">A</span> ⇒ <span class="id" title="keyword">let</span>: <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#tt"><span class="id" title="constructor">tt</span></a> := <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.k"><span class="id" title="variable">k</span></a> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F1"><span class="id" title="variable">F1</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F2"><span class="id" title="variable">F2</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#A"><span class="id" title="variable">A</span></a>).<br/>
+<span class="id" title="keyword">Definition</span> <a name="GFunctor.comp_head"><span class="id" title="definition">comp_head</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.object_map"><span class="id" title="definition">object_map</span></a> := <span class="id" title="keyword">fun</span> <span class="id" title="var">gT</span> <span class="id" title="var">A</span> ⇒ <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> := <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.k"><span class="id" title="variable">k</span></a> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F1"><span class="id" title="variable">F1</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F2"><span class="id" title="variable">F2</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#A"><span class="id" title="variable">A</span></a>).<br/>
 
 <br/>
 <span class="id" title="keyword">Definition</span> <a name="GFunctor.modulo"><span class="id" title="definition">modulo</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.object_map"><span class="id" title="definition">object_map</span></a> :=<br/>
-&nbsp;&nbsp;<span class="id" title="keyword">fun</span> <span class="id" title="var">gT</span> <span class="id" title="var">A</span> ⇒ <a class="idref" href="mathcomp.fingroup.quotient.html#coset"><span class="id" title="definition">coset</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F2"><span class="id" title="variable">F2</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#A"><span class="id" title="variable">A</span></a>) <a class="idref" href="mathcomp.fingroup.morphism.html#619a2190d60a66179f3396458e2a09ae"><span class="id" title="notation">@*^-1</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#619a2190d60a66179f3396458e2a09ae"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F1"><span class="id" title="variable">F1</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#c7768147d2d560601601fbf95706ddcc"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#c7768147d2d560601601fbf95706ddcc"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F2"><span class="id" title="variable">F2</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.quotient.html#c7768147d2d560601601fbf95706ddcc"><span class="id" title="notation">)</span></a>)<a class="idref" href="mathcomp.fingroup.morphism.html#619a2190d60a66179f3396458e2a09ae"><span class="id" title="notation">)</span></a>.<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">fun</span> <span class="id" title="var">gT</span> <span class="id" title="var">A</span> ⇒ <a class="idref" href="mathcomp.fingroup.quotient.html#coset"><span class="id" title="definition">coset</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F2"><span class="id" title="variable">F2</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#A"><span class="id" title="variable">A</span></a>) <a class="idref" href="mathcomp.fingroup.morphism.html#320f70d30c9a649ec82642b364681418"><span class="id" title="notation">@*^-1</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#320f70d30c9a649ec82642b364681418"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F1"><span class="id" title="variable">F1</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#3e65ad3edf5f7fb3ea6bc63a878112a8"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#3e65ad3edf5f7fb3ea6bc63a878112a8"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions.F2"><span class="id" title="variable">F2</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.quotient.html#3e65ad3edf5f7fb3ea6bc63a878112a8"><span class="id" title="notation">)</span></a>)<a class="idref" href="mathcomp.fingroup.morphism.html#320f70d30c9a649ec82642b364681418"><span class="id" title="notation">)</span></a>.<br/>
 
 <br/>
 <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Definitions"><span class="id" title="section">Definitions</span></a>.<br/>
@@ -257,25 +256,25 @@
 <br/>
 <span class="id" title="keyword">Definition</span> <a name="GFunctor.clone_iso"><span class="id" title="definition">clone_iso</span></a> (<span class="id" title="var">F</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.object_map"><span class="id" title="definition">object_map</span></a>) :=<br/>
 &nbsp;&nbsp;<span class="id" title="keyword">fun</span> <span class="id" title="var">Fgrp</span> <span class="id" title="var">Fsub</span> <span class="id" title="var">Fcont</span> (<span class="id" title="var">isoF</span> := @<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.IsoMap"><span class="id" title="constructor">IsoMap</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#Fgrp"><span class="id" title="variable">Fgrp</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#Fsub"><span class="id" title="variable">Fsub</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#Fcont"><span class="id" title="variable">Fcont</span></a>) ⇒<br/>
-&nbsp;&nbsp;<span class="id" title="keyword">fun</span> <span class="id" title="var">isoF0</span> &amp; <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.apply"><span class="id" title="projection">apply</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#isoF0"><span class="id" title="variable">isoF0</span></a>) <a class="idref" href="mathcomp.solvable.gfunctor.html#F"><span class="id" title="variable">F</span></a> &amp; <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#isoF"><span class="id" title="variable">isoF</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#isoF0"><span class="id" title="variable">isoF0</span></a> ⇒ <a class="idref" href="mathcomp.solvable.gfunctor.html#isoF"><span class="id" title="variable">isoF</span></a>.<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">fun</span> <span class="id" title="var">isoF0</span> &amp; <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.apply"><span class="id" title="projection">apply</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#isoF0"><span class="id" title="variable">isoF0</span></a>) <a class="idref" href="mathcomp.solvable.gfunctor.html#F"><span class="id" title="variable">F</span></a> &amp; <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#isoF"><span class="id" title="variable">isoF</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#isoF0"><span class="id" title="variable">isoF0</span></a> ⇒ <a class="idref" href="mathcomp.solvable.gfunctor.html#isoF"><span class="id" title="variable">isoF</span></a>.<br/>
 
 <br/>
 <span class="id" title="keyword">Definition</span> <a name="GFunctor.clone"><span class="id" title="definition">clone</span></a> (<span class="id" title="var">F</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.object_map"><span class="id" title="definition">object_map</span></a>) :=<br/>
-&nbsp;&nbsp;<span class="id" title="keyword">fun</span> <span class="id" title="var">isoF</span> &amp; <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.apply"><span class="id" title="projection">apply</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#isoF"><span class="id" title="variable">isoF</span></a>) <a class="idref" href="mathcomp.solvable.gfunctor.html#F"><span class="id" title="variable">F</span></a> ⇒<br/>
-&nbsp;&nbsp;<span class="id" title="keyword">fun</span> (<span class="id" title="var">funF0</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.map"><span class="id" title="record">map</span></a>) &amp; <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.apply"><span class="id" title="projection">apply</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#funF0"><span class="id" title="variable">funF0</span></a>) <a class="idref" href="mathcomp.solvable.gfunctor.html#F"><span class="id" title="variable">F</span></a> ⇒<br/>
-&nbsp;&nbsp;<span class="id" title="keyword">fun</span> <span class="id" title="var">Fcont</span> (<span class="id" title="var">funF</span> := @<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Map"><span class="id" title="constructor">Map</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#isoF"><span class="id" title="variable">isoF</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#Fcont"><span class="id" title="variable">Fcont</span></a>) &amp; <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#funF0"><span class="id" title="variable">funF0</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#funF"><span class="id" title="variable">funF</span></a> ⇒ <a class="idref" href="mathcomp.solvable.gfunctor.html#funF"><span class="id" title="variable">funF</span></a>.<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">fun</span> <span class="id" title="var">isoF</span> &amp; <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.apply"><span class="id" title="projection">apply</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#isoF"><span class="id" title="variable">isoF</span></a>) <a class="idref" href="mathcomp.solvable.gfunctor.html#F"><span class="id" title="variable">F</span></a> ⇒<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">fun</span> (<span class="id" title="var">funF0</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.map"><span class="id" title="record">map</span></a>) &amp; <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.apply"><span class="id" title="projection">apply</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#funF0"><span class="id" title="variable">funF0</span></a>) <a class="idref" href="mathcomp.solvable.gfunctor.html#F"><span class="id" title="variable">F</span></a> ⇒<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">fun</span> <span class="id" title="var">Fcont</span> (<span class="id" title="var">funF</span> := @<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Map"><span class="id" title="constructor">Map</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#isoF"><span class="id" title="variable">isoF</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#Fcont"><span class="id" title="variable">Fcont</span></a>) &amp; <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#funF0"><span class="id" title="variable">funF0</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#funF"><span class="id" title="variable">funF</span></a> ⇒ <a class="idref" href="mathcomp.solvable.gfunctor.html#funF"><span class="id" title="variable">funF</span></a>.<br/>
 
 <br/>
 <span class="id" title="keyword">Definition</span> <a name="GFunctor.clone_pmap"><span class="id" title="definition">clone_pmap</span></a> (<span class="id" title="var">F</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.object_map"><span class="id" title="definition">object_map</span></a>) :=<br/>
-&nbsp;&nbsp;<span class="id" title="keyword">fun</span> (<span class="id" title="var">funF</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.map"><span class="id" title="record">map</span></a>) &amp; <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.apply"><span class="id" title="projection">apply</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#funF"><span class="id" title="variable">funF</span></a>) <a class="idref" href="mathcomp.solvable.gfunctor.html#F"><span class="id" title="variable">F</span></a> ⇒<br/>
-&nbsp;&nbsp;<span class="id" title="keyword">fun</span> (<span class="id" title="var">pfunF0</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pmap"><span class="id" title="record">pmap</span></a>) &amp; <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.apply"><span class="id" title="projection">apply</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#pfunF0"><span class="id" title="variable">pfunF0</span></a>) <a class="idref" href="mathcomp.solvable.gfunctor.html#F"><span class="id" title="variable">F</span></a> ⇒<br/>
-&nbsp;&nbsp;<span class="id" title="keyword">fun</span> <span class="id" title="var">Fher</span> (<span class="id" title="var">pfunF</span> := @<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Pmap"><span class="id" title="constructor">Pmap</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#funF"><span class="id" title="variable">funF</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#Fher"><span class="id" title="variable">Fher</span></a>) &amp; <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#pfunF0"><span class="id" title="variable">pfunF0</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#pfunF"><span class="id" title="variable">pfunF</span></a> ⇒ <a class="idref" href="mathcomp.solvable.gfunctor.html#pfunF"><span class="id" title="variable">pfunF</span></a>.<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">fun</span> (<span class="id" title="var">funF</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.map"><span class="id" title="record">map</span></a>) &amp; <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.apply"><span class="id" title="projection">apply</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#funF"><span class="id" title="variable">funF</span></a>) <a class="idref" href="mathcomp.solvable.gfunctor.html#F"><span class="id" title="variable">F</span></a> ⇒<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">fun</span> (<span class="id" title="var">pfunF0</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pmap"><span class="id" title="record">pmap</span></a>) &amp; <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.apply"><span class="id" title="projection">apply</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#pfunF0"><span class="id" title="variable">pfunF0</span></a>) <a class="idref" href="mathcomp.solvable.gfunctor.html#F"><span class="id" title="variable">F</span></a> ⇒<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">fun</span> <span class="id" title="var">Fher</span> (<span class="id" title="var">pfunF</span> := @<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Pmap"><span class="id" title="constructor">Pmap</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#funF"><span class="id" title="variable">funF</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#Fher"><span class="id" title="variable">Fher</span></a>) &amp; <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#pfunF0"><span class="id" title="variable">pfunF0</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#pfunF"><span class="id" title="variable">pfunF</span></a> ⇒ <a class="idref" href="mathcomp.solvable.gfunctor.html#pfunF"><span class="id" title="variable">pfunF</span></a>.<br/>
 
 <br/>
 <span class="id" title="keyword">Definition</span> <a name="GFunctor.clone_mono"><span class="id" title="definition">clone_mono</span></a> (<span class="id" title="var">F</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.object_map"><span class="id" title="definition">object_map</span></a>) :=<br/>
-&nbsp;&nbsp;<span class="id" title="keyword">fun</span> (<span class="id" title="var">funF</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.map"><span class="id" title="record">map</span></a>) &amp; <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.apply"><span class="id" title="projection">apply</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#funF"><span class="id" title="variable">funF</span></a>) <a class="idref" href="mathcomp.solvable.gfunctor.html#F"><span class="id" title="variable">F</span></a> ⇒<br/>
-&nbsp;&nbsp;<span class="id" title="keyword">fun</span> (<span class="id" title="var">mfunF0</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.mono_map"><span class="id" title="record">mono_map</span></a>) &amp; <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.apply"><span class="id" title="projection">apply</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#mfunF0"><span class="id" title="variable">mfunF0</span></a>) <a class="idref" href="mathcomp.solvable.gfunctor.html#F"><span class="id" title="variable">F</span></a> ⇒<br/>
-&nbsp;&nbsp;<span class="id" title="keyword">fun</span> <span class="id" title="var">Fmon</span> (<span class="id" title="var">mfunF</span> := @<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.MonoMap"><span class="id" title="constructor">MonoMap</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#funF"><span class="id" title="variable">funF</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#Fmon"><span class="id" title="variable">Fmon</span></a>) &amp; <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#mfunF0"><span class="id" title="variable">mfunF0</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#mfunF"><span class="id" title="variable">mfunF</span></a> ⇒ <a class="idref" href="mathcomp.solvable.gfunctor.html#mfunF"><span class="id" title="variable">mfunF</span></a>.<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">fun</span> (<span class="id" title="var">funF</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.map"><span class="id" title="record">map</span></a>) &amp; <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.apply"><span class="id" title="projection">apply</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#funF"><span class="id" title="variable">funF</span></a>) <a class="idref" href="mathcomp.solvable.gfunctor.html#F"><span class="id" title="variable">F</span></a> ⇒<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">fun</span> (<span class="id" title="var">mfunF0</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.mono_map"><span class="id" title="record">mono_map</span></a>) &amp; <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.apply"><span class="id" title="projection">apply</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#mfunF0"><span class="id" title="variable">mfunF0</span></a>) <a class="idref" href="mathcomp.solvable.gfunctor.html#F"><span class="id" title="variable">F</span></a> ⇒<br/>
+&nbsp;&nbsp;<span class="id" title="keyword">fun</span> <span class="id" title="var">Fmon</span> (<span class="id" title="var">mfunF</span> := @<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.MonoMap"><span class="id" title="constructor">MonoMap</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#funF"><span class="id" title="variable">funF</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#Fmon"><span class="id" title="variable">Fmon</span></a>) &amp; <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#phant_id"><span class="id" title="definition">phant_id</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#mfunF0"><span class="id" title="variable">mfunF0</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#mfunF"><span class="id" title="variable">mfunF</span></a> ⇒ <a class="idref" href="mathcomp.solvable.gfunctor.html#mfunF"><span class="id" title="variable">mfunF</span></a>.<br/>
 
 <br/>
 <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.ClassDefinitions"><span class="id" title="section">ClassDefinitions</span></a>.<br/>
@@ -294,41 +293,41 @@
 <span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pcontinuous_is_hereditary"><span class="id" title="lemma">pcontinuous_is_hereditary</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pcontinuous_is_hereditary"><span class="id" title="lemma">:</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pcontinuous_is_hereditary"><span class="id" title="lemma">pcontinuous</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pcontinuous_is_hereditary"><span class="id" title="lemma">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pcontinuous_is_hereditary"><span class="id" title="lemma">hereditary</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Notation</span> <a name="a1ae11930941a680f6750f6723874923"><span class="id" title="notation">&quot;</span></a>[ 'igFun' 'by' Fsub &amp; Fcont ]" :=<br/>
+<span class="id" title="keyword">Notation</span> <a name="c0205c751a17b7793ccdaf02cc4999e3"><span class="id" title="notation">&quot;</span></a>[ 'igFun' 'by' Fsub &amp; Fcont ]" :=<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;(<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pack_iso"><span class="id" title="definition">pack_iso</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.continuous_is_iso_continuous"><span class="id" title="lemma">continuous_is_iso_continuous</span></a> <span class="id" title="var">Fcont</span>) (<span class="id" title="keyword">fun</span> <span class="id" title="var">gT</span> <span class="id" title="var">G</span> ⇒ <a class="idref" href="mathcomp.fingroup.fingroup.html#groupP"><span class="id" title="lemma">groupP</span></a> <span class="id" title="var">_</span>) <span class="id" title="var">Fsub</span>)<br/>
 &nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'igFun'  'by'  Fsub  &amp;  Fcont ]") : <span class="id" title="var">form_scope</span>.<br/>
 
 <br/>
-<span class="id" title="keyword">Notation</span> <a name="6a21e731147765f65bc5f2e922126efc"><span class="id" title="notation">&quot;</span></a>[ 'igFun' 'by' Fsub &amp; ! Fcont ]" :=<br/>
+<span class="id" title="keyword">Notation</span> <a name="8dd9a311237b4fd5bc515a2cbf48517e"><span class="id" title="notation">&quot;</span></a>[ 'igFun' 'by' Fsub &amp; ! Fcont ]" :=<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;(<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pack_iso"><span class="id" title="definition">pack_iso</span></a> <span class="id" title="var">Fcont</span> (<span class="id" title="keyword">fun</span> <span class="id" title="var">gT</span> <span class="id" title="var">G</span> ⇒ <a class="idref" href="mathcomp.fingroup.fingroup.html#groupP"><span class="id" title="lemma">groupP</span></a> <span class="id" title="var">_</span>) <span class="id" title="var">Fsub</span>)<br/>
 &nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'igFun'  'by'  Fsub  &amp;  ! Fcont ]") : <span class="id" title="var">form_scope</span>.<br/>
 
 <br/>
-<span class="id" title="keyword">Notation</span> <a name="0d3cf0514afe70d7a29245834117002f"><span class="id" title="notation">&quot;</span></a>[ 'igFun' 'of' F ]" := (@<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.clone_iso"><span class="id" title="definition">clone_iso</span></a> <span class="id" title="var">F</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a>)<br/>
+<span class="id" title="keyword">Notation</span> <a name="0a3c3d64903581df0193a363279f22cc"><span class="id" title="notation">&quot;</span></a>[ 'igFun' 'of' F ]" := (@<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.clone_iso"><span class="id" title="definition">clone_iso</span></a> <span class="id" title="var">F</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a>)<br/>
 &nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'igFun'  'of'  F ]") : <span class="id" title="var">form_scope</span>.<br/>
 
 <br/>
-<span class="id" title="keyword">Notation</span> <a name="f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">&quot;</span></a>[ 'gFun' 'by' Fcont ]" := (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Map"><span class="id" title="constructor">Map</span></a> <span class="id" title="var">Fcont</span>)<br/>
+<span class="id" title="keyword">Notation</span> <a name="cecbde1597e0d77a491e8c4f94033af4"><span class="id" title="notation">&quot;</span></a>[ 'gFun' 'by' Fcont ]" := (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Map"><span class="id" title="constructor">Map</span></a> <span class="id" title="var">Fcont</span>)<br/>
 &nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'gFun'  'by'  Fcont ]") : <span class="id" title="var">form_scope</span>.<br/>
 
 <br/>
-<span class="id" title="keyword">Notation</span> <a name="607d805a80d936daf34262a28a285db3"><span class="id" title="notation">&quot;</span></a>[ 'gFun' 'of' F ]" := (@<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.clone"><span class="id" title="definition">clone</span></a> <span class="id" title="var">F</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a>)<br/>
+<span class="id" title="keyword">Notation</span> <a name="b978f29f27d17b625bd1a96535c57314"><span class="id" title="notation">&quot;</span></a>[ 'gFun' 'of' F ]" := (@<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.clone"><span class="id" title="definition">clone</span></a> <span class="id" title="var">F</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</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#id"><span class="id" title="abbreviation">id</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#id"><span class="id" title="abbreviation">id</span></a>)<br/>
 &nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'gFun'  'of'  F ]") : <span class="id" title="var">form_scope</span>.<br/>
 
 <br/>
-<span class="id" title="keyword">Notation</span> <a name="75f5bf98333ce9930f3fc4415f01e6a0"><span class="id" title="notation">&quot;</span></a>[ 'pgFun' 'by' Fher ]" := (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Pmap"><span class="id" title="constructor">Pmap</span></a> <span class="id" title="var">Fher</span>)<br/>
+<span class="id" title="keyword">Notation</span> <a name="f4a0ec7c18bd128b271d4428328fd43b"><span class="id" title="notation">&quot;</span></a>[ 'pgFun' 'by' Fher ]" := (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Pmap"><span class="id" title="constructor">Pmap</span></a> <span class="id" title="var">Fher</span>)<br/>
 &nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'pgFun'  'by'  Fher ]") : <span class="id" title="var">form_scope</span>.<br/>
 
 <br/>
-<span class="id" title="keyword">Notation</span> <a name="ee155ab488843b0ecc37c27fc7341f64"><span class="id" title="notation">&quot;</span></a>[ 'pgFun' 'of' F ]" := (@<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.clone_pmap"><span class="id" title="definition">clone_pmap</span></a> <span class="id" title="var">F</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a>)<br/>
+<span class="id" title="keyword">Notation</span> <a name="09ca9041b424fb3a198e2a775c1edfdd"><span class="id" title="notation">&quot;</span></a>[ 'pgFun' 'of' F ]" := (@<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.clone_pmap"><span class="id" title="definition">clone_pmap</span></a> <span class="id" title="var">F</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</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#id"><span class="id" title="abbreviation">id</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#id"><span class="id" title="abbreviation">id</span></a>)<br/>
 &nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'pgFun' 'of'  F ]") : <span class="id" title="var">form_scope</span>.<br/>
 
 <br/>
-<span class="id" title="keyword">Notation</span> <a name="34d675edff20d6d91e43f305650662d9"><span class="id" title="notation">&quot;</span></a>[ 'mgFun' 'by' Fmon ]" := (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.MonoMap"><span class="id" title="constructor">MonoMap</span></a> <span class="id" title="var">Fmon</span>)<br/>
+<span class="id" title="keyword">Notation</span> <a name="f3da3221c5171e732a65fec8cc2ba4fa"><span class="id" title="notation">&quot;</span></a>[ 'mgFun' 'by' Fmon ]" := (<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.MonoMap"><span class="id" title="constructor">MonoMap</span></a> <span class="id" title="var">Fmon</span>)<br/>
 &nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'mgFun'  'by'  Fmon ]") : <span class="id" title="var">form_scope</span>.<br/>
 
 <br/>
-<span class="id" title="keyword">Notation</span> <a name="617ba6355e0c6813ccd42cf7ac127f20"><span class="id" title="notation">&quot;</span></a>[ 'mgFun' 'of' F ]" := (@<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.clone_mono"><span class="id" title="definition">clone_mono</span></a> <span class="id" title="var">F</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</span></a>)<br/>
+<span class="id" title="keyword">Notation</span> <a name="703ce4e21f8af3122d8da8159ae55c98"><span class="id" title="notation">&quot;</span></a>[ 'mgFun' 'of' F ]" := (@<a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.clone_mono"><span class="id" title="definition">clone_mono</span></a> <span class="id" title="var">F</span> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#id"><span class="id" title="abbreviation">id</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#id"><span class="id" title="abbreviation">id</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#id"><span class="id" title="abbreviation">id</span></a>)<br/>
 &nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'mgFun' 'of'  F ]") : <span class="id" title="var">form_scope</span>.<br/>
 
 <br/>
@@ -341,14 +340,14 @@
 <br/>
 
 <br/>
-<span class="id" title="keyword">Notation</span> <a name="5feaca9261529b1a79b9f50bc9e0bd05"><span class="id" title="notation">&quot;</span></a>F1 \o F2" := (<a class="idref" href="mathcomp.solvable.gfunctor.html#comp_head"><span class="id" title="definition">GFunctor.comp_head</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#tt"><span class="id" title="constructor">tt</span></a> <span class="id" title="var">F1</span> <span class="id" title="var">F2</span>) : <span class="id" title="var">gFun_scope</span>.<br/>
-<span class="id" title="keyword">Notation</span> <a name="397612d5557f5f74747d26baf6517ab7"><span class="id" title="notation">&quot;</span></a>F1 %% F2" := (<a class="idref" href="mathcomp.solvable.gfunctor.html#modulo"><span class="id" title="definition">GFunctor.modulo</span></a> <span class="id" title="var">F1</span> <span class="id" title="var">F2</span>) : <span class="id" title="var">gFun_scope</span>.<br/>
+<span class="id" title="keyword">Notation</span> <a name="dca792ff4a91f336726016c880ff4199"><span class="id" title="notation">&quot;</span></a>F1 \o F2" := (<a class="idref" href="mathcomp.solvable.gfunctor.html#comp_head"><span class="id" title="definition">GFunctor.comp_head</span></a> <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="var">F1</span> <span class="id" title="var">F2</span>) : <span class="id" title="var">gFun_scope</span>.<br/>
+<span class="id" title="keyword">Notation</span> <a name="961a0e2d620e204ca234a2667f1e9a3c"><span class="id" title="notation">&quot;</span></a>F1 %% F2" := (<a class="idref" href="mathcomp.solvable.gfunctor.html#modulo"><span class="id" title="definition">GFunctor.modulo</span></a> <span class="id" title="var">F1</span> <span class="id" title="var">F2</span>) : <span class="id" title="var">gFun_scope</span>.<br/>
 
 <br/>
 <span class="id" title="keyword">Section</span> <a name="FunctorGroup"><span class="id" title="section">FunctorGroup</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Variables</span> (<a name="FunctorGroup.F"><span class="id" title="variable">F</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#iso_map"><span class="id" title="record">GFunctor.iso_map</span></a>) (<a name="FunctorGroup.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="FunctorGroup.G"><span class="id" title="variable">G</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>).<br/>
+<span class="id" title="keyword">Variables</span> (<a name="FunctorGroup.F"><span class="id" title="variable">F</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#iso_map"><span class="id" title="record">GFunctor.iso_map</span></a>) (<a name="FunctorGroup.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="FunctorGroup.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.gfunctor.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/>
 <span class="id" title="keyword">Lemma</span> <a name="gFgroupset"><span class="id" title="lemma">gFgroupset</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.gfunctor.html#FunctorGroup.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#FunctorGroup.gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#FunctorGroup.G"><span class="id" title="variable">G</span></a>).  <br/>
 <span class="id" title="keyword">Canonical</span> <span class="id" title="var">gFgroup</span> := <a class="idref" href="mathcomp.fingroup.fingroup.html#Group"><span class="id" title="constructor">Group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gFgroupset"><span class="id" title="lemma">gFgroupset</span></a>.<br/>
 
@@ -358,8 +357,8 @@
 <br/>
 <span class="id" title="keyword">Canonical</span> <span class="id" title="var">gFmod_group</span><br/>
 &nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" title="var">F1</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#iso_map"><span class="id" title="record">GFunctor.iso_map</span></a>) (<span class="id" title="var">F2</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#object_map"><span class="id" title="definition">GFunctor.object_map</span></a>)<br/>
-&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" title="var">gT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) :=<br/>
-&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.fingroup.html#ccb763a84253e971fd106aeeb9cd3cb0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ccb763a84253e971fd106aeeb9cd3cb0"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#ccb763a84253e971fd106aeeb9cd3cb0"><span class="id" title="notation">of</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#F1"><span class="id" title="variable">F1</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#397612d5557f5f74747d26baf6517ab7"><span class="id" title="notation">%%</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#F2"><span class="id" title="variable">F2</span></a>)%<span class="id" title="var">gF</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ccb763a84253e971fd106aeeb9cd3cb0"><span class="id" title="notation">]</span></a>.<br/>
+&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" title="var">gT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<span class="id" title="var">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.gfunctor.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/>
+&nbsp;&nbsp;<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.gfunctor.html#F1"><span class="id" title="variable">F1</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#961a0e2d620e204ca234a2667f1e9a3c"><span class="id" title="notation">%%</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#F2"><span class="id" title="variable">F2</span></a>)%<span class="id" title="var">gF</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.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">Section</span> <a name="IsoFunctorTheory"><span class="id" title="section">IsoFunctorTheory</span></a>.<br/>
@@ -369,55 +368,55 @@
 <span class="id" title="keyword">Variable</span> <a name="IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#iso_map"><span class="id" title="record">GFunctor.iso_map</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="gFsub"><span class="id" title="lemma">gFsub</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) : <a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="gFsub"><span class="id" title="lemma">gFsub</span></a> <span class="id" title="var">gT</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.gfunctor.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>) : <a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.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.gfunctor.html#G"><span class="id" title="variable">G</span></a>.<br/>
  
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="gFsub_trans"><span class="id" title="lemma">gFsub_trans</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">A</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred_class"><span class="id" title="abbreviation">pred_class</span></a>) :<br/>
-&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#A"><span class="id" title="variable">A</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="gFsub_trans"><span class="id" title="lemma">gFsub_trans</span></a> <span class="id" title="var">gT</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.gfunctor.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>) (<span class="id" title="var">A</span> : <a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">pred</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">}</span></a>) :<br/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.gfunctor.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.gfunctor.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#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.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.gfunctor.html#A"><span class="id" title="variable">A</span></a>.<br/>
  
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="gF1"><span class="id" title="lemma">gF1</span></a> <span class="id" title="var">gT</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 1.  <br/>
+<span class="id" title="keyword">Lemma</span> <a name="gF1"><span class="id" title="lemma">gF1</span></a> <span class="id" title="var">gT</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> 1 <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> 1.  <br/>
 
 <br/>
 <span class="id" title="keyword">Lemma</span> <a name="gFiso_cont"><span class="id" title="lemma">gFiso_cont</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#iso_continuous"><span class="id" title="definition">GFunctor.iso_continuous</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a>.<br/>
  
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="gFchar"><span class="id" title="lemma">gFchar</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) : <a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#004858100bfba9714bde1cdbce60358b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#004858100bfba9714bde1cdbce60358b"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="gFchar"><span class="id" title="lemma">gFchar</span></a> <span class="id" title="var">gT</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.gfunctor.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>) : <a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</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.gfunctor.html#G"><span class="id" title="variable">G</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="gFnorm"><span class="id" title="lemma">gFnorm</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) : <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">)</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="gFnorm"><span class="id" title="lemma">gFnorm</span></a> <span class="id" title="var">gT</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.gfunctor.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>) : <a class="idref" href="mathcomp.solvable.gfunctor.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.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.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</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="gFnorms"><span class="id" title="lemma">gFnorms</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) : <a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">)</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="gFnorms"><span class="id" title="lemma">gFnorms</span></a> <span class="id" title="var">gT</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.gfunctor.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>) : <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.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><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.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</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="gFnormal"><span class="id" title="lemma">gFnormal</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) : <a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#c27c638e534bbb5b7de2d4b4aa0a3e82"><span class="id" title="notation">&lt;|</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="gFnormal"><span class="id" title="lemma">gFnormal</span></a> <span class="id" title="var">gT</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.gfunctor.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>) : <a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7e8095b432e7aa5c3c22bb87584658b7"><span class="id" title="notation">&lt;|</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>.<br/>
  
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="gFchar_trans"><span class="id" title="lemma">gFchar_trans</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) : <a class="idref" href="mathcomp.solvable.gfunctor.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#004858100bfba9714bde1cdbce60358b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#004858100bfba9714bde1cdbce60358b"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#004858100bfba9714bde1cdbce60358b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#004858100bfba9714bde1cdbce60358b"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="gFchar_trans"><span class="id" title="lemma">gFchar_trans</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> <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.gfunctor.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>) : <a class="idref" href="mathcomp.solvable.gfunctor.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.gfunctor.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.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.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.gfunctor.html#G"><span class="id" title="variable">G</span></a>.<br/>
  
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="gFnormal_trans"><span class="id" title="lemma">gFnormal_trans</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) : <a class="idref" href="mathcomp.solvable.gfunctor.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#c27c638e534bbb5b7de2d4b4aa0a3e82"><span class="id" title="notation">&lt;|</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#c27c638e534bbb5b7de2d4b4aa0a3e82"><span class="id" title="notation">&lt;|</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="gFnormal_trans"><span class="id" title="lemma">gFnormal_trans</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> <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.gfunctor.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>) : <a class="idref" href="mathcomp.solvable.gfunctor.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7e8095b432e7aa5c3c22bb87584658b7"><span class="id" title="notation">&lt;|</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.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.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7e8095b432e7aa5c3c22bb87584658b7"><span class="id" title="notation">&lt;|</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>.<br/>
  
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="gFnorm_trans"><span class="id" title="lemma">gFnorm_trans</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">A</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred_class"><span class="id" title="abbreviation">pred_class</span></a>) (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) :<br/>
-&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.gfunctor.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">)</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="gFnorm_trans"><span class="id" title="lemma">gFnorm_trans</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">A</span> : <a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">pred</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.ssrbool.html#64f8873130736b599801d4930af00e74"><span class="id" title="notation">}</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.gfunctor.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/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.gfunctor.html#A"><span class="id" title="variable">A</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.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><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.gfunctor.html#A"><span class="id" title="variable">A</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.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</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="injmF_sub"><span class="id" title="lemma">injmF_sub</span></a> <span class="id" title="var">gT</span> <span class="id" title="var">rT</span> (<span class="id" title="var">G</span> <span class="id" title="var">D</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">}</span></a>) :<br/>
-&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.morphism.html#14bfb149f00fa839cfb11397f4fe629f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#14bfb149f00fa839cfb11397f4fe629f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#rT"><span class="id" title="variable">rT</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>).<br/>
+<span class="id" title="keyword">Lemma</span> <a name="injmF_sub"><span class="id" title="lemma">injmF_sub</span></a> <span class="id" title="var">gT</span> <span class="id" title="var">rT</span> (<span class="id" title="var">G</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.gfunctor.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>) (<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.gfunctor.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.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/>
+&nbsp;&nbsp;<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.gfunctor.html#f"><span class="id" title="variable">f</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.gfunctor.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.gfunctor.html#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.gfunctor.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.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><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.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#rT"><span class="id" title="variable">rT</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.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.gfunctor.html#G"><span class="id" title="variable">G</span></a>).<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="injmF"><span class="id" title="lemma">injmF</span></a> <span class="id" title="var">gT</span> <span class="id" title="var">rT</span> (<span class="id" title="var">G</span> <span class="id" title="var">D</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">}</span></a>) :<br/>
-&nbsp;&nbsp;<a class="idref" href="mathcomp.fingroup.morphism.html#14bfb149f00fa839cfb11397f4fe629f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#14bfb149f00fa839cfb11397f4fe629f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#rT"><span class="id" title="variable">rT</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>).<br/>
+<span class="id" title="keyword">Lemma</span> <a name="injmF"><span class="id" title="lemma">injmF</span></a> <span class="id" title="var">gT</span> <span class="id" title="var">rT</span> (<span class="id" title="var">G</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.gfunctor.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>) (<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.gfunctor.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.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/>
+&nbsp;&nbsp;<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.gfunctor.html#f"><span class="id" title="variable">f</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.gfunctor.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.gfunctor.html#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.gfunctor.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.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</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.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#rT"><span class="id" title="variable">rT</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.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.gfunctor.html#G"><span class="id" title="variable">G</span></a>).<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="gFisom"><span class="id" title="lemma">gFisom</span></a> <span class="id" title="var">gT</span> <span class="id" title="var">rT</span> (<span class="id" title="var">G</span> <span class="id" title="var">D</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) <span class="id" title="var">R</span> (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">}</span></a>) :<br/>
-&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#isom"><span class="id" title="definition">isom</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> (<a class="idref" href="mathcomp.fingroup.fingroup.html#gval"><span class="id" title="projection">gval</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#R"><span class="id" title="variable">R</span></a>) <a class="idref" href="mathcomp.solvable.gfunctor.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#isom"><span class="id" title="definition">isom</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>) (<a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#rT"><span class="id" title="variable">rT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#R"><span class="id" title="variable">R</span></a>) <a class="idref" href="mathcomp.solvable.gfunctor.html#f"><span class="id" title="variable">f</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="gFisom"><span class="id" title="lemma">gFisom</span></a> <span class="id" title="var">gT</span> <span class="id" title="var">rT</span> (<span class="id" title="var">G</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.gfunctor.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>) <span class="id" title="var">R</span> (<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.gfunctor.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.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/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.gfunctor.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.gfunctor.html#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.fingroup.morphism.html#isom"><span class="id" title="definition">isom</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> (<a class="idref" href="mathcomp.fingroup.fingroup.html#gval"><span class="id" title="projection">gval</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#R"><span class="id" title="variable">R</span></a>) <a class="idref" href="mathcomp.solvable.gfunctor.html#f"><span class="id" title="variable">f</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.morphism.html#isom"><span class="id" title="definition">isom</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>) (<a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#rT"><span class="id" title="variable">rT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#R"><span class="id" title="variable">R</span></a>) <a class="idref" href="mathcomp.solvable.gfunctor.html#f"><span class="id" title="variable">f</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="gFisog"><span class="id" title="lemma">gFisog</span></a> <span class="id" title="var">gT</span> <span class="id" title="var">rT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">R</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) :<br/>
-&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#R"><span class="id" title="variable">R</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#rT"><span class="id" title="variable">rT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#R"><span class="id" title="variable">R</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="gFisog"><span class="id" title="lemma">gFisog</span></a> <span class="id" title="var">gT</span> <span class="id" title="var">rT</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.gfunctor.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>) (<span class="id" title="var">R</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.gfunctor.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/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.gfunctor.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.gfunctor.html#R"><span class="id" title="variable">R</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.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.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.gfunctor.html#IsoFunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#rT"><span class="id" title="variable">rT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#R"><span class="id" title="variable">R</span></a>.<br/>
  
 <br/>
 <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#IsoFunctorTheory"><span class="id" title="section">IsoFunctorTheory</span></a>.<br/>
@@ -433,8 +432,8 @@
 <span class="id" title="keyword">Lemma</span> <a name="gFcont"><span class="id" title="lemma">gFcont</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#continuous"><span class="id" title="definition">GFunctor.continuous</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#FunctorTheory.F"><span class="id" title="variable">F</span></a>.<br/>
  
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="morphimF"><span class="id" title="lemma">morphimF</span></a> <span class="id" title="var">gT</span> <span class="id" title="var">rT</span> (<span class="id" title="var">G</span> <span class="id" title="var">D</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">}</span></a>) :<br/>
-&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#FunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#FunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#rT"><span class="id" title="variable">rT</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>).<br/>
+<span class="id" title="keyword">Lemma</span> <a name="morphimF"><span class="id" title="lemma">morphimF</span></a> <span class="id" title="var">gT</span> <span class="id" title="var">rT</span> (<span class="id" title="var">G</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.gfunctor.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>) (<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.gfunctor.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">&gt;-&gt;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.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/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.gfunctor.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.gfunctor.html#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.gfunctor.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.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#FunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><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.gfunctor.html#FunctorTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#rT"><span class="id" title="variable">rT</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.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.gfunctor.html#G"><span class="id" title="variable">G</span></a>).<br/>
 
 <br/>
 <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#FunctorTheory"><span class="id" title="section">FunctorTheory</span></a>.<br/>
@@ -455,14 +454,14 @@
 <span class="id" title="keyword">Lemma</span> <a name="gFhereditary"><span class="id" title="lemma">gFhereditary</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#hereditary"><span class="id" title="definition">GFunctor.hereditary</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.BasicTheory.F"><span class="id" title="variable">F</span></a>.<br/>
  
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="gFunctorI"><span class="id" title="lemma">gFunctorI</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) :<br/>
-&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.BasicTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#cb41714a5a23482f7a48a98975fa8c59"><span class="id" title="notation">:&amp;:</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.BasicTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#cb41714a5a23482f7a48a98975fa8c59"><span class="id" title="notation">:&amp;:</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.BasicTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#cb41714a5a23482f7a48a98975fa8c59"><span class="id" title="notation">:&amp;:</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#H"><span class="id" title="variable">H</span></a>).<br/>
+<span class="id" title="keyword">Lemma</span> <a name="gFunctorI"><span class="id" title="lemma">gFunctorI</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> <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.gfunctor.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/>
+&nbsp;&nbsp;<a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.BasicTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#b9596739b058766532fc6517a36fef9f"><span class="id" title="notation">:&amp;:</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.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#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.BasicTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#b9596739b058766532fc6517a36fef9f"><span class="id" title="notation">:&amp;:</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.BasicTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#b9596739b058766532fc6517a36fef9f"><span class="id" title="notation">:&amp;:</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#H"><span class="id" title="variable">H</span></a>).<br/>
 
 <br/>
 <span class="id" title="keyword">Lemma</span> <a name="pmorphimF"><span class="id" title="lemma">pmorphimF</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#pcontinuous"><span class="id" title="definition">GFunctor.pcontinuous</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.BasicTheory.F"><span class="id" title="variable">F</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="gFid"><span class="id" title="lemma">gFid</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) : <a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.BasicTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.BasicTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>)  <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.BasicTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>.<br/>
+<span class="id" title="keyword">Lemma</span> <a name="gFid"><span class="id" title="lemma">gFid</span></a> <span class="id" title="var">gT</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.gfunctor.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>) : <a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.BasicTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.BasicTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.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#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.BasicTheory.F"><span class="id" title="variable">F</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#G"><span class="id" title="variable">G</span></a>.<br/>
 
 <br/>
 <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.BasicTheory"><span class="id" title="section">BasicTheory</span></a>.<br/>
@@ -474,14 +473,14 @@
 <span class="id" title="keyword">Variables</span> (<a name="PartialFunctorTheory.Modulo.F1"><span class="id" title="variable">F1</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#pmap"><span class="id" title="record">GFunctor.pmap</span></a>) (<a name="PartialFunctorTheory.Modulo.F2"><span class="id" title="variable">F2</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#map"><span class="id" title="record">GFunctor.map</span></a>).<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="gFmod_closed"><span class="id" title="lemma">gFmod_closed</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#closed"><span class="id" title="definition">GFunctor.closed</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.Modulo.F1"><span class="id" title="variable">F1</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#397612d5557f5f74747d26baf6517ab7"><span class="id" title="notation">%%</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.Modulo.F2"><span class="id" title="variable">F2</span></a>).<br/>
+<span class="id" title="keyword">Lemma</span> <a name="gFmod_closed"><span class="id" title="lemma">gFmod_closed</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#closed"><span class="id" title="definition">GFunctor.closed</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.Modulo.F1"><span class="id" title="variable">F1</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#961a0e2d620e204ca234a2667f1e9a3c"><span class="id" title="notation">%%</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.Modulo.F2"><span class="id" title="variable">F2</span></a>).<br/>
  
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="gFmod_cont"><span class="id" title="lemma">gFmod_cont</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#continuous"><span class="id" title="definition">GFunctor.continuous</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.Modulo.F1"><span class="id" title="variable">F1</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#397612d5557f5f74747d26baf6517ab7"><span class="id" title="notation">%%</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.Modulo.F2"><span class="id" title="variable">F2</span></a>).<br/>
+<span class="id" title="keyword">Lemma</span> <a name="gFmod_cont"><span class="id" title="lemma">gFmod_cont</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#continuous"><span class="id" title="definition">GFunctor.continuous</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.Modulo.F1"><span class="id" title="variable">F1</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#961a0e2d620e204ca234a2667f1e9a3c"><span class="id" title="notation">%%</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.Modulo.F2"><span class="id" title="variable">F2</span></a>).<br/>
 
 <br/>
-<span class="id" title="keyword">Canonical</span> <span class="id" title="var">gFmod_igFun</span> := <a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">igFun</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gFmod_closed"><span class="id" title="lemma">gFmod_closed</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gFmod_cont"><span class="id" title="lemma">gFmod_cont</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">]</span></a>.<br/>
-<span class="id" title="keyword">Canonical</span> <span class="id" title="var">gFmod_gFun</span> := <a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">gFun</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gFmod_cont"><span class="id" title="lemma">gFmod_cont</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">gFmod_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> <a class="idref" href="mathcomp.solvable.gfunctor.html#gFmod_closed"><span class="id" title="lemma">gFmod_closed</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#c0205c751a17b7793ccdaf02cc4999e3"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gFmod_cont"><span class="id" title="lemma">gFmod_cont</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">gFmod_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.gfunctor.html#gFmod_cont"><span class="id" title="lemma">gFmod_cont</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#cecbde1597e0d77a491e8c4f94033af4"><span class="id" title="notation">]</span></a>.<br/>
 
 <br/>
 <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.Modulo"><span class="id" title="section">Modulo</span></a>.<br/>
@@ -490,10 +489,10 @@
 <span class="id" title="keyword">Variables</span> <a name="PartialFunctorTheory.F1"><span class="id" title="variable">F1</span></a> <a name="PartialFunctorTheory.F2"><span class="id" title="variable">F2</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#pmap"><span class="id" title="record">GFunctor.pmap</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="gFmod_hereditary"><span class="id" title="lemma">gFmod_hereditary</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#hereditary"><span class="id" title="definition">GFunctor.hereditary</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.F1"><span class="id" title="variable">F1</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#397612d5557f5f74747d26baf6517ab7"><span class="id" title="notation">%%</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.F2"><span class="id" title="variable">F2</span></a>).<br/>
+<span class="id" title="keyword">Lemma</span> <a name="gFmod_hereditary"><span class="id" title="lemma">gFmod_hereditary</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#hereditary"><span class="id" title="definition">GFunctor.hereditary</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.F1"><span class="id" title="variable">F1</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#961a0e2d620e204ca234a2667f1e9a3c"><span class="id" title="notation">%%</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory.F2"><span class="id" title="variable">F2</span></a>).<br/>
 
 <br/>
-<span class="id" title="keyword">Canonical</span> <span class="id" title="var">gFmod_pgFun</span> := <a class="idref" href="mathcomp.solvable.gfunctor.html#75f5bf98333ce9930f3fc4415f01e6a0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#75f5bf98333ce9930f3fc4415f01e6a0"><span class="id" title="notation">pgFun</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#75f5bf98333ce9930f3fc4415f01e6a0"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gFmod_hereditary"><span class="id" title="lemma">gFmod_hereditary</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#75f5bf98333ce9930f3fc4415f01e6a0"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">gFmod_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.gfunctor.html#gFmod_hereditary"><span class="id" title="lemma">gFmod_hereditary</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">End</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#PartialFunctorTheory"><span class="id" title="section">PartialFunctorTheory</span></a>.<br/>
@@ -514,14 +513,14 @@
 <span class="id" title="keyword">Variables</span> (<a name="MonotonicFunctorTheory.Composition.F1"><span class="id" title="variable">F1</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#mono_map"><span class="id" title="record">GFunctor.mono_map</span></a>) (<a name="MonotonicFunctorTheory.Composition.F2"><span class="id" title="variable">F2</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#map"><span class="id" title="record">GFunctor.map</span></a>).<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="gFcomp_closed"><span class="id" title="lemma">gFcomp_closed</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#closed"><span class="id" title="definition">GFunctor.closed</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#MonotonicFunctorTheory.Composition.F1"><span class="id" title="variable">F1</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#5feaca9261529b1a79b9f50bc9e0bd05"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#5feaca9261529b1a79b9f50bc9e0bd05"><span class="id" title="notation">o</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#MonotonicFunctorTheory.Composition.F2"><span class="id" title="variable">F2</span></a>).<br/>
+<span class="id" title="keyword">Lemma</span> <a name="gFcomp_closed"><span class="id" title="lemma">gFcomp_closed</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#closed"><span class="id" title="definition">GFunctor.closed</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#MonotonicFunctorTheory.Composition.F1"><span class="id" title="variable">F1</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#dca792ff4a91f336726016c880ff4199"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#dca792ff4a91f336726016c880ff4199"><span class="id" title="notation">o</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#MonotonicFunctorTheory.Composition.F2"><span class="id" title="variable">F2</span></a>).<br/>
  
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="gFcomp_cont"><span class="id" title="lemma">gFcomp_cont</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#continuous"><span class="id" title="definition">GFunctor.continuous</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#MonotonicFunctorTheory.Composition.F1"><span class="id" title="variable">F1</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#5feaca9261529b1a79b9f50bc9e0bd05"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#5feaca9261529b1a79b9f50bc9e0bd05"><span class="id" title="notation">o</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#MonotonicFunctorTheory.Composition.F2"><span class="id" title="variable">F2</span></a>).<br/>
+<span class="id" title="keyword">Lemma</span> <a name="gFcomp_cont"><span class="id" title="lemma">gFcomp_cont</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#continuous"><span class="id" title="definition">GFunctor.continuous</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#MonotonicFunctorTheory.Composition.F1"><span class="id" title="variable">F1</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#dca792ff4a91f336726016c880ff4199"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#dca792ff4a91f336726016c880ff4199"><span class="id" title="notation">o</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#MonotonicFunctorTheory.Composition.F2"><span class="id" title="variable">F2</span></a>).<br/>
 
 <br/>
-<span class="id" title="keyword">Canonical</span> <span class="id" title="var">gFcomp_igFun</span> := <a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">igFun</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gFcomp_closed"><span class="id" title="lemma">gFcomp_closed</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gFcomp_cont"><span class="id" title="lemma">gFcomp_cont</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">]</span></a>.<br/>
-<span class="id" title="keyword">Canonical</span> <span class="id" title="var">gFcomp_gFun</span> :=<a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">gFun</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gFcomp_cont"><span class="id" title="lemma">gFcomp_cont</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">gFcomp_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> <a class="idref" href="mathcomp.solvable.gfunctor.html#gFcomp_closed"><span class="id" title="lemma">gFcomp_closed</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#c0205c751a17b7793ccdaf02cc4999e3"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gFcomp_cont"><span class="id" title="lemma">gFcomp_cont</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">gFcomp_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.gfunctor.html#gFcomp_cont"><span class="id" title="lemma">gFcomp_cont</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#cecbde1597e0d77a491e8c4f94033af4"><span class="id" title="notation">]</span></a>.<br/>
 
 <br/>
 <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#MonotonicFunctorTheory.Composition"><span class="id" title="section">Composition</span></a>.<br/>
@@ -530,10 +529,10 @@
 <span class="id" title="keyword">Variables</span> <a name="MonotonicFunctorTheory.F1"><span class="id" title="variable">F1</span></a> <a name="MonotonicFunctorTheory.F2"><span class="id" title="variable">F2</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#mono_map"><span class="id" title="record">GFunctor.mono_map</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Lemma</span> <a name="gFcompS"><span class="id" title="lemma">gFcompS</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#monotonic"><span class="id" title="definition">GFunctor.monotonic</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#MonotonicFunctorTheory.F1"><span class="id" title="variable">F1</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#5feaca9261529b1a79b9f50bc9e0bd05"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#5feaca9261529b1a79b9f50bc9e0bd05"><span class="id" title="notation">o</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#MonotonicFunctorTheory.F2"><span class="id" title="variable">F2</span></a>).<br/>
+<span class="id" title="keyword">Lemma</span> <a name="gFcompS"><span class="id" title="lemma">gFcompS</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#monotonic"><span class="id" title="definition">GFunctor.monotonic</span></a> (<a class="idref" href="mathcomp.solvable.gfunctor.html#MonotonicFunctorTheory.F1"><span class="id" title="variable">F1</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#dca792ff4a91f336726016c880ff4199"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#dca792ff4a91f336726016c880ff4199"><span class="id" title="notation">o</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#MonotonicFunctorTheory.F2"><span class="id" title="variable">F2</span></a>).<br/>
  
 <br/>
-<span class="id" title="keyword">Canonical</span> <span class="id" title="var">gFcomp_mgFun</span> := <a class="idref" href="mathcomp.solvable.gfunctor.html#34d675edff20d6d91e43f305650662d9"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#34d675edff20d6d91e43f305650662d9"><span class="id" title="notation">mgFun</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#34d675edff20d6d91e43f305650662d9"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gFcompS"><span class="id" title="lemma">gFcompS</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#34d675edff20d6d91e43f305650662d9"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">gFcomp_mgFun</span> := <a class="idref" href="mathcomp.solvable.gfunctor.html#f3da3221c5171e732a65fec8cc2ba4fa"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#f3da3221c5171e732a65fec8cc2ba4fa"><span class="id" title="notation">mgFun</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#f3da3221c5171e732a65fec8cc2ba4fa"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gFcompS"><span class="id" title="lemma">gFcompS</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#f3da3221c5171e732a65fec8cc2ba4fa"><span class="id" title="notation">]</span></a>.<br/>
 
 <br/>
 <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#MonotonicFunctorTheory"><span class="id" title="section">MonotonicFunctorTheory</span></a>.<br/>
@@ -545,7 +544,7 @@
 <span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">gT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Definition</span> <a name="idGfun"><span class="id" title="definition">idGfun</span></a> <span class="id" title="var">gT</span> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#18cd0ece1c60c28b29a57eea4cb098ca"><span class="id" title="notation">@</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#18cd0ece1c60c28b29a57eea4cb098ca"><span class="id" title="notation">id</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="idGfun"><span class="id" title="definition">idGfun</span></a> <span class="id" title="var">gT</span> := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#481b7e18e0f4d27d48ec2e56a543d475"><span class="id" title="notation">@</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#481b7e18e0f4d27d48ec2e56a543d475"><span class="id" title="notation">id</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.gfunctor.html#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="idGfun_closed"><span class="id" title="lemma">idGfun_closed</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#closed"><span class="id" title="definition">GFunctor.closed</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#idGfun"><span class="id" title="definition">idGfun</span></a>.  <br/>
@@ -553,20 +552,20 @@
 <span class="id" title="keyword">Lemma</span> <a name="idGfun_monotonic"><span class="id" title="lemma">idGfun_monotonic</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#monotonic"><span class="id" title="definition">GFunctor.monotonic</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#idGfun"><span class="id" title="definition">idGfun</span></a>.  <br/>
 
 <br/>
-<span class="id" title="keyword">Canonical</span> <span class="id" title="var">bgFunc_id</span> := <a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">igFun</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#idGfun_closed"><span class="id" title="lemma">idGfun_closed</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#idGfun_cont"><span class="id" title="lemma">idGfun_cont</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">]</span></a>.<br/>
-<span class="id" title="keyword">Canonical</span> <span class="id" title="var">gFunc_id</span> := <a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">gFun</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#idGfun_cont"><span class="id" title="lemma">idGfun_cont</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">]</span></a>.<br/>
-<span class="id" title="keyword">Canonical</span> <span class="id" title="var">mgFunc_id</span> := <a class="idref" href="mathcomp.solvable.gfunctor.html#34d675edff20d6d91e43f305650662d9"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#34d675edff20d6d91e43f305650662d9"><span class="id" title="notation">mgFun</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#34d675edff20d6d91e43f305650662d9"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#idGfun_monotonic"><span class="id" title="lemma">idGfun_monotonic</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#34d675edff20d6d91e43f305650662d9"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">bgFunc_id</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> <a class="idref" href="mathcomp.solvable.gfunctor.html#idGfun_closed"><span class="id" title="lemma">idGfun_closed</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#c0205c751a17b7793ccdaf02cc4999e3"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#idGfun_cont"><span class="id" title="lemma">idGfun_cont</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">gFunc_id</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.gfunctor.html#idGfun_cont"><span class="id" title="lemma">idGfun_cont</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">mgFunc_id</span> := <a class="idref" href="mathcomp.solvable.gfunctor.html#f3da3221c5171e732a65fec8cc2ba4fa"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#f3da3221c5171e732a65fec8cc2ba4fa"><span class="id" title="notation">mgFun</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#f3da3221c5171e732a65fec8cc2ba4fa"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#idGfun_monotonic"><span class="id" title="lemma">idGfun_monotonic</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#f3da3221c5171e732a65fec8cc2ba4fa"><span class="id" title="notation">]</span></a>.<br/>
 
 <br/>
-<span class="id" title="keyword">Definition</span> <a name="trivGfun"><span class="id" title="definition">trivGfun</span></a> <span class="id" title="var">gT</span> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a> := <a class="idref" href="mathcomp.fingroup.fingroup.html#26d0437a0433a7dd4f49130a7fb26acc"><span class="id" title="notation">[1</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#26d0437a0433a7dd4f49130a7fb26acc"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Definition</span> <a name="trivGfun"><span class="id" title="definition">trivGfun</span></a> <span class="id" title="var">gT</span> <span class="id" title="keyword">of</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.gfunctor.html#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#80a826bb5c5b3ef58870b90cd3030216"><span class="id" title="notation">[1</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#80a826bb5c5b3ef58870b90cd3030216"><span class="id" title="notation">]</span></a>.<br/>
 
 <br/>
 <span class="id" title="keyword">Lemma</span> <a name="trivGfun_cont"><span class="id" title="lemma">trivGfun_cont</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#pcontinuous"><span class="id" title="definition">GFunctor.pcontinuous</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#trivGfun"><span class="id" title="definition">trivGfun</span></a>.<br/>
  
 <br/>
-<span class="id" title="keyword">Canonical</span> <span class="id" title="var">trivGfun_igFun</span> := <a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">igFun</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#sub1G"><span class="id" title="lemma">sub1G</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#trivGfun_cont"><span class="id" title="lemma">trivGfun_cont</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#a1ae11930941a680f6750f6723874923"><span class="id" title="notation">]</span></a>.<br/>
-<span class="id" title="keyword">Canonical</span> <span class="id" title="var">trivGfun_gFun</span> := <a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">gFun</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#trivGfun_cont"><span class="id" title="lemma">trivGfun_cont</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#f83b8fb103ae042d25e7034a8b11b7e7"><span class="id" title="notation">]</span></a>.<br/>
-<span class="id" title="keyword">Canonical</span> <span class="id" title="var">trivGfun_pgFun</span> := <a class="idref" href="mathcomp.solvable.gfunctor.html#75f5bf98333ce9930f3fc4415f01e6a0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#75f5bf98333ce9930f3fc4415f01e6a0"><span class="id" title="notation">pgFun</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#75f5bf98333ce9930f3fc4415f01e6a0"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#trivGfun_cont"><span class="id" title="lemma">trivGfun_cont</span></a><a class="idref" href="mathcomp.solvable.gfunctor.html#75f5bf98333ce9930f3fc4415f01e6a0"><span class="id" title="notation">]</span></a>.<br/>
+<span class="id" title="keyword">Canonical</span> <span class="id" title="var">trivGfun_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> <a class="idref" href="mathcomp.fingroup.fingroup.html#sub1G"><span class="id" title="lemma">sub1G</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#c0205c751a17b7793ccdaf02cc4999e3"><span class="id" title="notation">&amp;</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#trivGfun_cont"><span class="id" title="lemma">trivGfun_cont</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">trivGfun_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.gfunctor.html#trivGfun_cont"><span class="id" title="lemma">trivGfun_cont</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">trivGfun_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.gfunctor.html#trivGfun_cont"><span class="id" title="lemma">trivGfun_cont</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">End</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctorExamples"><span class="id" title="section">GFunctorExamples</span></a>.<br/>
author	Enrico Tassi	2019-05-22 13:43:08 +0200
committer	Enrico Tassi	2019-05-22 15:34:14 +0200
commit	748d716efb2f2f75946c8386e441ce1789806a39 (patch)
tree	fe7bb1c5235550410c64e968f4a4d69b7f10a047 /docs/htmldoc/mathcomp.solvable.gfunctor.html
parent	415be3b908daadabf178a292c885db78e5b2c9a4 (diff)