diff options
| author | Enrico Tassi | 2019-05-22 13:43:08 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-05-22 15:34:14 +0200 |
| commit | 748d716efb2f2f75946c8386e441ce1789806a39 (patch) | |
| tree | fe7bb1c5235550410c64e968f4a4d69b7f10a047 /docs/htmldoc/mathcomp.fingroup.presentation.html | |
| parent | 415be3b908daadabf178a292c885db78e5b2c9a4 (diff) | |
htmldoc regenerated
Diffstat (limited to 'docs/htmldoc/mathcomp.fingroup.presentation.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.fingroup.presentation.html | 95 |
1 files changed, 47 insertions, 48 deletions
diff --git a/docs/htmldoc/mathcomp.fingroup.presentation.html b/docs/htmldoc/mathcomp.fingroup.presentation.html index 319155d..301b4f4 100644 --- a/docs/htmldoc/mathcomp.fingroup.presentation.html +++ b/docs/htmldoc/mathcomp.fingroup.presentation.html @@ -21,7 +21,6 @@ <div class="code"> <span class="comment">(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. <br/> Distributed under the terms of CeCILL-B. *)</span><br/> -<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#"><span class="id" title="library">mathcomp.ssreflect.ssreflect</span></a>.<br/> <br/> </div> @@ -110,10 +109,10 @@ <br/> <span class="id" title="keyword">Inductive</span> <a name="Presentation.term"><span class="id" title="inductive">term</span></a> :=<br/> - | <a name="Presentation.Cst"><span class="id" title="constructor">Cst</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><br/> + | <a name="Presentation.Cst"><span class="id" title="constructor">Cst</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><br/> | <a name="Presentation.Idx"><span class="id" title="constructor">Idx</span></a><br/> | <a name="Presentation.Inv"><span class="id" title="constructor">Inv</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.fingroup.presentation.html#term"><span class="id" title="inductive">term</span></a><br/> - | <a name="Presentation.Exp"><span class="id" title="constructor">Exp</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.fingroup.presentation.html#term"><span class="id" title="inductive">term</span></a> & <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><br/> + | <a name="Presentation.Exp"><span class="id" title="constructor">Exp</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.fingroup.presentation.html#term"><span class="id" title="inductive">term</span></a> & <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><br/> | <a name="Presentation.Mul"><span class="id" title="constructor">Mul</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.fingroup.presentation.html#term"><span class="id" title="inductive">term</span></a> & <a class="idref" href="mathcomp.fingroup.presentation.html#term"><span class="id" title="inductive">term</span></a><br/> | <a name="Presentation.Conj"><span class="id" title="constructor">Conj</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.fingroup.presentation.html#term"><span class="id" title="inductive">term</span></a> & <a class="idref" href="mathcomp.fingroup.presentation.html#term"><span class="id" title="inductive">term</span></a><br/> | <a name="Presentation.Comm"><span class="id" title="constructor">Comm</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.fingroup.presentation.html#term"><span class="id" title="inductive">term</span></a> & <a class="idref" href="mathcomp.fingroup.presentation.html#term"><span class="id" title="inductive">term</span></a>.<br/> @@ -123,11 +122,11 @@ <span class="id" title="keyword">match</span> <a class="idref" href="mathcomp.fingroup.presentation.html#t"><span class="id" title="variable">t</span></a> <span class="id" title="keyword">with</span><br/> | <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Cst"><span class="id" title="constructor">Cst</span></a> <span class="id" title="var">i</span> ⇒ <a class="idref" href="mathcomp.ssreflect.seq.html#nth"><span class="id" title="definition">nth</span></a> 1 <a class="idref" href="mathcomp.fingroup.presentation.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="var">i</span><br/> | <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Idx"><span class="id" title="constructor">Idx</span></a> ⇒ 1<br/> - | <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Inv"><span class="id" title="constructor">Inv</span></a> <span class="id" title="var">t1</span> ⇒ <a class="idref" href="mathcomp.fingroup.fingroup.html#a605acbeae7597f74f5a9b816ed8a717"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#eval"><span class="id" title="definition">eval</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="var">t1</span><a class="idref" href="mathcomp.fingroup.fingroup.html#a605acbeae7597f74f5a9b816ed8a717"><span class="id" title="notation">)^-1</span></a><br/> - | <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Exp"><span class="id" title="constructor">Exp</span></a> <span class="id" title="var">t1</span> <span class="id" title="var">n</span> ⇒ <a class="idref" href="mathcomp.fingroup.presentation.html#eval"><span class="id" title="definition">eval</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="var">t1</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#86a04fb564fb97d388cad84a3a204260"><span class="id" title="notation">^+</span></a> <span class="id" title="var">n</span><br/> - | <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Mul"><span class="id" title="constructor">Mul</span></a> <span class="id" title="var">t1</span> <span class="id" title="var">t2</span> ⇒ <a class="idref" href="mathcomp.fingroup.presentation.html#eval"><span class="id" title="definition">eval</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="var">t1</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#eval"><span class="id" title="definition">eval</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="var">t2</span><br/> - | <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Conj"><span class="id" title="constructor">Conj</span></a> <span class="id" title="var">t1</span> <span class="id" title="var">t2</span> ⇒ <a class="idref" href="mathcomp.fingroup.presentation.html#eval"><span class="id" title="definition">eval</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="var">t1</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#808c6b8e35e792f23899f360a21e4638"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#eval"><span class="id" title="definition">eval</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="var">t2</span><br/> - | <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Comm"><span class="id" title="constructor">Comm</span></a> <span class="id" title="var">t1</span> <span class="id" title="var">t2</span> ⇒ <a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#eval"><span class="id" title="definition">eval</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="var">t1</span><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#eval"><span class="id" title="definition">eval</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="var">t2</span><a class="idref" href="mathcomp.fingroup.fingroup.html#d5d566f861753940ef0e9a18d348c2b8"><span class="id" title="notation">]</span></a><br/> + | <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Inv"><span class="id" title="constructor">Inv</span></a> <span class="id" title="var">t1</span> ⇒ <a class="idref" href="mathcomp.fingroup.fingroup.html#766fd55608aa0e125ed6f55c83bcc09a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#eval"><span class="id" title="definition">eval</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="var">t1</span><a class="idref" href="mathcomp.fingroup.fingroup.html#766fd55608aa0e125ed6f55c83bcc09a"><span class="id" title="notation">)^-1</span></a><br/> + | <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Exp"><span class="id" title="constructor">Exp</span></a> <span class="id" title="var">t1</span> <span class="id" title="var">n</span> ⇒ <a class="idref" href="mathcomp.fingroup.presentation.html#eval"><span class="id" title="definition">eval</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="var">t1</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#06cdd2633d7788bac7abeac13b2dd91e"><span class="id" title="notation">^+</span></a> <span class="id" title="var">n</span><br/> + | <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Mul"><span class="id" title="constructor">Mul</span></a> <span class="id" title="var">t1</span> <span class="id" title="var">t2</span> ⇒ <a class="idref" href="mathcomp.fingroup.presentation.html#eval"><span class="id" title="definition">eval</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="var">t1</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#8b8794efbfbae1b793d9cb62ce802285"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#eval"><span class="id" title="definition">eval</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="var">t2</span><br/> + | <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Conj"><span class="id" title="constructor">Conj</span></a> <span class="id" title="var">t1</span> <span class="id" title="var">t2</span> ⇒ <a class="idref" href="mathcomp.fingroup.presentation.html#eval"><span class="id" title="definition">eval</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="var">t1</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#746f7e4d3218aa2699eefc064b513fc2"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#eval"><span class="id" title="definition">eval</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="var">t2</span><br/> + | <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Comm"><span class="id" title="constructor">Comm</span></a> <span class="id" title="var">t1</span> <span class="id" title="var">t2</span> ⇒ <a class="idref" href="mathcomp.fingroup.fingroup.html#fd6a490bd0f786b0eb5a7c1f70a1610e"><span class="id" title="notation">[~</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#eval"><span class="id" title="definition">eval</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="var">t1</span><a class="idref" href="mathcomp.fingroup.fingroup.html#fd6a490bd0f786b0eb5a7c1f70a1610e"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#eval"><span class="id" title="definition">eval</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="var">t2</span><a class="idref" href="mathcomp.fingroup.fingroup.html#fd6a490bd0f786b0eb5a7c1f70a1610e"><span class="id" title="notation">]</span></a><br/> <span class="id" title="keyword">end</span>.<br/> <br/> @@ -139,11 +138,11 @@ <span class="id" title="keyword">Inductive</span> <a name="Presentation.rel_type"><span class="id" title="inductive">rel_type</span></a> := <a name="Presentation.NoRel"><span class="id" title="constructor">NoRel</span></a> | <a name="Presentation.Rel"><span class="id" title="constructor">Rel</span></a> <span class="id" title="var">vT</span> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.fingroup.presentation.html#vT"><span class="id" title="variable">vT</span></a> & <a class="idref" href="mathcomp.fingroup.presentation.html#vT"><span class="id" title="variable">vT</span></a>.<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="Presentation.bool_of_rel"><span class="id" title="definition">bool_of_rel</span></a> <span class="id" title="var">r</span> := <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.fingroup.presentation.html#r"><span class="id" title="variable">r</span></a> <span class="id" title="keyword">is</span> <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Rel"><span class="id" title="constructor">Rel</span></a> <span class="id" title="var">vT</span> <span class="id" title="var">v1</span> <span class="id" title="var">v2</span> <span class="id" title="keyword">then</span> <span class="id" title="var">v1</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <span class="id" title="var">v2</span> <span class="id" title="keyword">else</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="Presentation.bool_of_rel"><span class="id" title="definition">bool_of_rel</span></a> <span class="id" title="var">r</span> := <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.fingroup.presentation.html#r"><span class="id" title="variable">r</span></a> <span class="id" title="keyword">is</span> <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Rel"><span class="id" title="constructor">Rel</span></a> <span class="id" title="var">vT</span> <span class="id" title="var">v1</span> <span class="id" title="var">v2</span> <span class="id" title="keyword">then</span> <span class="id" title="var">v1</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <span class="id" title="var">v2</span> <span class="id" title="keyword">else</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a>.<br/> <br/> <span class="id" title="keyword">Definition</span> <a name="Presentation.and_rel"><span class="id" title="definition">and_rel</span></a> <span class="id" title="var">vT</span> (<span class="id" title="var">v1</span> <span class="id" title="var">v2</span> : <a class="idref" href="mathcomp.fingroup.presentation.html#vT"><span class="id" title="variable">vT</span></a>) <span class="id" title="var">r</span> :=<br/> - <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.fingroup.presentation.html#r"><span class="id" title="variable">r</span></a> <span class="id" title="keyword">is</span> <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Rel"><span class="id" title="constructor">Rel</span></a> <span class="id" title="var">wT</span> <span class="id" title="var">w1</span> <span class="id" title="var">w2</span> <span class="id" title="keyword">then</span> <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Rel"><span class="id" title="constructor">Rel</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#v1"><span class="id" title="variable">v1</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <span class="id" title="var">w1</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#v2"><span class="id" title="variable">v2</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">,</span></a> <span class="id" title="var">w2</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#44400027531d4bc3f586a1997dc874c0"><span class="id" title="notation">)</span></a> <span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Rel"><span class="id" title="constructor">Rel</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#v1"><span class="id" title="variable">v1</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#v2"><span class="id" title="variable">v2</span></a>.<br/> + <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.fingroup.presentation.html#r"><span class="id" title="variable">r</span></a> <span class="id" title="keyword">is</span> <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Rel"><span class="id" title="constructor">Rel</span></a> <span class="id" title="var">wT</span> <span class="id" title="var">w1</span> <span class="id" title="var">w2</span> <span class="id" title="keyword">then</span> <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Rel"><span class="id" title="constructor">Rel</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#v1"><span class="id" title="variable">v1</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <span class="id" title="var">w1</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#v2"><span class="id" title="variable">v2</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <span class="id" title="var">w2</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> <span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Rel"><span class="id" title="constructor">Rel</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#v1"><span class="id" title="variable">v1</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#v2"><span class="id" title="variable">v2</span></a>.<br/> <br/> <span class="id" title="keyword">Fixpoint</span> <a name="Presentation.rel"><span class="id" title="definition">rel</span></a> {<span class="id" title="var">gT</span>} (<span class="id" title="var">e</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#gT"><span class="id" title="variable">gT</span></a>) <span class="id" title="var">f</span> <span class="id" title="var">r</span> :=<br/> @@ -153,27 +152,27 @@ <span class="id" title="keyword">end</span>.<br/> <br/> -<span class="id" title="keyword">Inductive</span> <a name="Presentation.type"><span class="id" title="inductive">type</span></a> := <a name="Presentation.Generator"><span class="id" title="constructor">Generator</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.term"><span class="id" title="inductive">term</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#type"><span class="id" title="inductive">type</span></a> | <a name="Presentation.Formula"><span class="id" title="constructor">Formula</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.formula"><span class="id" title="inductive">formula</span></a>.<br/> +<span class="id" title="keyword">Inductive</span> <a name="Presentation.type"><span class="id" title="inductive">type</span></a> := <a name="Presentation.Generator"><span class="id" title="constructor">Generator</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.term"><span class="id" title="inductive">term</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.presentation.html#type"><span class="id" title="inductive">type</span></a> | <a name="Presentation.Formula"><span class="id" title="constructor">Formula</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.formula"><span class="id" title="inductive">formula</span></a>.<br/> <span class="id" title="keyword">Definition</span> <a name="Presentation.Cast"><span class="id" title="definition">Cast</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.type"><span class="id" title="inductive">type</span></a> := <a class="idref" href="mathcomp.fingroup.presentation.html#p"><span class="id" title="variable">p</span></a>. <span class="comment">(* syntactic scope cast *)</span><br/> <br/> -<span class="id" title="keyword">Inductive</span> <a name="Presentation.env"><span class="id" title="inductive">env</span></a> <span class="id" title="var">gT</span> := <a name="Presentation.Env"><span class="id" title="constructor">Env</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a> & <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#gT"><span class="id" title="variable">gT</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="Presentation.env1"><span class="id" title="definition">env1</span></a> {<span class="id" title="var">gT</span>} (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.fingroup.presentation.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#4509b22bf26e3d6d771897e22bd8bc8f"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) := <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Env"><span class="id" title="constructor">Env</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#30152704c0ab4066186d0284456667e8"><span class="id" title="notation"><[</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#30152704c0ab4066186d0284456667e8"><span class="id" title="notation">]></span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">[::</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#36229928b54642a4a7da943ccf8f9612"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Inductive</span> <a name="Presentation.env"><span class="id" title="inductive">env</span></a> <span class="id" title="var">gT</span> := <a name="Presentation.Env"><span class="id" title="constructor">Env</span></a> <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.fingroup.presentation.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.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#gT"><span class="id" title="variable">gT</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="Presentation.env1"><span class="id" title="definition">env1</span></a> {<span class="id" title="var">gT</span>} (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.fingroup.presentation.html#gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) := <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Env"><span class="id" title="constructor">Env</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#5e5825d099c952c2db2842c142cbde94"><span class="id" title="notation"><[</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#5e5825d099c952c2db2842c142cbde94"><span class="id" title="notation">]></span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#506674b18256ef8f50efed43fa1dfd7d"><span class="id" title="notation">[::</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.ssreflect.seq.html#506674b18256ef8f50efed43fa1dfd7d"><span class="id" title="notation">]</span></a>.<br/> <br/> -<span class="id" title="keyword">Fixpoint</span> <a name="Presentation.sat"><span class="id" title="definition">sat</span></a> <span class="id" title="var">gT</span> <span class="id" title="var">vT</span> <span class="id" title="var">B</span> <span class="id" title="var">n</span> (<span class="id" title="var">s</span> : <a class="idref" href="mathcomp.fingroup.presentation.html#vT"><span class="id" title="variable">vT</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.env"><span class="id" title="inductive">env</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#gT"><span class="id" title="variable">gT</span></a>) <span class="id" title="var">p</span> :=<br/> +<span class="id" title="keyword">Fixpoint</span> <a name="Presentation.sat"><span class="id" title="definition">sat</span></a> <span class="id" title="var">gT</span> <span class="id" title="var">vT</span> <span class="id" title="var">B</span> <span class="id" title="var">n</span> (<span class="id" title="var">s</span> : <a class="idref" href="mathcomp.fingroup.presentation.html#vT"><span class="id" title="variable">vT</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.presentation.html#Presentation.env"><span class="id" title="inductive">env</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#gT"><span class="id" title="variable">gT</span></a>) <span class="id" title="var">p</span> :=<br/> <span class="id" title="keyword">match</span> <a class="idref" href="mathcomp.fingroup.presentation.html#p"><span class="id" title="variable">p</span></a> <span class="id" title="keyword">with</span><br/> | <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Formula"><span class="id" title="constructor">Formula</span></a> <span class="id" title="var">f</span> ⇒<br/> - <a class="idref" href="mathcomp.ssreflect.fintype.html#e1fcc6c8b4370f06a39f9b1b3c9764b2"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#e1fcc6c8b4370f06a39f9b1b3c9764b2"><span class="id" title="notation">∃</span></a> <span class="id" title="var">v</span><a class="idref" href="mathcomp.ssreflect.fintype.html#46e5a4123d46e6b126f7788a77176785"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">let</span>: <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Env"><span class="id" title="constructor">Env</span></a> <span class="id" title="var">A</span> <span class="id" title="var">e</span> := <a class="idref" href="mathcomp.fingroup.presentation.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#v"><span class="id" title="variable">v</span></a> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.and_rel"><span class="id" title="definition">and_rel</span></a> <span class="id" title="var">A</span> <a class="idref" href="mathcomp.fingroup.presentation.html#B"><span class="id" title="variable">B</span></a> (<a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.rel"><span class="id" title="definition">rel</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#rev"><span class="id" title="definition">rev</span></a> <span class="id" title="var">e</span>) <span class="id" title="var">f</span> <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.NoRel"><span class="id" title="constructor">NoRel</span></a>)<a class="idref" href="mathcomp.ssreflect.fintype.html#e1fcc6c8b4370f06a39f9b1b3c9764b2"><span class="id" title="notation">]</span></a><br/> + <a class="idref" href="mathcomp.ssreflect.fintype.html#ea6c97f834d69613538d4da1fb704b25"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#ea6c97f834d69613538d4da1fb704b25"><span class="id" title="notation">∃</span></a> <span class="id" title="var">v</span><a class="idref" href="mathcomp.ssreflect.fintype.html#f3be25edeb0349b0a76405eded9d0b98"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">let</span>: <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Env"><span class="id" title="constructor">Env</span></a> <span class="id" title="var">A</span> <span class="id" title="var">e</span> := <a class="idref" href="mathcomp.fingroup.presentation.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#v"><span class="id" title="variable">v</span></a> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.and_rel"><span class="id" title="definition">and_rel</span></a> <span class="id" title="var">A</span> <a class="idref" href="mathcomp.fingroup.presentation.html#B"><span class="id" title="variable">B</span></a> (<a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.rel"><span class="id" title="definition">rel</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#rev"><span class="id" title="definition">rev</span></a> <span class="id" title="var">e</span>) <span class="id" title="var">f</span> <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.NoRel"><span class="id" title="constructor">NoRel</span></a>)<a class="idref" href="mathcomp.ssreflect.fintype.html#ea6c97f834d69613538d4da1fb704b25"><span class="id" title="notation">]</span></a><br/> | <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Generator"><span class="id" title="constructor">Generator</span></a> <span class="id" title="var">p'</span> ⇒<br/> - <span class="id" title="keyword">let</span> <span class="id" title="var">s'</span> <span class="id" title="var">v</span> := <span class="id" title="keyword">let</span>: <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Env"><span class="id" title="constructor">Env</span></a> <span class="id" title="var">A</span> <span class="id" title="var">e</span> := <a class="idref" href="mathcomp.fingroup.presentation.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#v"><span class="id" title="variable">v</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c4877bbfe60d8f22b47ac99ace86216a"><span class="id" title="notation">.1</span></a> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Env"><span class="id" title="constructor">Env</span></a> (<span class="id" title="var">A</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#80208730563aa86aa7861f6fe1b846da"><span class="id" title="notation"><*></span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#30152704c0ab4066186d0284456667e8"><span class="id" title="notation"><[</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#v"><span class="id" title="variable">v</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#f4827404159513e7fd691b60b7877737"><span class="id" title="notation">.2</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#30152704c0ab4066186d0284456667e8"><span class="id" title="notation">]></span></a>) (<a class="idref" href="mathcomp.fingroup.presentation.html#v"><span class="id" title="variable">v</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#f4827404159513e7fd691b60b7877737"><span class="id" title="notation">.2</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#d7fed0909a58e41c49e3ee117361b0a5"><span class="id" title="notation">::</span></a> <span class="id" title="var">e</span>) <span class="id" title="tactic">in</span><br/> - <a class="idref" href="mathcomp.fingroup.presentation.html#sat"><span class="id" title="definition">sat</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#B"><span class="id" title="variable">B</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#s'"><span class="id" title="variable">s'</span></a> (<span class="id" title="var">p'</span> (<a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Cst"><span class="id" title="constructor">Cst</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#n"><span class="id" title="variable">n</span></a>))<br/> + <span class="id" title="keyword">let</span> <span class="id" title="var">s'</span> <span class="id" title="var">v</span> := <span class="id" title="keyword">let</span>: <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Env"><span class="id" title="constructor">Env</span></a> <span class="id" title="var">A</span> <span class="id" title="var">e</span> := <a class="idref" href="mathcomp.fingroup.presentation.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#v"><span class="id" title="variable">v</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e0817251e7d67ad994b4d9b1aa82a412"><span class="id" title="notation">.1</span></a> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Env"><span class="id" title="constructor">Env</span></a> (<span class="id" title="var">A</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#0d7ccd69af81527d9facc6293603bbef"><span class="id" title="notation"><*></span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#5e5825d099c952c2db2842c142cbde94"><span class="id" title="notation"><[</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#v"><span class="id" title="variable">v</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#675082cc4d4538da052b547bdc6ea4c9"><span class="id" title="notation">.2</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#5e5825d099c952c2db2842c142cbde94"><span class="id" title="notation">]></span></a>) (<a class="idref" href="mathcomp.fingroup.presentation.html#v"><span class="id" title="variable">v</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#675082cc4d4538da052b547bdc6ea4c9"><span class="id" title="notation">.2</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#407cde5b61fbf27196d1a7c5a475e083"><span class="id" title="notation">::</span></a> <span class="id" title="var">e</span>) <span class="id" title="tactic">in</span><br/> + <a class="idref" href="mathcomp.fingroup.presentation.html#sat"><span class="id" title="definition">sat</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#B"><span class="id" title="variable">B</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#s'"><span class="id" title="variable">s'</span></a> (<span class="id" title="var">p'</span> (<a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Cst"><span class="id" title="constructor">Cst</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#n"><span class="id" title="variable">n</span></a>))<br/> <span class="id" title="keyword">end</span>.<br/> <br/> -<span class="id" title="keyword">Definition</span> <a name="Presentation.hom"><span class="id" title="definition">hom</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">B</span> : <a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a>) <span class="id" title="var">p</span> := <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.sat"><span class="id" title="definition">sat</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#B"><span class="id" title="variable">B</span></a> 1 <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.env1"><span class="id" title="definition">env1</span></a> (<a class="idref" href="mathcomp.fingroup.presentation.html#p"><span class="id" title="variable">p</span></a> (<a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Cst"><span class="id" title="constructor">Cst</span></a> 0)).<br/> -<span class="id" title="keyword">Definition</span> <a name="Presentation.iso"><span class="id" title="definition">iso</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">B</span> : <a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a>) <span class="id" title="var">p</span> :=<br/> - <span class="id" title="keyword">∀</span> <span class="id" title="var">rT</span> (<span class="id" title="var">H</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>), <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#660be9f1a393f4f575133c9df42aec65"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#660be9f1a393f4f575133c9df42aec65"><span class="id" title="notation">homg</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.hom"><span class="id" title="definition">hom</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#p"><span class="id" title="variable">p</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="Presentation.hom"><span class="id" title="definition">hom</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">B</span> : <a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.fingroup.presentation.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>) <span class="id" title="var">p</span> := <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.sat"><span class="id" title="definition">sat</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#B"><span class="id" title="variable">B</span></a> 1 <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.env1"><span class="id" title="definition">env1</span></a> (<a class="idref" href="mathcomp.fingroup.presentation.html#p"><span class="id" title="variable">p</span></a> (<a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Cst"><span class="id" title="constructor">Cst</span></a> 0)).<br/> +<span class="id" title="keyword">Definition</span> <a name="Presentation.iso"><span class="id" title="definition">iso</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">B</span> : <a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.fingroup.presentation.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>) <span class="id" title="var">p</span> :=<br/> + <span class="id" title="keyword">∀</span> <span class="id" title="var">rT</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.fingroup.presentation.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>), <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#9899c777f5fa3790d4aad7f054b13e7e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#9899c777f5fa3790d4aad7f054b13e7e"><span class="id" title="notation">homg</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.hom"><span class="id" title="definition">hom</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#p"><span class="id" title="variable">p</span></a>.<br/> <br/> <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Presentation"><span class="id" title="section">Presentation</span></a>.<br/> @@ -196,19 +195,19 @@ Declare (implicitly) the argument scope tags. </div> <div class="code"> -<span class="id" title="keyword">Notation</span> <a name="fdd08c360a81ff74ae8a2a86cc557420"><span class="id" title="notation">"</span></a>1" := <a class="idref" href="mathcomp.fingroup.presentation.html#Idx"><span class="id" title="constructor">Idx</span></a> : <span class="id" title="var">group_presentation</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="3711121880f447b061452286b0381dec"><span class="id" title="notation">"</span></a>1" := <a class="idref" href="mathcomp.fingroup.presentation.html#Idx"><span class="id" title="constructor">Idx</span></a> : <span class="id" title="var">group_presentation</span>.<br/> <br/> -<span class="id" title="keyword">Infix</span> <a name="40473e5ae833bb83bfffbe406bfcb79c"><span class="id" title="notation">"</span></a>×" := <a class="idref" href="mathcomp.fingroup.presentation.html#Mul"><span class="id" title="constructor">Mul</span></a> : <span class="id" title="var">group_presentation</span>.<br/> -<span class="id" title="keyword">Infix</span> <a name="93f82d9635dc31e1d0b435f42eb3dc73"><span class="id" title="notation">"</span></a>^+" := <a class="idref" href="mathcomp.fingroup.presentation.html#Exp"><span class="id" title="constructor">Exp</span></a> : <span class="id" title="var">group_presentation</span>.<br/> -<span class="id" title="keyword">Infix</span> <a name="0fbb201450901f2490e64ed12c373bb6"><span class="id" title="notation">"</span></a>^" := <a class="idref" href="mathcomp.fingroup.presentation.html#Conj"><span class="id" title="constructor">Conj</span></a> : <span class="id" title="var">group_presentation</span>.<br/> -<span class="id" title="keyword">Notation</span> <a name="5006c7a985edeed550bd2a6db74b0161"><span class="id" title="notation">"</span></a>x ^-1" := (<a class="idref" href="mathcomp.fingroup.presentation.html#Inv"><span class="id" title="constructor">Inv</span></a> <span class="id" title="var">x</span>) : <span class="id" title="var">group_presentation</span>.<br/> -<span class="id" title="keyword">Notation</span> <a name="566c15f2d6f782a9d09a9fb26344b7d3"><span class="id" title="notation">"</span></a>x ^- n" := (<a class="idref" href="mathcomp.fingroup.presentation.html#Inv"><span class="id" title="constructor">Inv</span></a> (<span class="id" title="var">x</span> <a class="idref" href="mathcomp.fingroup.presentation.html#93f82d9635dc31e1d0b435f42eb3dc73"><span class="id" title="notation">^+</span></a> <span class="id" title="var">n</span>)) : <span class="id" title="var">group_presentation</span>.<br/> -<span class="id" title="keyword">Notation</span> <a name="a0040f72df5ea25d5ed5fbb0e00c50b5"><span class="id" title="notation">"</span></a>[ ~ x1 , x2 , .. , xn ]" :=<br/> +<span class="id" title="keyword">Infix</span> <a name="7ff3ac9f611fe85cb06e80e4192d07f5"><span class="id" title="notation">"</span></a>×" := <a class="idref" href="mathcomp.fingroup.presentation.html#Mul"><span class="id" title="constructor">Mul</span></a> : <span class="id" title="var">group_presentation</span>.<br/> +<span class="id" title="keyword">Infix</span> <a name="0280afab3b6487b32e979a01bfa577e6"><span class="id" title="notation">"</span></a>^+" := <a class="idref" href="mathcomp.fingroup.presentation.html#Exp"><span class="id" title="constructor">Exp</span></a> : <span class="id" title="var">group_presentation</span>.<br/> +<span class="id" title="keyword">Infix</span> <a name="b52ad9f454dbbbe5277b0e0896d02a68"><span class="id" title="notation">"</span></a>^" := <a class="idref" href="mathcomp.fingroup.presentation.html#Conj"><span class="id" title="constructor">Conj</span></a> : <span class="id" title="var">group_presentation</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="ad1588003f4b5e4ce0779af0b97dfde8"><span class="id" title="notation">"</span></a>x ^-1" := (<a class="idref" href="mathcomp.fingroup.presentation.html#Inv"><span class="id" title="constructor">Inv</span></a> <span class="id" title="var">x</span>) : <span class="id" title="var">group_presentation</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="59cc92029134a0bad1f342fa3593323a"><span class="id" title="notation">"</span></a>x ^- n" := (<a class="idref" href="mathcomp.fingroup.presentation.html#Inv"><span class="id" title="constructor">Inv</span></a> (<span class="id" title="var">x</span> <a class="idref" href="mathcomp.fingroup.presentation.html#0280afab3b6487b32e979a01bfa577e6"><span class="id" title="notation">^+</span></a> <span class="id" title="var">n</span>)) : <span class="id" title="var">group_presentation</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="2363e834cb9646bb24ef8d00777408b1"><span class="id" title="notation">"</span></a>[ ~ x1 , x2 , .. , xn ]" :=<br/> (<a class="idref" href="mathcomp.fingroup.presentation.html#Comm"><span class="id" title="constructor">Comm</span></a> .. (<a class="idref" href="mathcomp.fingroup.presentation.html#Comm"><span class="id" title="constructor">Comm</span></a> <span class="id" title="var">x1</span> <span class="id" title="var">x2</span>) .. <span class="id" title="var">xn</span>) : <span class="id" title="var">group_presentation</span>.<br/> -<span class="id" title="keyword">Notation</span> <a name="4783ea425920bc277a91db85db3ac693"><span class="id" title="notation">"</span></a>x = y" := (<a class="idref" href="mathcomp.fingroup.presentation.html#Eq2"><span class="id" title="constructor">Eq2</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) : <span class="id" title="var">group_presentation</span>.<br/> -<span class="id" title="keyword">Notation</span> <a name="59d6fe8b58ea45b75d962567e360006e"><span class="id" title="notation">"</span></a>x = y = z" := (<a class="idref" href="mathcomp.fingroup.presentation.html#Eq3"><span class="id" title="definition">Eq3</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span>) : <span class="id" title="var">group_presentation</span>.<br/> -<span class="id" title="keyword">Notation</span> <a name="5b8f67ffc457596b97fe80b0e075accd"><span class="id" title="notation">"</span></a>( r1 , r2 , .. , rn )" := <br/> +<span class="id" title="keyword">Notation</span> <a name="49dac265a72037ecb7c7f91d122c63b2"><span class="id" title="notation">"</span></a>x = y" := (<a class="idref" href="mathcomp.fingroup.presentation.html#Eq2"><span class="id" title="constructor">Eq2</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span>) : <span class="id" title="var">group_presentation</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="c694df6233deb9f06aafe9c8b549df99"><span class="id" title="notation">"</span></a>x = y = z" := (<a class="idref" href="mathcomp.fingroup.presentation.html#Eq3"><span class="id" title="definition">Eq3</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span>) : <span class="id" title="var">group_presentation</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="2ae8188eecf4af229df8a7611e947bc2"><span class="id" title="notation">"</span></a>( r1 , r2 , .. , rn )" := <br/> (<a class="idref" href="mathcomp.fingroup.presentation.html#And"><span class="id" title="constructor">And</span></a> .. (<a class="idref" href="mathcomp.fingroup.presentation.html#And"><span class="id" title="constructor">And</span></a> <span class="id" title="var">r1</span> <span class="id" title="var">r2</span>) .. <span class="id" title="var">rn</span>) : <span class="id" title="var">group_presentation</span>.<br/> <br/> @@ -218,26 +217,26 @@ Declare (implicitly) the argument scope tags. </div> <div class="code"> -<span class="id" title="keyword">Notation</span> <a name="2ae0895480985bc952c837cfb1a204f0"><span class="id" title="notation">"</span></a>x : p" := (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> ⇒ <a class="idref" href="mathcomp.fingroup.presentation.html#Cast"><span class="id" title="definition">Cast</span></a> <span class="id" title="var">p</span>) : <span class="id" title="var">nt_group_presentation</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="6e2a81a60d9e95e3dfebb879373bbe48"><span class="id" title="notation">"</span></a>x : p" := (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> ⇒ <a class="idref" href="mathcomp.fingroup.presentation.html#Cast"><span class="id" title="definition">Cast</span></a> <span class="id" title="var">p</span>) : <span class="id" title="var">nt_group_presentation</span>.<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="953d1fbe50819ac104ff2928ed9f1f35"><span class="id" title="notation">"</span></a>x : p" := (<a class="idref" href="mathcomp.fingroup.presentation.html#Generator"><span class="id" title="constructor">Generator</span></a> (<span class="id" title="var">x</span> <a class="idref" href="mathcomp.fingroup.presentation.html#2ae0895480985bc952c837cfb1a204f0"><span class="id" title="notation">:</span></a> <span class="id" title="var">p</span>)) : <span class="id" title="var">group_presentation</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="dabeb9211165bee23a272123a1fbb765"><span class="id" title="notation">"</span></a>x : p" := (<a class="idref" href="mathcomp.fingroup.presentation.html#Generator"><span class="id" title="constructor">Generator</span></a> (<span class="id" title="var">x</span> <a class="idref" href="mathcomp.fingroup.presentation.html#6e2a81a60d9e95e3dfebb879373bbe48"><span class="id" title="notation">:</span></a> <span class="id" title="var">p</span>)) : <span class="id" title="var">group_presentation</span>.<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="05034b80a22270f72f61c5366c67d457"><span class="id" title="notation">"</span></a>H \homg 'Grp' p" := (<a class="idref" href="mathcomp.fingroup.presentation.html#hom"><span class="id" title="definition">hom</span></a> <span class="id" title="var">H</span> <span class="id" title="var">p</span>)<br/> +<span class="id" title="keyword">Notation</span> <a name="7a9fb4aa00755e86dee5fc756da05fc2"><span class="id" title="notation">"</span></a>H \homg 'Grp' p" := (<a class="idref" href="mathcomp.fingroup.presentation.html#hom"><span class="id" title="definition">hom</span></a> <span class="id" title="var">H</span> <span class="id" title="var">p</span>)<br/> (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 70, <span class="id" title="var">p</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "H \homg 'Grp' p") : <span class="id" title="var">group_scope</span>.<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="19e0d8275b5f9ef645d1fd2c7dda9a9b"><span class="id" title="notation">"</span></a>H \isog 'Grp' p" := (<a class="idref" href="mathcomp.fingroup.presentation.html#iso"><span class="id" title="definition">iso</span></a> <span class="id" title="var">H</span> <span class="id" title="var">p</span>)<br/> +<span class="id" title="keyword">Notation</span> <a name="2033817e0a446c02fb5fa9a7fdad6117"><span class="id" title="notation">"</span></a>H \isog 'Grp' p" := (<a class="idref" href="mathcomp.fingroup.presentation.html#iso"><span class="id" title="definition">iso</span></a> <span class="id" title="var">H</span> <span class="id" title="var">p</span>)<br/> (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 70, <span class="id" title="var">p</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "H \isog 'Grp' p") : <span class="id" title="var">group_scope</span>.<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="9ecb35394efff43e3edfa027e1fd0f1f"><span class="id" title="notation">"</span></a>H \homg 'Grp' ( x : p )" := (<a class="idref" href="mathcomp.fingroup.presentation.html#hom"><span class="id" title="definition">hom</span></a> <span class="id" title="var">H</span> (<span class="id" title="var">x</span> <a class="idref" href="mathcomp.fingroup.presentation.html#2ae0895480985bc952c837cfb1a204f0"><span class="id" title="notation">:</span></a> <span class="id" title="var">p</span>))<br/> +<span class="id" title="keyword">Notation</span> <a name="d500832abea87e915b3cd89b548763b1"><span class="id" title="notation">"</span></a>H \homg 'Grp' ( x : p )" := (<a class="idref" href="mathcomp.fingroup.presentation.html#hom"><span class="id" title="definition">hom</span></a> <span class="id" title="var">H</span> (<span class="id" title="var">x</span> <a class="idref" href="mathcomp.fingroup.presentation.html#6e2a81a60d9e95e3dfebb879373bbe48"><span class="id" title="notation">:</span></a> <span class="id" title="var">p</span>))<br/> (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 70, <span class="id" title="var">x</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0,<br/> <span class="id" title="var">format</span> "'[hv' H '/ ' \homg 'Grp' ( x : p ) ']'") : <span class="id" title="var">group_scope</span>.<br/> <br/> -<span class="id" title="keyword">Notation</span> <a name="2e7e6fdc2fcc257cb8670b6b97d9b9ee"><span class="id" title="notation">"</span></a>H \isog 'Grp' ( x : p )" := (<a class="idref" href="mathcomp.fingroup.presentation.html#iso"><span class="id" title="definition">iso</span></a> <span class="id" title="var">H</span> (<span class="id" title="var">x</span> <a class="idref" href="mathcomp.fingroup.presentation.html#2ae0895480985bc952c837cfb1a204f0"><span class="id" title="notation">:</span></a> <span class="id" title="var">p</span>))<br/> +<span class="id" title="keyword">Notation</span> <a name="b9a7ff3fba421494dc2f1155a1739bdd"><span class="id" title="notation">"</span></a>H \isog 'Grp' ( x : p )" := (<a class="idref" href="mathcomp.fingroup.presentation.html#iso"><span class="id" title="definition">iso</span></a> <span class="id" title="var">H</span> (<span class="id" title="var">x</span> <a class="idref" href="mathcomp.fingroup.presentation.html#6e2a81a60d9e95e3dfebb879373bbe48"><span class="id" title="notation">:</span></a> <span class="id" title="var">p</span>))<br/> (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 70, <span class="id" title="var">x</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0,<br/> <span class="id" title="var">format</span> "'[hv' H '/ ' \isog 'Grp' ( x : p ) ']'") : <span class="id" title="var">group_scope</span>.<br/> @@ -251,28 +250,28 @@ <span class="id" title="keyword">Import</span> <span class="id" title="var">Presentation</span>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="isoGrp_hom"><span class="id" title="lemma">isoGrp_hom</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.fingroup.presentation.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#19e0d8275b5f9ef645d1fd2c7dda9a9b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#19e0d8275b5f9ef645d1fd2c7dda9a9b"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#19e0d8275b5f9ef645d1fd2c7dda9a9b"><span class="id" title="notation">Grp</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#05034b80a22270f72f61c5366c67d457"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#05034b80a22270f72f61c5366c67d457"><span class="id" title="notation">homg</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#05034b80a22270f72f61c5366c67d457"><span class="id" title="notation">Grp</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#p"><span class="id" title="variable">p</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="isoGrp_hom"><span class="id" title="lemma">isoGrp_hom</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.fingroup.presentation.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">p</span> : <a class="idref" href="mathcomp.fingroup.presentation.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#2033817e0a446c02fb5fa9a7fdad6117"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#2033817e0a446c02fb5fa9a7fdad6117"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#2033817e0a446c02fb5fa9a7fdad6117"><span class="id" title="notation">Grp</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#p"><span class="id" title="variable">p</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.presentation.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#7a9fb4aa00755e86dee5fc756da05fc2"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#7a9fb4aa00755e86dee5fc756da05fc2"><span class="id" title="notation">homg</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#7a9fb4aa00755e86dee5fc756da05fc2"><span class="id" title="notation">Grp</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#p"><span class="id" title="variable">p</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="isoGrpP"><span class="id" title="lemma">isoGrpP</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) <span class="id" title="var">p</span> <span class="id" title="var">rT</span> (<span class="id" title="var">H</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) :<br/> - <a class="idref" href="mathcomp.fingroup.presentation.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#19e0d8275b5f9ef645d1fd2c7dda9a9b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#19e0d8275b5f9ef645d1fd2c7dda9a9b"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#19e0d8275b5f9ef645d1fd2c7dda9a9b"><span class="id" title="notation">Grp</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#05034b80a22270f72f61c5366c67d457"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#05034b80a22270f72f61c5366c67d457"><span class="id" title="notation">homg</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#05034b80a22270f72f61c5366c67d457"><span class="id" title="notation">Grp</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#p"><span class="id" title="variable">p</span></a>) (<a class="idref" href="mathcomp.fingroup.presentation.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#G"><span class="id" title="variable">G</span></a>).<br/> +<span class="id" title="keyword">Lemma</span> <a name="isoGrpP"><span class="id" title="lemma">isoGrpP</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.fingroup.presentation.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">p</span> <span class="id" title="var">rT</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.fingroup.presentation.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) :<br/> + <a class="idref" href="mathcomp.fingroup.presentation.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#2033817e0a446c02fb5fa9a7fdad6117"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#2033817e0a446c02fb5fa9a7fdad6117"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#2033817e0a446c02fb5fa9a7fdad6117"><span class="id" title="notation">Grp</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#p"><span class="id" title="variable">p</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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#ba2b0e492d2b4675a0acf3ea92aabadd"><span class="id" title="notation">∧</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#7a9fb4aa00755e86dee5fc756da05fc2"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#7a9fb4aa00755e86dee5fc756da05fc2"><span class="id" title="notation">homg</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#7a9fb4aa00755e86dee5fc756da05fc2"><span class="id" title="notation">Grp</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#p"><span class="id" title="variable">p</span></a>) (<a class="idref" href="mathcomp.fingroup.presentation.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#13d63916ddaa339df3fcf04363ae7cde"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#G"><span class="id" title="variable">G</span></a>).<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="homGrp_trans"><span class="id" title="lemma">homGrp_trans</span></a> <span class="id" title="var">rT</span> <span class="id" title="var">gT</span> (<span class="id" title="var">H</span> : <a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) <span class="id" title="var">p</span> :<br/> - <a class="idref" href="mathcomp.fingroup.presentation.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#660be9f1a393f4f575133c9df42aec65"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#660be9f1a393f4f575133c9df42aec65"><span class="id" title="notation">homg</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#05034b80a22270f72f61c5366c67d457"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#05034b80a22270f72f61c5366c67d457"><span class="id" title="notation">homg</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#05034b80a22270f72f61c5366c67d457"><span class="id" title="notation">Grp</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#05034b80a22270f72f61c5366c67d457"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#05034b80a22270f72f61c5366c67d457"><span class="id" title="notation">homg</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#05034b80a22270f72f61c5366c67d457"><span class="id" title="notation">Grp</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#p"><span class="id" title="variable">p</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="homGrp_trans"><span class="id" title="lemma">homGrp_trans</span></a> <span class="id" title="var">rT</span> <span class="id" title="var">gT</span> (<span class="id" title="var">H</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.fingroup.presentation.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">G</span> : <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.fingroup.presentation.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">p</span> :<br/> + <a class="idref" href="mathcomp.fingroup.presentation.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#9899c777f5fa3790d4aad7f054b13e7e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#9899c777f5fa3790d4aad7f054b13e7e"><span class="id" title="notation">homg</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#7a9fb4aa00755e86dee5fc756da05fc2"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#7a9fb4aa00755e86dee5fc756da05fc2"><span class="id" title="notation">homg</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#7a9fb4aa00755e86dee5fc756da05fc2"><span class="id" title="notation">Grp</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#p"><span class="id" title="variable">p</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.presentation.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#7a9fb4aa00755e86dee5fc756da05fc2"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#7a9fb4aa00755e86dee5fc756da05fc2"><span class="id" title="notation">homg</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#7a9fb4aa00755e86dee5fc756da05fc2"><span class="id" title="notation">Grp</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#p"><span class="id" title="variable">p</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="eq_homGrp"><span class="id" title="lemma">eq_homGrp</span></a> <span class="id" title="var">gT</span> <span class="id" title="var">rT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">H</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) <span class="id" title="var">p</span> :<br/> - <a class="idref" href="mathcomp.fingroup.presentation.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#05034b80a22270f72f61c5366c67d457"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#05034b80a22270f72f61c5366c67d457"><span class="id" title="notation">homg</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#05034b80a22270f72f61c5366c67d457"><span class="id" title="notation">Grp</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#05034b80a22270f72f61c5366c67d457"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#05034b80a22270f72f61c5366c67d457"><span class="id" title="notation">homg</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#05034b80a22270f72f61c5366c67d457"><span class="id" title="notation">Grp</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="eq_homGrp"><span class="id" title="lemma">eq_homGrp</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.fingroup.presentation.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">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.fingroup.presentation.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>) <span class="id" title="var">p</span> :<br/> + <a class="idref" href="mathcomp.fingroup.presentation.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.fingroup.presentation.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#7a9fb4aa00755e86dee5fc756da05fc2"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#7a9fb4aa00755e86dee5fc756da05fc2"><span class="id" title="notation">homg</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#7a9fb4aa00755e86dee5fc756da05fc2"><span class="id" title="notation">Grp</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#p"><span class="id" title="variable">p</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="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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#7a9fb4aa00755e86dee5fc756da05fc2"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#7a9fb4aa00755e86dee5fc756da05fc2"><span class="id" title="notation">homg</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#7a9fb4aa00755e86dee5fc756da05fc2"><span class="id" title="notation">Grp</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#p"><span class="id" title="variable">p</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>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="isoGrp_trans"><span class="id" title="lemma">isoGrp_trans</span></a> <span class="id" title="var">gT</span> <span class="id" title="var">rT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">H</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) <span class="id" title="var">p</span> :<br/> - <a class="idref" href="mathcomp.fingroup.presentation.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#cec6c3028572f2d4d267ecf02dc64058"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#19e0d8275b5f9ef645d1fd2c7dda9a9b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#19e0d8275b5f9ef645d1fd2c7dda9a9b"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#19e0d8275b5f9ef645d1fd2c7dda9a9b"><span class="id" title="notation">Grp</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#19e0d8275b5f9ef645d1fd2c7dda9a9b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#19e0d8275b5f9ef645d1fd2c7dda9a9b"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#19e0d8275b5f9ef645d1fd2c7dda9a9b"><span class="id" title="notation">Grp</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#p"><span class="id" title="variable">p</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="isoGrp_trans"><span class="id" title="lemma">isoGrp_trans</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.fingroup.presentation.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">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.fingroup.presentation.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>) <span class="id" title="var">p</span> :<br/> + <a class="idref" href="mathcomp.fingroup.presentation.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.fingroup.presentation.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#2033817e0a446c02fb5fa9a7fdad6117"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#2033817e0a446c02fb5fa9a7fdad6117"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#2033817e0a446c02fb5fa9a7fdad6117"><span class="id" title="notation">Grp</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#p"><span class="id" title="variable">p</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.presentation.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#2033817e0a446c02fb5fa9a7fdad6117"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#2033817e0a446c02fb5fa9a7fdad6117"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#2033817e0a446c02fb5fa9a7fdad6117"><span class="id" title="notation">Grp</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#p"><span class="id" title="variable">p</span></a>.<br/> <br/> -<span class="id" title="keyword">Lemma</span> <a name="intro_isoGrp"><span class="id" title="lemma">intro_isoGrp</span></a> <span class="id" title="var">gT</span> (<span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) <span class="id" title="var">p</span> :<br/> - <a class="idref" href="mathcomp.fingroup.presentation.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#05034b80a22270f72f61c5366c67d457"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#05034b80a22270f72f61c5366c67d457"><span class="id" title="notation">homg</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#05034b80a22270f72f61c5366c67d457"><span class="id" title="notation">Grp</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">(</span></a><span class="id" title="keyword">∀</span> <span class="id" title="var">rT</span> (<span class="id" title="var">H</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>), <a class="idref" href="mathcomp.fingroup.presentation.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#05034b80a22270f72f61c5366c67d457"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#05034b80a22270f72f61c5366c67d457"><span class="id" title="notation">homg</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#05034b80a22270f72f61c5366c67d457"><span class="id" title="notation">Grp</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#660be9f1a393f4f575133c9df42aec65"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#660be9f1a393f4f575133c9df42aec65"><span class="id" title="notation">homg</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.fingroup.presentation.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#19e0d8275b5f9ef645d1fd2c7dda9a9b"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#19e0d8275b5f9ef645d1fd2c7dda9a9b"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#19e0d8275b5f9ef645d1fd2c7dda9a9b"><span class="id" title="notation">Grp</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#p"><span class="id" title="variable">p</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="intro_isoGrp"><span class="id" title="lemma">intro_isoGrp</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.fingroup.presentation.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">p</span> :<br/> + <a class="idref" href="mathcomp.fingroup.presentation.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#7a9fb4aa00755e86dee5fc756da05fc2"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#7a9fb4aa00755e86dee5fc756da05fc2"><span class="id" title="notation">homg</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#7a9fb4aa00755e86dee5fc756da05fc2"><span class="id" title="notation">Grp</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#p"><span class="id" title="variable">p</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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">(</span></a><span class="id" title="keyword">∀</span> <span class="id" title="var">rT</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.fingroup.presentation.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>), <a class="idref" href="mathcomp.fingroup.presentation.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#7a9fb4aa00755e86dee5fc756da05fc2"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#7a9fb4aa00755e86dee5fc756da05fc2"><span class="id" title="notation">homg</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#7a9fb4aa00755e86dee5fc756da05fc2"><span class="id" title="notation">Grp</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#p"><span class="id" title="variable">p</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.presentation.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#9899c777f5fa3790d4aad7f054b13e7e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#9899c777f5fa3790d4aad7f054b13e7e"><span class="id" title="notation">homg</span></a> <a class="idref" href="mathcomp.fingroup.presentation.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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.fingroup.presentation.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#2033817e0a446c02fb5fa9a7fdad6117"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.presentation.html#2033817e0a446c02fb5fa9a7fdad6117"><span class="id" title="notation">isog</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#2033817e0a446c02fb5fa9a7fdad6117"><span class="id" title="notation">Grp</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#p"><span class="id" title="variable">p</span></a>.<br/> <br/> <span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.fingroup.presentation.html#PresentationTheory"><span class="id" title="section">PresentationTheory</span></a>.<br/> |