diff options
Diffstat (limited to 'docs/htmldoc/mathcomp.fingroup.presentation.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.fingroup.presentation.html | 290 |
1 files changed, 0 insertions, 290 deletions
diff --git a/docs/htmldoc/mathcomp.fingroup.presentation.html b/docs/htmldoc/mathcomp.fingroup.presentation.html deleted file mode 100644 index 301b4f4..0000000 --- a/docs/htmldoc/mathcomp.fingroup.presentation.html +++ /dev/null @@ -1,290 +0,0 @@ -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" -"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> -<html xmlns="http://www.w3.org/1999/xhtml"> -<head> -<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> -<link href="coqdoc.css" rel="stylesheet" type="text/css" /> -<title>mathcomp.fingroup.presentation</title> -</head> - -<body> - -<div id="page"> - -<div id="header"> -</div> - -<div id="main"> - -<h1 class="libtitle">Library mathcomp.fingroup.presentation</h1> - -<div class="code"> -<span class="comment">(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. <br/> - Distributed under the terms of CeCILL-B. *)</span><br/> - -<br/> -</div> - -<div class="doc"> - Support for generator-and-relation presentations of groups. We provide the - syntax: - G \homg Grp (x_1 : ... x_n : (s_1 = t_1, ..., s_m = t_m)) - <=> G is generated by elements x_1, ..., x_m satisfying the relations - s_1 = t_1, ..., s_m = t_m, i.e., G is a homomorphic image of the - group generated by the x_i, subject to the relations s_j = t_j. - G \isog Grp (x_1 : ... x_n : (s_1 = t_1, ..., s_m = t_m)) - <=> G is isomorphic to the group generated by the x_i, subject to the - relations s_j = t_j. This is an intensional predicate (in Prop), as - even the non-triviality of a generated group is undecidable. - Syntax details: -<ul class="doclist"> -<li> Grp is a litteral constant. - -</li> -<li> There must be at least one generator and one relation. - -</li> -<li> A relation s_j = 1 can be abbreviated as simply s_j (a.k.a. a relator). - -</li> -<li> Two consecutive relations s_j = t, s_j+1 = t can be abbreviated - s_j = s_j+1 = t. - -</li> -<li> The s_j and t_j are terms built from the x_i and the standard group - operators *, 1, ^-1, ^+, ^-, ^, [~ u_1, ..., u_k]; no other operator or - abbreviation may be used, as the notation is implemented using static - overloading. - -</li> -<li> This is the closest we could get to the notation used in Aschbacher, - Grp (x_1, ... x_n : t_1,1 = ... = t_1,k1, ..., t_m,1 = ... = t_m,km) - under the current limitations of the Coq Notation facility. - -</li> -</ul> - Semantics details: -<ul class="doclist"> -<li> G \isog Grp (...) : Prop expands to the statement - forall rT (H : {group rT}), (H \homg G) = (H \homg Grp (...)) - (with rT : finGroupType). - -</li> -<li> G \homg Grp (x_1 : ... x_n : (s_1 = t_1, ..., s_m = t_m)) : bool, with - G : {set gT}, is convertible to the boolean expression - [exists t : gT * ... gT, let: (x_1, ..., x_n) := t in - (< [x_1]> <*> ... <*> < [x_n]>, (s_1, ... (s_m-1, s_m) ...)) - == (G, (t_1, ... (t_m-1, t_m) ...)) ] - where the tuple comparison above is convertible to the conjunction - [&& < [x_1]> <*> ... <*> < [x_n]> == G, s_1 == t_1, ... & s_m == t_m] - Thus G \homg Grp (...) can be easily exploited by destructing the tuple - created case/existsP, then destructing the tuple equality with case/eqP. - Conversely it can be proved by using apply/existsP, providing the tuple - with a single exists (u_1, ..., u_n), then using rewrite !xpair_eqE /= - to expose the conjunction, and optionally using an apply/and{m+1}P view - to split it into subgoals (in that case, the rewrite is in principle - redundant, but necessary in practice because of the poor performance of - conversion in the Coq unifier). -</li> -</ul> - -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Set Implicit Arguments</span>.<br/> - -<br/> -<span class="id" title="keyword">Import</span> <span class="id" title="var">GroupScope</span>.<br/> - -<br/> -<span class="id" title="keyword">Module</span> <a name="Presentation"><span class="id" title="module">Presentation</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="Presentation.Presentation"><span class="id" title="section">Presentation</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">gT</span> <span class="id" title="var">rT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>.<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Type</span> <span class="id" title="var">vT</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>. <span class="comment">(* tuple value type *)</span><br/> - -<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/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/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/> - -<br/> -<span class="id" title="keyword">Fixpoint</span> <a name="Presentation.eval"><span class="id" title="definition">eval</span></a> {<span class="id" title="var">gT</span>} <span class="id" title="var">e</span> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.fingroup.presentation.html#gT"><span class="id" title="variable">gT</span></a> :=<br/> - <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#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/> -<span class="id" title="keyword">Inductive</span> <a name="Presentation.formula"><span class="id" title="inductive">formula</span></a> := <a name="Presentation.Eq2"><span class="id" title="constructor">Eq2</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="mathcomp.fingroup.presentation.html#Presentation.term"><span class="id" title="inductive">term</span></a> | <a name="Presentation.And"><span class="id" title="constructor">And</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.fingroup.presentation.html#formula"><span class="id" title="inductive">formula</span></a> & <a class="idref" href="mathcomp.fingroup.presentation.html#formula"><span class="id" title="inductive">formula</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="Presentation.Eq1"><span class="id" title="definition">Eq1</span></a> <span class="id" title="var">s</span> := <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Eq2"><span class="id" title="constructor">Eq2</span></a> <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#Presentation.Idx"><span class="id" title="constructor">Idx</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="Presentation.Eq3"><span class="id" title="definition">Eq3</span></a> <span class="id" title="var">s1</span> <span class="id" title="var">s2</span> <span class="id" title="var">t</span> := <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.And"><span class="id" title="constructor">And</span></a> (<a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Eq2"><span class="id" title="constructor">Eq2</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#s1"><span class="id" title="variable">s1</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#t"><span class="id" title="variable">t</span></a>) (<a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Eq2"><span class="id" title="constructor">Eq2</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#s2"><span class="id" title="variable">s2</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#t"><span class="id" title="variable">t</span></a>).<br/> - -<br/> -<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#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/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/> - <span class="id" title="keyword">match</span> <a class="idref" href="mathcomp.fingroup.presentation.html#f"><span class="id" title="variable">f</span></a> <span class="id" title="keyword">with</span><br/> - | <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.Eq2"><span class="id" title="constructor">Eq2</span></a> <span class="id" title="var">s</span> <span class="id" title="var">t</span> ⇒ <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.and_rel"><span class="id" title="definition">and_rel</span></a> (<a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.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">s</span>) (<a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.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">t</span>) <a class="idref" href="mathcomp.fingroup.presentation.html#r"><span class="id" title="variable">r</span></a><br/> - | <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation.And"><span class="id" title="constructor">And</span></a> <span class="id" title="var">f1</span> <span class="id" title="var">f2</span> ⇒ <a class="idref" href="mathcomp.fingroup.presentation.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="var">f1</span> (<a class="idref" href="mathcomp.fingroup.presentation.html#rel"><span class="id" title="definition">rel</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#e"><span class="id" title="variable">e</span></a> <span class="id" title="var">f2</span> <a class="idref" href="mathcomp.fingroup.presentation.html#r"><span class="id" title="variable">r</span></a>)<br/> - <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/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#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/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#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/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#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/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.fingroup.presentation.html#Presentation"><span class="id" title="module">Presentation</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Import</span> <span class="id" title="var">Presentation</span>.<br/> - -<br/> -<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.fingroup.presentation.html#bool_of_rel"><span class="id" title="definition">bool_of_rel</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#bool_of_rel"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#bool_of_rel"><span class="id" title="definition">rel_type</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#bool_of_rel"><span class="id" title="definition">>-></span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#bool_of_rel"><span class="id" title="definition">bool</span></a>.<br/> -<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.fingroup.presentation.html#Eq1"><span class="id" title="definition">Eq1</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#Eq1"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#Eq1"><span class="id" title="definition">term</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#Eq1"><span class="id" title="definition">>-></span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#Eq1"><span class="id" title="definition">formula</span></a>.<br/> -<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.fingroup.presentation.html#Formula"><span class="id" title="constructor">Formula</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#Formula"><span class="id" title="constructor">:</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#Formula"><span class="id" title="constructor">formula</span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#Formula"><span class="id" title="constructor">>-></span></a> <a class="idref" href="mathcomp.fingroup.presentation.html#Formula"><span class="id" title="constructor">type</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - Declare (implicitly) the argument scope tags. -</div> -<div class="code"> -<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="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="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/> -</div> - -<div class="doc"> - Declare (implicitly) the argument scope tags. -</div> -<div class="code"> -<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="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="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="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="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="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/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="PresentationTheory"><span class="id" title="section">PresentationTheory</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">gT</span> <span class="id" title="var">rT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>.<br/> - -<br/> -<span class="id" title="keyword">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#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#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#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#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#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#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/> - -<br/> -</div> -</div> - -<div id="footer"> -<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a> -</div> - -</div> - -</body> -</html>
\ No newline at end of file |