diff options
Diffstat (limited to 'docs/htmldoc/mathcomp.fingroup.presentation.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.fingroup.presentation.html | 291 |
1 files changed, 291 insertions, 0 deletions
diff --git a/docs/htmldoc/mathcomp.fingroup.presentation.html b/docs/htmldoc/mathcomp.fingroup.presentation.html new file mode 100644 index 0000000..319155d --- /dev/null +++ b/docs/htmldoc/mathcomp.fingroup.presentation.html @@ -0,0 +1,291 @@ +<!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/> +<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> + +<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/8.8.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.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#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/> + <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#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/> + +<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/> + +<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/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">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/> + +<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">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.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">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/> + +<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="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/> + +<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/> + (<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/> + (<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="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/> + +<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/> + +<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="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="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="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="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#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/> + +<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/> + +<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/> + +<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/> + +<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/> + +<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/> + +<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 |