diff options
Diffstat (limited to 'docs/htmldoc/mathcomp.solvable.gfunctor.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.solvable.gfunctor.html | 584 |
1 files changed, 0 insertions, 584 deletions
diff --git a/docs/htmldoc/mathcomp.solvable.gfunctor.html b/docs/htmldoc/mathcomp.solvable.gfunctor.html deleted file mode 100644 index c5f3789..0000000 --- a/docs/htmldoc/mathcomp.solvable.gfunctor.html +++ /dev/null @@ -1,584 +0,0 @@ -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" -"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> -<html xmlns="http://www.w3.org/1999/xhtml"> -<head> -<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> -<link href="coqdoc.css" rel="stylesheet" type="text/css" /> -<title>mathcomp.solvable.gfunctor</title> -</head> - -<body> - -<div id="page"> - -<div id="header"> -</div> - -<div id="main"> - -<h1 class="libtitle">Library mathcomp.solvable.gfunctor</h1> - -<div class="code"> -<span class="comment">(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. <br/> - Distributed under the terms of CeCILL-B. *)</span><br/> - -<br/> -</div> - -<div class="doc"> - This file provides basic interfaces for the notion of "generic" - characteristic subgroups; these amount to subfunctors of the identity - functor in some category of groups. - See "Generic Proof Tools And Finite Group Theory", - Francois Garillot, PhD, 2011, Chapter 3. - The implementation proposed here is fairly basic, relying on first order - function matching and on structure telescopes, both of which are somewhat - limited and fragile. It should switch in the future to more general and - more robust quotation matching. - The definitions in this file (types, properties and structures) are all - packaged under the GFunctor submodule, i.e., client code should refer to - GFunctor.continuous, GFunctor.map, etc. Notations, Coercions and Lemmas - are exported and thus directly available, however. - We provide the following: - object_map == the type of the (polymorphic) object map of a group - functor; the %gF scope is bound to object_map. - := forall gT : finGroupType, {set gT} -> {set gT}. - We define two operations on object_map (with notations in the %gF scope): - F1 \o F2 == the composite map; (F1 \o F2) G expands to F1 (F2 G). - F1 %% F2 == F1 computed modulo F2; we have - (F1 %% F2) G / F2 G = F1 (G / F2 G) - We define the following (type-polymorphic) properties of an object_map F: - group_valued F <-> F G is a group when G is a group - closed F <-> F G is a subgroup o fG when G is a group - continuous F <-> F is continuous with respect to morphism image: - for any f : {morphism G >-> ..}, f @* (F G) is a - a subgroup of F (f @* G); equivalently, F is - functorial in the category Grp of groups. - Most common "characteristic subgroup" are produced - continuous object maps. - iso_continuous F <-> F is continuous with respect to isomorphism image; - equivalently, F is functorial in the Grp groupoid. - The Puig and the Thompson J subgroups are examples - of iso_continuous maps that are not continuous. - pcontinuous F <-> F is continuous with respect to partial morphism - image, i.e., functorial in the category of groups - and partial morphisms. The center and p-core are - examples of pcontinuous maps. - hereditary F <-> inclusion in the image of F is hereditary, i.e., - for any subgroup H of G, the intersection of H with - F G is included in H. Note that F is pcontinuous - iff it is continuous and hereditary; indeed proofs - of pcontinuous F coerce to proofs of hereditary F - and continuous F. - monotonic F <-> F is monotonic with respect to inclusion: for any - subgroup H of G, F H is a subgroup of F G. The - derived and lower central series are examples of - monotonic maps. - Four structures provide interfaces to these properties: - GFunctor.iso_map == structure for object maps that are group_valued, - closed, and iso_continuous. - [igFun by Fsub & !Fcont] == the iso_map structure for an object map F - such that F G is canonically a group when G is, and - given Fsub : closed F and Fcont : iso_continuous F. - [igFun by Fsub & Fcont] == as above, but expecting Fcont : continuous F. - [igFun of F] == clone an existing GFunctor.iso_map structure for F. - GFunctor.map == structure for continuous object maps, inheriting - from the GFunctor.iso_map structure. - [gFun by Fcont] == the map structure for an F with a canonical iso_map - structure, given Fcont : continuous F. - [gFun of F] == clone an existing GFunctor.map structure for F. - GFunctor.pmap == structure for pcontinuous object maps, inheriting - from the GFunctor.map structure. - [pgFun by Fher] == the pmap structure for an F with a canonical map - structure, given Fher : hereditary F. - [pgFun of F] == clone an existing GFunctor.pmap structure for F. - GFunctor.mono_map == structure for monotonic, continuous object maps - inheriting from the GFunctor.map structure. - [mgFun by Fmon] == the mono_map structure for an F with a canonical - map structure, given Fmon : monotonic F. - [mgFun of F] == clone an existing GFunctor.mono_map structure for F - Lemmas for these group functors use either a 'gF' prefix or an 'F' suffix. - The (F1 \o F2) and (F1 %% F2) operations have canonical GFunctor.map - structures when F1 is monotonic or hereditary, respectively. -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Import</span> <span class="id" title="var">GroupScope</span>.<br/> - -<br/> -<span class="id" title="keyword">Set Implicit Arguments</span>.<br/> - -<br/> -<span class="id" title="keyword">Delimit</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">gFun_scope</span> <span class="id" title="keyword">with</span> <span class="id" title="var">gF</span>.<br/> - -<br/> -<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#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/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="GFunctor.Definitions"><span class="id" title="section">Definitions</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">gT</span> <span class="id" title="var">hT</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">Variable</span> <a name="GFunctor.Definitions.F"><span class="id" title="variable">F</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.object_map"><span class="id" title="definition">object_map</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - 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#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> - -<div class="doc"> - 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#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> - -<div class="doc"> - General functoriality, i.e., continuity of the object map -</div> -<div class="code"> -<span class="id" title="keyword">Definition</span> <a name="GFunctor.continuous"><span class="id" title="definition">continuous</span></a> :=<br/> - <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">>-></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/> - <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> - -<div class="doc"> - Functoriality on the Grp groupoid (arrows are restricted to isos). -</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/> - <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">>-></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/> - <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/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> - -<div class="doc"> - Functoriality on Grp with partial morphisms. -</div> -<div class="code"> -<span class="id" title="keyword">Definition</span> <a name="GFunctor.pcontinuous"><span class="id" title="definition">pcontinuous</span></a> :=<br/> - <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">>-></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/> - <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/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> - -<div class="doc"> - Heredity with respect to inclusion -</div> -<div class="code"> -<span class="id" title="keyword">Definition</span> <a name="GFunctor.hereditary"><span class="id" title="definition">hereditary</span></a> :=<br/> - <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">:&:</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/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> - -<div class="doc"> - Monotonicity with respect to inclusion -</div> -<div class="code"> -<span class="id" title="keyword">Definition</span> <a name="GFunctor.monotonic"><span class="id" title="definition">monotonic</span></a> :=<br/> - <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> - -<div class="doc"> - Self-expanding composition, and modulo -</div> -<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/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/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/> - <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/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="GFunctor.ClassDefinitions"><span class="id" title="section">ClassDefinitions</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Structure</span> <a name="GFunctor.iso_map"><span class="id" title="record">iso_map</span></a> := <a name="GFunctor.IsoMap"><span class="id" title="constructor">IsoMap</span></a> {<br/> - <a name="GFunctor.apply"><span class="id" title="projection">apply</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="var">_</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.group_valued"><span class="id" title="definition">group_valued</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#apply"><span class="id" title="method">apply</span></a>;<br/> - <span class="id" title="var">_</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.closed"><span class="id" title="definition">closed</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#apply"><span class="id" title="method">apply</span></a>;<br/> - <span class="id" title="var">_</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.iso_continuous"><span class="id" title="definition">iso_continuous</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#apply"><span class="id" title="method">apply</span></a><br/> -}.<br/> - -<br/> -<span class="id" title="keyword">Structure</span> <a name="GFunctor.map"><span class="id" title="record">map</span></a> := <a name="GFunctor.Map"><span class="id" title="constructor">Map</span></a> { <a name="GFunctor.iso_of_map"><span class="id" title="projection">iso_of_map</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.iso_map"><span class="id" title="record">iso_map</span></a>; <span class="id" title="var">_</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.continuous"><span class="id" title="definition">continuous</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#iso_of_map"><span class="id" title="method">iso_of_map</span></a> }.<br/> - -<br/> -<span class="id" title="keyword">Structure</span> <a name="GFunctor.pmap"><span class="id" title="record">pmap</span></a> := <a name="GFunctor.Pmap"><span class="id" title="constructor">Pmap</span></a> { <a name="GFunctor.map_of_pmap"><span class="id" title="projection">map_of_pmap</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.map"><span class="id" title="record">map</span></a>; <span class="id" title="var">_</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.hereditary"><span class="id" title="definition">hereditary</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#map_of_pmap"><span class="id" title="method">map_of_pmap</span></a> }.<br/> - -<br/> -<span class="id" title="keyword">Structure</span> <a name="GFunctor.mono_map"><span class="id" title="record">mono_map</span></a> := <a name="GFunctor.MonoMap"><span class="id" title="constructor">MonoMap</span></a> { <a name="GFunctor.map_of_mono"><span class="id" title="projection">map_of_mono</span></a> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.map"><span class="id" title="record">map</span></a>; <span class="id" title="var">_</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.monotonic"><span class="id" title="definition">monotonic</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#map_of_mono"><span class="id" title="method">map_of_mono</span></a> }.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="GFunctor.pack_iso"><span class="id" title="definition">pack_iso</span></a> <span class="id" title="var">F</span> <span class="id" title="var">Fcont</span> <span class="id" title="var">Fgrp</span> <span class="id" title="var">Fsub</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/> - -<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/> - <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/> - <span class="id" title="keyword">fun</span> <span class="id" title="var">isoF0</span> & <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> & <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/> - <span class="id" title="keyword">fun</span> <span class="id" title="var">isoF</span> & <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/> - <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>) & <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/> - <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>) & <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/> - <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>) & <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/> - <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>) & <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/> - <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>) & <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/> - <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>) & <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/> - <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>) & <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/> - <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>) & <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/> - -<br/> -<span class="id" title="keyword">Module</span> <a name="GFunctor.Exports"><span class="id" title="module">Exports</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Identity</span> <span class="id" title="keyword">Coercion</span> <span class="id" title="var">fun_of_object_map</span> : <span class="id" title="var">object_map</span> >-> <span class="id" title="var">Funclass</span>.<br/> -<span class="id" title="keyword">Coercion</span> <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#GFunctor.apply"><span class="id" title="projection">:</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.apply"><span class="id" title="projection">iso_map</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.apply"><span class="id" title="projection">>-></span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.apply"><span class="id" title="projection">object_map</span></a>.<br/> -<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.iso_of_map"><span class="id" title="projection">iso_of_map</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.iso_of_map"><span class="id" title="projection">:</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.iso_of_map"><span class="id" title="projection">map</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.iso_of_map"><span class="id" title="projection">>-></span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.iso_of_map"><span class="id" title="projection">iso_map</span></a>.<br/> -<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.map_of_pmap"><span class="id" title="projection">map_of_pmap</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.map_of_pmap"><span class="id" title="projection">:</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.map_of_pmap"><span class="id" title="projection">pmap</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.map_of_pmap"><span class="id" title="projection">>-></span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.map_of_pmap"><span class="id" title="projection">map</span></a>.<br/> -<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.map_of_mono"><span class="id" title="projection">map_of_mono</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.map_of_mono"><span class="id" title="projection">:</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.map_of_mono"><span class="id" title="projection">mono_map</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.map_of_mono"><span class="id" title="projection">>-></span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.map_of_mono"><span class="id" title="projection">map</span></a>.<br/> -<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#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_is_iso_continuous"><span class="id" title="lemma">:</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.continuous_is_iso_continuous"><span class="id" title="lemma">continuous</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.continuous_is_iso_continuous"><span class="id" title="lemma">>-></span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.continuous_is_iso_continuous"><span class="id" title="lemma">iso_continuous</span></a>.<br/> -<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pcontinuous_is_continuous"><span class="id" title="lemma">pcontinuous_is_continuous</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pcontinuous_is_continuous"><span class="id" title="lemma">:</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pcontinuous_is_continuous"><span class="id" title="lemma">pcontinuous</span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pcontinuous_is_continuous"><span class="id" title="lemma">>-></span></a> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.pcontinuous_is_continuous"><span class="id" title="lemma">continuous</span></a>.<br/> -<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">>-></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="c0205c751a17b7793ccdaf02cc4999e3"><span class="id" title="notation">"</span></a>[ 'igFun' 'by' Fsub & Fcont ]" :=<br/> - (<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/> - (<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 & Fcont ]") : <span class="id" title="var">form_scope</span>.<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="8dd9a311237b4fd5bc515a2cbf48517e"><span class="id" title="notation">"</span></a>[ 'igFun' 'by' Fsub & ! Fcont ]" :=<br/> - (<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/> - (<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 & ! Fcont ]") : <span class="id" title="var">form_scope</span>.<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="0a3c3d64903581df0193a363279f22cc"><span class="id" title="notation">"</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/> - (<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="cecbde1597e0d77a491e8c4f94033af4"><span class="id" title="notation">"</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="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="b978f29f27d17b625bd1a96535c57314"><span class="id" title="notation">"</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/> - (<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="f4a0ec7c18bd128b271d4428328fd43b"><span class="id" title="notation">"</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="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="09ca9041b424fb3a198e2a775c1edfdd"><span class="id" title="notation">"</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/> - (<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="f3da3221c5171e732a65fec8cc2ba4fa"><span class="id" title="notation">"</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="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="703ce4e21f8af3122d8da8159ae55c98"><span class="id" title="notation">"</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/> - (<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/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor.Exports"><span class="id" title="module">Exports</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#GFunctor"><span class="id" title="module">GFunctor</span></a>.<br/> -<span class="id" title="keyword">Export</span> <span class="id" title="var">GFunctor.Exports</span>.<br/> - -<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="dca792ff4a91f336726016c880ff4199"><span class="id" title="notation">"</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">"</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#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/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.gfunctor.html#FunctorGroup"><span class="id" title="section">FunctorGroup</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">gFmod_group</span><br/> - (<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/> - (<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/> - <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/> - -<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">gT</span> <span class="id" title="var">rT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>.<br/> -<span class="id" title="keyword">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#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#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/> - <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/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#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#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#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#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"><|</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#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#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"><|</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"><|</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="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/> - <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#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">>-></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/> - <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#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">>-></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/> - <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#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">>-></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/> - <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#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/> - <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/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="FunctorTheory"><span class="id" title="section">FunctorTheory</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">gT</span> <span class="id" title="var">rT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>.<br/> -<span class="id" title="keyword">Variable</span> <a name="FunctorTheory.F"><span class="id" title="variable">F</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="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#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">>-></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/> - <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/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="PartialFunctorTheory"><span class="id" title="section">PartialFunctorTheory</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">gT</span> <span class="id" title="var">rT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="PartialFunctorTheory.BasicTheory"><span class="id" title="section">BasicTheory</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="PartialFunctorTheory.BasicTheory.F"><span class="id" title="variable">F</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="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#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/> - <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">:&:</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">:&:</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">:&:</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#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/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="PartialFunctorTheory.Modulo"><span class="id" title="section">Modulo</span></a>.<br/> - -<br/> -<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#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#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#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">&</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/> - -<br/> -<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#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#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/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="MonotonicFunctorTheory"><span class="id" title="section">MonotonicFunctorTheory</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">gT</span> <span class="id" title="var">rT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="gFunctorS"><span class="id" title="lemma">gFunctorS</span></a> (<span class="id" title="var">F</span> : <a class="idref" href="mathcomp.solvable.gfunctor.html#mono_map"><span class="id" title="record">GFunctor.mono_map</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#F"><span class="id" title="variable">F</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="MonotonicFunctorTheory.Composition"><span class="id" title="section">Composition</span></a>.<br/> - -<br/> -<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#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#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#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">&</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/> - -<br/> -<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#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#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/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="GFunctorExamples"><span class="id" title="section">GFunctorExamples</span></a>.<br/> - -<br/> -<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/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/> -<span class="id" title="keyword">Lemma</span> <a name="idGfun_cont"><span class="id" title="lemma">idGfun_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#idGfun"><span class="id" title="definition">idGfun</span></a>. <br/> -<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#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">&</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#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#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">&</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/> - -<br/> -</div> -</div> - -<div id="footer"> -<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a> -</div> - -</div> - -</body> -</html>
\ No newline at end of file |