diff options
| author | Cyril Cohen | 2019-10-16 11:26:43 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2019-10-16 11:26:43 +0200 |
| commit | 6b59540a2460633df4e3d8347cb4dfe2fb3a3afb (patch) | |
| tree | 1239c1d5553d51a7d73f2f8b465f6a23178ff8a0 /docs/htmldoc/mathcomp.fingroup.automorphism.html | |
| parent | dd82aaeae7e9478efc178ce8430986649555b032 (diff) | |
removing everything but index which redirects to the new page
Diffstat (limited to 'docs/htmldoc/mathcomp.fingroup.automorphism.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.fingroup.automorphism.html | 490 |
1 files changed, 0 insertions, 490 deletions
diff --git a/docs/htmldoc/mathcomp.fingroup.automorphism.html b/docs/htmldoc/mathcomp.fingroup.automorphism.html deleted file mode 100644 index bac4533..0000000 --- a/docs/htmldoc/mathcomp.fingroup.automorphism.html +++ /dev/null @@ -1,490 +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.automorphism</title> -</head> - -<body> - -<div id="page"> - -<div id="header"> -</div> - -<div id="main"> - -<h1 class="libtitle">Library mathcomp.fingroup.automorphism</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"> - Group automorphisms and characteristic subgroups. - Unlike morphisms on a group G, which are functions of type gT -> rT, with - a canonical structure of dependent type {morphim G >-> rT}, automorphisms - are permutations of type {perm gT} contained in Aut G : {set {perm gT}}. - This lets us use the finGroupType of {perm gT}. Note also that while - morphisms on G are undefined outside G, automorphisms have their support - in G, i.e., they are the identity outside G. - Definitions: - Aut G (or [Aut G]) == the automorphism group of G. - [Aut G]%G == the group structure for Aut G. - autm AutGa == the morphism on G induced by a, given - AutGa : a \in Aut G. - perm_in injf fA == the permutation with support B in induced by f, - given injf : {in A &, injective f} and - fA : f @: A \subset A. - aut injf fG == the automorphism of G induced by the morphism f, - given injf : 'injm f and fG : f @* G \subset G. - Aut_isom injf sDom == the injective homomorphism that maps Aut G to - Aut (f @* G), with f : {morphism D >-> rT} and - given injf: 'injm f and sDom : G \subset D. - conjgm G == the conjugation automorphism on G. - H \char G == H is a characteristic subgroup of G. -</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/> -</div> - -<div class="doc"> - A group automorphism, defined as a permutation on a subset of a - finGroupType that respects the morphism law. - Here perm_on is used as a closure rule for the set A. -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Section</span> <a name="Automorphism"><span class="id" title="section">Automorphism</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="Automorphism.gT"><span class="id" title="variable">gT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>.<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Type</span> <span class="id" title="var">A</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.automorphism.html#Automorphism.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>.<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span> : <a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#Automorphism.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="Aut"><span class="id" title="definition">Aut</span></a> <span class="id" title="var">A</span> := <a class="idref" href="mathcomp.ssreflect.finset.html#4e173ac66c4bfb69f9f0316bf3f59a43"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#4e173ac66c4bfb69f9f0316bf3f59a43"><span class="id" title="notation">set</span></a> <span class="id" title="var">a</span> <a class="idref" href="mathcomp.ssreflect.finset.html#4e173ac66c4bfb69f9f0316bf3f59a43"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_on"><span class="id" title="definition">perm_on</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#4e173ac66c4bfb69f9f0316bf3f59a43"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#morphic"><span class="id" title="definition">morphic</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#4e173ac66c4bfb69f9f0316bf3f59a43"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Aut_morphic"><span class="id" title="lemma">Aut_morphic</span></a> <span class="id" title="var">A</span> <span class="id" title="var">a</span> : <a class="idref" href="mathcomp.fingroup.automorphism.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#morphic"><span class="id" title="definition">morphic</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#a"><span class="id" title="variable">a</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="out_Aut"><span class="id" title="lemma">out_Aut</span></a> <span class="id" title="var">A</span> <span class="id" title="var">a</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.fingroup.automorphism.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#c1ad6bcc76a6221225111f87bc3b0c3d"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#c1ad6bcc76a6221225111f87bc3b0c3d"><span class="id" title="notation">notin</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#x"><span class="id" title="variable">x</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.automorphism.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="eq_Aut"><span class="id" title="lemma">eq_Aut</span></a> <span class="id" title="var">A</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">&,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span>, <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#b"><span class="id" title="variable">b</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#b"><span class="id" title="variable">b</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - The morphism that is represented by a given element of Aut A. -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="autm"><span class="id" title="definition">autm</span></a> <span class="id" title="var">A</span> <span class="id" title="var">a</span> (<span class="id" title="var">AutAa</span> : <a class="idref" href="mathcomp.fingroup.automorphism.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a>) := <a class="idref" href="mathcomp.fingroup.morphism.html#morphm"><span class="id" title="definition">morphm</span></a> (<a class="idref" href="mathcomp.fingroup.automorphism.html#Aut_morphic"><span class="id" title="lemma">Aut_morphic</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#AutAa"><span class="id" title="variable">AutAa</span></a>).<br/> -<span class="id" title="keyword">Lemma</span> <a name="autmE"><span class="id" title="lemma">autmE</span></a> <span class="id" title="var">A</span> <span class="id" title="var">a</span> (<span class="id" title="var">AutAa</span> : <a class="idref" href="mathcomp.fingroup.automorphism.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a>) : <a class="idref" href="mathcomp.fingroup.automorphism.html#autm"><span class="id" title="definition">autm</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#AutAa"><span class="id" title="variable">AutAa</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.automorphism.html#a"><span class="id" title="variable">a</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">autm_morphism</span> <span class="id" title="var">A</span> <span class="id" title="var">a</span> <span class="id" title="var">aM</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.fingroup.morphism.html#d22b43813ec744a6a8786f15c9267991"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#d22b43813ec744a6a8786f15c9267991"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#d22b43813ec744a6a8786f15c9267991"><span class="id" title="notation">of</span></a> @<a class="idref" href="mathcomp.fingroup.automorphism.html#autm"><span class="id" title="definition">autm</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#aM"><span class="id" title="variable">aM</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#d22b43813ec744a6a8786f15c9267991"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="Automorphism.AutGroup"><span class="id" title="section">AutGroup</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="Automorphism.AutGroup.G"><span class="id" title="variable">G</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#Automorphism.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Aut_group_set"><span class="id" title="lemma">Aut_group_set</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#group_set"><span class="id" title="definition">group_set</span></a> (<a class="idref" href="mathcomp.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#Automorphism.AutGroup.G"><span class="id" title="variable">G</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Aut_group</span> := <a class="idref" href="mathcomp.fingroup.fingroup.html#group"><span class="id" title="definition">group</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#Aut_group_set"><span class="id" title="lemma">Aut_group_set</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> (<a name="Automorphism.AutGroup.a"><span class="id" title="variable">a</span></a> : <a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#Automorphism.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">}</span></a>) (<a name="Automorphism.AutGroup.AutGa"><span class="id" title="variable">AutGa</span></a> : <a class="idref" href="mathcomp.fingroup.automorphism.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#Automorphism.AutGroup.G"><span class="id" title="variable">G</span></a>).<br/> -<span class="id" title="keyword">Notation</span> <a name="f"><span class="id" title="abbreviation">f</span></a> := (<a class="idref" href="mathcomp.fingroup.automorphism.html#autm"><span class="id" title="definition">autm</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#Automorphism.AutGroup.AutGa"><span class="id" title="variable">AutGa</span></a>).<br/> -<span class="id" title="keyword">Notation</span> <a name="fE"><span class="id" title="abbreviation">fE</span></a> := (<a class="idref" href="mathcomp.fingroup.automorphism.html#autmE"><span class="id" title="lemma">autmE</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#Automorphism.AutGroup.AutGa"><span class="id" title="variable">AutGa</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="injm_autm"><span class="id" title="lemma">injm_autm</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#f"><span class="id" title="abbreviation">f</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="ker_autm"><span class="id" title="lemma">ker_autm</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#7ef99623452370540bbc44fd30b0bc94"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#7ef99623452370540bbc44fd30b0bc94"><span class="id" title="notation">ker</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#f"><span class="id" title="abbreviation">f</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> 1. <br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="im_autm"><span class="id" title="lemma">im_autm</span></a> : <a class="idref" href="mathcomp.fingroup.automorphism.html#f"><span class="id" title="abbreviation">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#Automorphism.AutGroup.G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#Automorphism.AutGroup.G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Aut_closed"><span class="id" title="lemma">Aut_closed</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.fingroup.automorphism.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#Automorphism.AutGroup.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.automorphism.html#Automorphism.AutGroup.a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#Automorphism.AutGroup.G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.fingroup.automorphism.html#Automorphism.AutGroup"><span class="id" title="section">AutGroup</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Aut1"><span class="id" title="lemma">Aut1</span></a> : <a class="idref" href="mathcomp.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 1.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.fingroup.automorphism.html#Automorphism"><span class="id" title="section">Automorphism</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="189678f8b01b373bc45cd1d222c1dab5"><span class="id" title="notation">"</span></a>[ 'Aut' G ]" := (<a class="idref" href="mathcomp.fingroup.automorphism.html#Aut_group"><span class="id" title="definition">Aut_group</span></a> <span class="id" title="var">G</span>)<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'Aut' G ]") : <span class="id" title="var">Group_scope</span>.<br/> -<span class="id" title="keyword">Notation</span> <a name="efd715eb30d6f7a29549acd8406ebac4"><span class="id" title="notation">"</span></a>[ 'Aut' G ]" := (<a class="idref" href="mathcomp.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <span class="id" title="var">G</span>)<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">only</span> <span class="id" title="var">parsing</span>) : <span class="id" title="var">group_scope</span>.<br/> - -<br/> - -<br/> -</div> - -<div class="doc"> - The permutation function (total on the underlying groupType) that is the - representant of a given morphism f with domain A in (Aut A). -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Section</span> <a name="PermIn"><span class="id" title="section">PermIn</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="PermIn.T"><span class="id" title="variable">T</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) (<a name="PermIn.A"><span class="id" title="variable">A</span></a> : <a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>) (<a name="PermIn.f"><span class="id" title="variable">f</span></a> : <a class="idref" href="mathcomp.fingroup.automorphism.html#T"><span class="id" title="variable">T</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.automorphism.html#T"><span class="id" title="variable">T</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Hypotheses</span> (<a name="PermIn.injf"><span class="id" title="variable">injf</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#PermIn.A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">&,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#injective"><span class="id" title="definition">injective</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#PermIn.f"><span class="id" title="variable">f</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">}</span></a>) (<a name="PermIn.sBf"><span class="id" title="variable">sBf</span></a> : <a class="idref" href="mathcomp.fingroup.automorphism.html#PermIn.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#de2c3fcab69008133cce8f8fc06f2b4b"><span class="id" title="notation">@:</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#PermIn.A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#PermIn.A"><span class="id" title="variable">A</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="perm_in_inj"><span class="id" title="lemma">perm_in_inj</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#injective"><span class="id" title="definition">injective</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#00a1a5b58aac8f1e3f1abff064a39f9d"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#PermIn.A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#00a1a5b58aac8f1e3f1abff064a39f9d"><span class="id" title="notation">then</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#PermIn.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#00a1a5b58aac8f1e3f1abff064a39f9d"><span class="id" title="notation">else</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#x"><span class="id" title="variable">x</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="perm_in"><span class="id" title="definition">perm_in</span></a> := <a class="idref" href="mathcomp.fingroup.perm.html#perm"><span class="id" title="abbreviation">perm</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#perm_in_inj"><span class="id" title="lemma">perm_in_inj</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="perm_in_on"><span class="id" title="lemma">perm_in_on</span></a> : <a class="idref" href="mathcomp.fingroup.perm.html#perm_on"><span class="id" title="definition">perm_on</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#PermIn.A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#perm_in"><span class="id" title="definition">perm_in</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="perm_inE"><span class="id" title="lemma">perm_inE</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#PermIn.A"><span class="id" title="variable">A</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#perm_in"><span class="id" title="definition">perm_in</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#PermIn.f"><span class="id" title="variable">f</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.fingroup.automorphism.html#PermIn"><span class="id" title="section">PermIn</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - properties of injective endomorphisms -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Section</span> <a name="MakeAut"><span class="id" title="section">MakeAut</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="MakeAut.gT"><span class="id" title="variable">gT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<a name="MakeAut.G"><span class="id" title="variable">G</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) (<a name="MakeAut.f"><span class="id" title="variable">f</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">}</span></a>).<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Type</span> <span class="id" title="var">A</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.automorphism.html#MakeAut.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Hypothesis</span> <a name="MakeAut.injf"><span class="id" title="variable">injf</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#MakeAut.f"><span class="id" title="variable">f</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="morphim_fixP"><span class="id" title="lemma">morphim_fixP</span></a> <span class="id" title="var">A</span> : <a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#MakeAut.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.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="mathcomp.fingroup.automorphism.html#MakeAut.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a>) (<a class="idref" href="mathcomp.fingroup.automorphism.html#MakeAut.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Hypothesis</span> <a name="MakeAut.Gf"><span class="id" title="variable">Gf</span></a> : <a class="idref" href="mathcomp.fingroup.automorphism.html#MakeAut.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#MakeAut.G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#MakeAut.G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="aut_closed"><span class="id" title="lemma">aut_closed</span></a> : <a class="idref" href="mathcomp.fingroup.automorphism.html#MakeAut.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#de2c3fcab69008133cce8f8fc06f2b4b"><span class="id" title="notation">@:</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#MakeAut.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#MakeAut.G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="aut"><span class="id" title="definition">aut</span></a> := <a class="idref" href="mathcomp.fingroup.automorphism.html#perm_in"><span class="id" title="definition">perm_in</span></a> (<a class="idref" href="mathcomp.fingroup.morphism.html#injmP"><span class="id" title="lemma">injmP</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#MakeAut.injf"><span class="id" title="variable">injf</span></a>) <a class="idref" href="mathcomp.fingroup.automorphism.html#aut_closed"><span class="id" title="lemma">aut_closed</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="autE"><span class="id" title="lemma">autE</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#MakeAut.G"><span class="id" title="variable">G</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#aut"><span class="id" title="definition">aut</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#MakeAut.f"><span class="id" title="variable">f</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="morphic_aut"><span class="id" title="lemma">morphic_aut</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#morphic"><span class="id" title="definition">morphic</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#MakeAut.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#aut"><span class="id" title="definition">aut</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Aut_aut"><span class="id" title="lemma">Aut_aut</span></a> : <a class="idref" href="mathcomp.fingroup.automorphism.html#aut"><span class="id" title="definition">aut</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#MakeAut.G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="imset_autE"><span class="id" title="lemma">imset_autE</span></a> <span class="id" title="var">A</span> : <a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#MakeAut.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.automorphism.html#aut"><span class="id" title="definition">aut</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#de2c3fcab69008133cce8f8fc06f2b4b"><span class="id" title="notation">@:</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#MakeAut.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="preim_autE"><span class="id" title="lemma">preim_autE</span></a> <span class="id" title="var">A</span> : <a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#MakeAut.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.automorphism.html#aut"><span class="id" title="definition">aut</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#a26e64199ff8828f9b3d592a35c487af"><span class="id" title="notation">@^-1:</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#MakeAut.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#320f70d30c9a649ec82642b364681418"><span class="id" title="notation">@*^-1</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.fingroup.automorphism.html#MakeAut"><span class="id" title="section">MakeAut</span></a>.<br/> - -<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="AutIsom"><span class="id" title="section">AutIsom</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="AutIsom.gT"><span class="id" title="variable">gT</span></a> <a name="AutIsom.rT"><span class="id" title="variable">rT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<a name="AutIsom.G"><span class="id" title="variable">G</span></a> <a name="AutIsom.D"><span class="id" title="variable">D</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) (<a name="AutIsom.f"><span class="id" title="variable">f</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">}</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Hypotheses</span> (<a name="AutIsom.injf"><span class="id" title="variable">injf</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#AutIsom.f"><span class="id" title="variable">f</span></a>) (<a name="AutIsom.sGD"><span class="id" title="variable">sGD</span></a> : <a class="idref" href="mathcomp.fingroup.automorphism.html#AutIsom.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#AutIsom.D"><span class="id" title="variable">D</span></a>).<br/> -<span class="id" title="keyword">Let</span> <a name="AutIsom.domG"><span class="id" title="variable">domG</span></a> := <a class="idref" href="mathcomp.ssreflect.fintype.html#subsetP"><span class="id" title="lemma">subsetP</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#AutIsom.sGD"><span class="id" title="variable">sGD</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Aut_isom_subproof"><span class="id" title="lemma">Aut_isom_subproof</span></a> <span class="id" title="var">a</span> :<br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#c0bbd202248f4def7aaf0c316cf2c29e"><span class="id" title="notation">{</span></a><span class="id" title="var">a'</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#c0bbd202248f4def7aaf0c316cf2c29e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#a'"><span class="id" title="variable">a'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> (<a class="idref" href="mathcomp.fingroup.automorphism.html#AutIsom.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#AutIsom.G"><span class="id" title="variable">G</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#c0bbd202248f4def7aaf0c316cf2c29e"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#AutIsom.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.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#AutIsom.G"><span class="id" title="variable">G</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#a'"><span class="id" title="variable">a'</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8b4742e3f67816503ce4ab2f3b81c27e"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8b4742e3f67816503ce4ab2f3b81c27e"><span class="id" title="notation">o</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#AutIsom.f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#876aa133fb3472bffd492f74ff496035"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#AutIsom.f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8b4742e3f67816503ce4ab2f3b81c27e"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#8b4742e3f67816503ce4ab2f3b81c27e"><span class="id" title="notation">o</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#c0bbd202248f4def7aaf0c316cf2c29e"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="Aut_isom"><span class="id" title="definition">Aut_isom</span></a> <span class="id" title="var">a</span> := <a class="idref" href="mathcomp.ssreflect.eqtype.html#s2val"><span class="id" title="definition">s2val</span></a> (<a class="idref" href="mathcomp.fingroup.automorphism.html#Aut_isom_subproof"><span class="id" title="lemma">Aut_isom_subproof</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#a"><span class="id" title="variable">a</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Aut_Aut_isom"><span class="id" title="lemma">Aut_Aut_isom</span></a> <span class="id" title="var">a</span> : <a class="idref" href="mathcomp.fingroup.automorphism.html#Aut_isom"><span class="id" title="definition">Aut_isom</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> (<a class="idref" href="mathcomp.fingroup.automorphism.html#AutIsom.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#AutIsom.G"><span class="id" title="variable">G</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Aut_isomE"><span class="id" title="lemma">Aut_isomE</span></a> <span class="id" title="var">a</span> : <a class="idref" href="mathcomp.fingroup.automorphism.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#AutIsom.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.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#AutIsom.G"><span class="id" title="variable">G</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.fingroup.automorphism.html#Aut_isom"><span class="id" title="definition">Aut_isom</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#a"><span class="id" title="variable">a</span></a> (<a class="idref" href="mathcomp.fingroup.automorphism.html#AutIsom.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#x"><span class="id" title="variable">x</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.automorphism.html#AutIsom.f"><span class="id" title="variable">f</span></a> (<a class="idref" href="mathcomp.fingroup.automorphism.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#x"><span class="id" title="variable">x</span></a>)<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Aut_isomM"><span class="id" title="lemma">Aut_isomM</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#AutIsom.G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">&,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#Aut_isom"><span class="id" title="definition">Aut_isom</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#8b8794efbfbae1b793d9cb62ce802285"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">}</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">Aut_isom_morphism</span> := <a class="idref" href="mathcomp.fingroup.morphism.html#Morphism"><span class="id" title="constructor">Morphism</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#Aut_isomM"><span class="id" title="lemma">Aut_isomM</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="injm_Aut_isom"><span class="id" title="lemma">injm_Aut_isom</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#Aut_isom"><span class="id" title="definition">Aut_isom</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.fingroup.automorphism.html#AutIsom"><span class="id" title="section">AutIsom</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="InjmAut"><span class="id" title="section">InjmAut</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="InjmAut.gT"><span class="id" title="variable">gT</span></a> <a name="InjmAut.rT"><span class="id" title="variable">rT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<a name="InjmAut.G"><span class="id" title="variable">G</span></a> <a name="InjmAut.D"><span class="id" title="variable">D</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) (<a name="InjmAut.f"><span class="id" title="variable">f</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">}</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Hypotheses</span> (<a name="InjmAut.injf"><span class="id" title="variable">injf</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#InjmAut.f"><span class="id" title="variable">f</span></a>) (<a name="InjmAut.sGD"><span class="id" title="variable">sGD</span></a> : <a class="idref" href="mathcomp.fingroup.automorphism.html#InjmAut.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#InjmAut.D"><span class="id" title="variable">D</span></a>).<br/> -<span class="id" title="keyword">Let</span> <a name="InjmAut.domG"><span class="id" title="variable">domG</span></a> := <a class="idref" href="mathcomp.ssreflect.fintype.html#subsetP"><span class="id" title="lemma">subsetP</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#InjmAut.sGD"><span class="id" title="variable">sGD</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="im_Aut_isom"><span class="id" title="lemma">im_Aut_isom</span></a> : <a class="idref" href="mathcomp.fingroup.automorphism.html#Aut_isom"><span class="id" title="definition">Aut_isom</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#InjmAut.injf"><span class="id" title="variable">injf</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#InjmAut.sGD"><span class="id" title="variable">sGD</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#InjmAut.G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> (<a class="idref" href="mathcomp.fingroup.automorphism.html#InjmAut.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#InjmAut.G"><span class="id" title="variable">G</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Aut_isomP"><span class="id" title="lemma">Aut_isomP</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#isom"><span class="id" title="definition">isom</span></a> (<a class="idref" href="mathcomp.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#InjmAut.G"><span class="id" title="variable">G</span></a>) (<a class="idref" href="mathcomp.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> (<a class="idref" href="mathcomp.fingroup.automorphism.html#InjmAut.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#InjmAut.G"><span class="id" title="variable">G</span></a>)) (<a class="idref" href="mathcomp.fingroup.automorphism.html#Aut_isom"><span class="id" title="definition">Aut_isom</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#InjmAut.injf"><span class="id" title="variable">injf</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#InjmAut.sGD"><span class="id" title="variable">sGD</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="injm_Aut"><span class="id" title="lemma">injm_Aut</span></a> : <a class="idref" href="mathcomp.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> (<a class="idref" href="mathcomp.fingroup.automorphism.html#InjmAut.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#InjmAut.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.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#InjmAut.G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.fingroup.automorphism.html#InjmAut"><span class="id" title="section">InjmAut</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - conjugation automorphism -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Section</span> <a name="ConjugationMorphism"><span class="id" title="section">ConjugationMorphism</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="ConjugationMorphism.gT"><span class="id" title="variable">gT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>.<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Type</span> <span class="id" title="var">A</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.automorphism.html#ConjugationMorphism.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="conjgm"><span class="id" title="definition">conjgm</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.automorphism.html#ConjugationMorphism.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="keyword">fun</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.fingroup.automorphism.html#ConjugationMorphism.gT"><span class="id" title="variable">gT</span></a> ⇒ <a class="idref" href="mathcomp.fingroup.automorphism.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#746f7e4d3218aa2699eefc064b513fc2"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="conjgmE"><span class="id" title="lemma">conjgmE</span></a> <span class="id" title="var">A</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.fingroup.automorphism.html#conjgm"><span class="id" title="definition">conjgm</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#y"><span class="id" title="variable">y</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.automorphism.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#746f7e4d3218aa2699eefc064b513fc2"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#x"><span class="id" title="variable">x</span></a>. <br/> - -<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">conjgm_morphism</span> <span class="id" title="var">A</span> <span class="id" title="var">x</span> :=<br/> - @<a class="idref" href="mathcomp.fingroup.morphism.html#Morphism"><span class="id" title="constructor">Morphism</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a> (<a class="idref" href="mathcomp.fingroup.automorphism.html#conjgm"><span class="id" title="definition">conjgm</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#in2W"><span class="id" title="lemma">in2W</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span> ⇒ <a class="idref" href="mathcomp.fingroup.fingroup.html#conjMg"><span class="id" title="lemma">conjMg</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#x"><span class="id" title="variable">x</span></a>)).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="morphim_conj"><span class="id" title="lemma">morphim_conj</span></a> <span class="id" title="var">A</span> <span class="id" title="var">x</span> <span class="id" title="var">B</span> : <a class="idref" href="mathcomp.fingroup.automorphism.html#conjgm"><span class="id" title="definition">conjgm</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.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="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#b9596739b058766532fc6517a36fef9f"><span class="id" title="notation">:&:</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="ConjugationMorphism.G"><span class="id" title="variable">G</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#ConjugationMorphism.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="injm_conj"><span class="id" title="lemma">injm_conj</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#conjgm"><span class="id" title="definition">conjgm</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#ConjugationMorphism.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">)</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="conj_isom"><span class="id" title="lemma">conj_isom</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.fingroup.morphism.html#isom"><span class="id" title="definition">isom</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#ConjugationMorphism.G"><span class="id" title="variable">G</span></a> (<a class="idref" href="mathcomp.fingroup.automorphism.html#ConjugationMorphism.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.fingroup.automorphism.html#conjgm"><span class="id" title="definition">conjgm</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#ConjugationMorphism.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#x"><span class="id" title="variable">x</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="conj_isog"><span class="id" title="lemma">conj_isog</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.fingroup.automorphism.html#ConjugationMorphism.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.automorphism.html#ConjugationMorphism.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="norm_conjg_im"><span class="id" title="lemma">norm_conjg_im</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.fingroup.automorphism.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#ConjugationMorphism.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#conjgm"><span class="id" title="definition">conjgm</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#ConjugationMorphism.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#ConjugationMorphism.G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#ConjugationMorphism.G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="norm_conj_isom"><span class="id" title="lemma">norm_conj_isom</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.fingroup.automorphism.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#ConjugationMorphism.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#isom"><span class="id" title="definition">isom</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#ConjugationMorphism.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#ConjugationMorphism.G"><span class="id" title="variable">G</span></a> (<a class="idref" href="mathcomp.fingroup.automorphism.html#conjgm"><span class="id" title="definition">conjgm</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#ConjugationMorphism.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#x"><span class="id" title="variable">x</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="conj_aut"><span class="id" title="definition">conj_aut</span></a> <span class="id" title="var">x</span> := <a class="idref" href="mathcomp.fingroup.automorphism.html#aut"><span class="id" title="definition">aut</span></a> (<a class="idref" href="mathcomp.fingroup.automorphism.html#injm_conj"><span class="id" title="lemma">injm_conj</span></a> <span class="id" title="var">_</span>) (<a class="idref" href="mathcomp.fingroup.automorphism.html#norm_conjg_im"><span class="id" title="lemma">norm_conjg_im</span></a> (<a class="idref" href="mathcomp.fingroup.fingroup.html#subgP"><span class="id" title="lemma">subgP</span></a> (<a class="idref" href="mathcomp.fingroup.fingroup.html#subg"><span class="id" title="definition">subg</span></a> <span class="id" title="var">_</span> <a class="idref" href="mathcomp.fingroup.automorphism.html#x"><span class="id" title="variable">x</span></a>))).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="norm_conj_autE"><span class="id" title="lemma">norm_conj_autE</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5f76d9959f82823e4253cd67e7dc0e96"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5f76d9959f82823e4253cd67e7dc0e96"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#ConjugationMorphism.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5f76d9959f82823e4253cd67e7dc0e96"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#ConjugationMorphism.G"><span class="id" title="variable">G</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5f76d9959f82823e4253cd67e7dc0e96"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>, <a class="idref" href="mathcomp.fingroup.automorphism.html#conj_aut"><span class="id" title="definition">conj_aut</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#y"><span class="id" title="variable">y</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.automorphism.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#746f7e4d3218aa2699eefc064b513fc2"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5f76d9959f82823e4253cd67e7dc0e96"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="conj_autE"><span class="id" title="lemma">conj_autE</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#ConjugationMorphism.G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">&,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>, <a class="idref" href="mathcomp.fingroup.automorphism.html#conj_aut"><span class="id" title="definition">conj_aut</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#y"><span class="id" title="variable">y</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.automorphism.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#746f7e4d3218aa2699eefc064b513fc2"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="conj_aut_morphM"><span class="id" title="lemma">conj_aut_morphM</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#ConjugationMorphism.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">&,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#conj_aut"><span class="id" title="definition">conj_aut</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#8b8794efbfbae1b793d9cb62ce802285"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e69c60b553f06d3463460a9f4cee3c01"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">conj_aut_morphism</span> := <a class="idref" href="mathcomp.fingroup.morphism.html#Morphism"><span class="id" title="constructor">Morphism</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#conj_aut_morphM"><span class="id" title="lemma">conj_aut_morphM</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="ker_conj_aut"><span class="id" title="lemma">ker_conj_aut</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#7ef99623452370540bbc44fd30b0bc94"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#7ef99623452370540bbc44fd30b0bc94"><span class="id" title="notation">ker</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#conj_aut"><span class="id" title="definition">conj_aut</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.fingroup.html#313ef60ac6c7566906fa5b28c1bbf405"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#313ef60ac6c7566906fa5b28c1bbf405"><span class="id" title="notation">C</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#313ef60ac6c7566906fa5b28c1bbf405"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#ConjugationMorphism.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#313ef60ac6c7566906fa5b28c1bbf405"><span class="id" title="notation">)</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Aut_conj_aut"><span class="id" title="lemma">Aut_conj_aut</span></a> <span class="id" title="var">A</span> : <a class="idref" href="mathcomp.fingroup.automorphism.html#conj_aut"><span class="id" title="definition">conj_aut</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#ConjugationMorphism.G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.fingroup.automorphism.html#ConjugationMorphism"><span class="id" title="section">ConjugationMorphism</span></a>.<br/> - -<br/> - -<br/> -<span class="id" title="keyword">Reserved Notation</span> "G \char H" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 70).<br/> - -<br/> -</div> - -<div class="doc"> - Characteristic subgroup -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Section</span> <a name="Characteristicity"><span class="id" title="section">Characteristicity</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="Characteristicity.gT"><span class="id" title="variable">gT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>.<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">A</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.automorphism.html#Characteristicity.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>.<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">G</span> <span class="id" title="var">H</span> <span class="id" title="var">K</span> <span class="id" title="var">L</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.automorphism.html#Characteristicity.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="characteristic"><span class="id" title="definition">characteristic</span></a> <span class="id" title="var">A</span> <span class="id" title="var">B</span> :=<br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.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.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">&&</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#9b40a7420e06ba2a775d87b43bd1c69f"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#9b40a7420e06ba2a775d87b43bd1c69f"><span class="id" title="notation">∀</span></a> <span class="id" title="var">f</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#9b40a7420e06ba2a775d87b43bd1c69f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#Aut"><span class="id" title="definition">Aut</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f3be25edeb0349b0a76405eded9d0b98"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#de2c3fcab69008133cce8f8fc06f2b4b"><span class="id" title="notation">@:</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#9b40a7420e06ba2a775d87b43bd1c69f"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Infix</span> <a name="29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">"</span></a>\char" := <a class="idref" href="mathcomp.fingroup.automorphism.html#characteristic"><span class="id" title="definition">characteristic</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="charP"><span class="id" title="lemma">charP</span></a> <span class="id" title="var">H</span> <span class="id" title="var">G</span> :<br/> - <span class="id" title="keyword">let</span> <span class="id" title="var">fixH</span> (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#Characteristicity.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">}</span></a>) := <a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.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.automorphism.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#H"><span class="id" title="variable">H</span></a> <span class="id" title="tactic">in</span><br/> - <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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#53e4c1e546d9b20e029d981f761726c2"><span class="id" title="notation">[/\</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#53e4c1e546d9b20e029d981f761726c2"><span class="id" title="notation">&</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">f</span>, <a class="idref" href="mathcomp.fingroup.automorphism.html#fixH"><span class="id" title="variable">fixH</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#f"><span class="id" title="variable">f</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#53e4c1e546d9b20e029d981f761726c2"><span class="id" title="notation">]</span></a> (<a class="idref" href="mathcomp.fingroup.automorphism.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#G"><span class="id" title="variable">G</span></a>).<br/> - -<br/> -</div> - -<div class="doc"> - Characteristic subgroup properties : composition, relational properties -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="char1"><span class="id" title="lemma">char1</span></a> <span class="id" title="var">G</span> : 1 <a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="char_refl"><span class="id" title="lemma">char_refl</span></a> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.automorphism.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="char_trans"><span class="id" title="lemma">char_trans</span></a> <span class="id" title="var">H</span> <span class="id" title="var">G</span> <span class="id" title="var">K</span> : <a class="idref" href="mathcomp.fingroup.automorphism.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.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.automorphism.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.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.automorphism.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="char_norms"><span class="id" title="lemma">char_norms</span></a> <span class="id" title="var">H</span> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.automorphism.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.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.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="char_sub"><span class="id" title="lemma">char_sub</span></a> <span class="id" title="var">A</span> <span class="id" title="var">B</span> : <a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.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#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#B"><span class="id" title="variable">B</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="char_norm_trans"><span class="id" title="lemma">char_norm_trans</span></a> <span class="id" title="var">H</span> <span class="id" title="var">G</span> <span class="id" title="var">A</span> : <a class="idref" href="mathcomp.fingroup.automorphism.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.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.automorphism.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="char_normal_trans"><span class="id" title="lemma">char_normal_trans</span></a> <span class="id" title="var">H</span> <span class="id" title="var">G</span> <span class="id" title="var">K</span> : <a class="idref" href="mathcomp.fingroup.automorphism.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.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.automorphism.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7e8095b432e7aa5c3c22bb87584658b7"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.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.automorphism.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7e8095b432e7aa5c3c22bb87584658b7"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="char_normal"><span class="id" title="lemma">char_normal</span></a> <span class="id" title="var">H</span> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.automorphism.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.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.automorphism.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7e8095b432e7aa5c3c22bb87584658b7"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="char_norm"><span class="id" title="lemma">char_norm</span></a> <span class="id" title="var">H</span> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.automorphism.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.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.automorphism.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="charI"><span class="id" title="lemma">charI</span></a> <span class="id" title="var">G</span> <span class="id" title="var">H</span> <span class="id" title="var">K</span> : <a class="idref" href="mathcomp.fingroup.automorphism.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.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.automorphism.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.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.automorphism.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#b9596739b058766532fc6517a36fef9f"><span class="id" title="notation">:&:</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="charY"><span class="id" title="lemma">charY</span></a> <span class="id" title="var">G</span> <span class="id" title="var">H</span> <span class="id" title="var">K</span> : <a class="idref" href="mathcomp.fingroup.automorphism.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.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.automorphism.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.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.automorphism.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#0d7ccd69af81527d9facc6293603bbef"><span class="id" title="notation"><*></span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="charM"><span class="id" title="lemma">charM</span></a> <span class="id" title="var">G</span> <span class="id" title="var">H</span> <span class="id" title="var">K</span> : <a class="idref" href="mathcomp.fingroup.automorphism.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.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.automorphism.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.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.automorphism.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#8b8794efbfbae1b793d9cb62ce802285"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="lone_subgroup_char"><span class="id" title="lemma">lone_subgroup_char</span></a> <span class="id" title="var">G</span> <span class="id" title="var">H</span> :<br/> - <a class="idref" href="mathcomp.fingroup.automorphism.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.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><span class="id" title="keyword">∀</span> <span class="id" title="var">K</span>, <a class="idref" href="mathcomp.fingroup.automorphism.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.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.automorphism.html#K"><span class="id" title="variable">K</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.automorphism.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.automorphism.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.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#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.fingroup.automorphism.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#29dd2439c5ea90842199fa951ba10bba"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.fingroup.automorphism.html#Characteristicity"><span class="id" title="section">Characteristicity</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="d9dc63f0c53bc5e6f232c50d48c40709"><span class="id" title="notation">"</span></a>H \char G" := (<a class="idref" href="mathcomp.fingroup.automorphism.html#characteristic"><span class="id" title="definition">characteristic</span></a> <span class="id" title="var">H</span> <span class="id" title="var">G</span>) : <span class="id" title="var">group_scope</span>.<br/> -<span class="id" title="keyword">Hint Resolve</span> <span class="id" title="var">char_refl</span> : <span class="id" title="var">core</span>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="InjmChar"><span class="id" title="section">InjmChar</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="InjmChar.aT"><span class="id" title="variable">aT</span></a> <a name="InjmChar.rT"><span class="id" title="variable">rT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<a name="InjmChar.D"><span class="id" title="variable">D</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) (<a name="InjmChar.f"><span class="id" title="variable">f</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">}</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Hypothesis</span> <a name="InjmChar.injf"><span class="id" title="variable">injf</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#InjmChar.f"><span class="id" title="variable">f</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="injm_char"><span class="id" title="lemma">injm_char</span></a> (<span class="id" title="var">G</span> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#InjmChar.aT"><span class="id" title="variable">aT</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.automorphism.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#InjmChar.D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#d9dc63f0c53bc5e6f232c50d48c40709"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#d9dc63f0c53bc5e6f232c50d48c40709"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.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.automorphism.html#InjmChar.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#d9dc63f0c53bc5e6f232c50d48c40709"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#d9dc63f0c53bc5e6f232c50d48c40709"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#InjmChar.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.fingroup.automorphism.html#InjmChar"><span class="id" title="section">InjmChar</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="CharInjm"><span class="id" title="section">CharInjm</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="CharInjm.aT"><span class="id" title="variable">aT</span></a> <a name="CharInjm.rT"><span class="id" title="variable">rT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<a name="CharInjm.D"><span class="id" title="variable">D</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) (<a name="CharInjm.f"><span class="id" title="variable">f</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">}</span></a>).<br/> -<span class="id" title="keyword">Hypothesis</span> <a name="CharInjm.injf"><span class="id" title="variable">injf</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#CharInjm.f"><span class="id" title="variable">f</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="char_injm"><span class="id" title="lemma">char_injm</span></a> (<span class="id" title="var">G</span> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#CharInjm.aT"><span class="id" title="variable">aT</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.automorphism.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#CharInjm.D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#CharInjm.D"><span class="id" title="variable">D</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="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.automorphism.html#CharInjm.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#d9dc63f0c53bc5e6f232c50d48c40709"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#d9dc63f0c53bc5e6f232c50d48c40709"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#CharInjm.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="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.automorphism.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#d9dc63f0c53bc5e6f232c50d48c40709"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.automorphism.html#d9dc63f0c53bc5e6f232c50d48c40709"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.fingroup.automorphism.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.fingroup.automorphism.html#CharInjm"><span class="id" title="section">CharInjm</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Unset Implicit Arguments</span>.<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 |