diff options
Diffstat (limited to 'docs/htmldoc/mathcomp.fingroup.perm.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.fingroup.perm.html | 469 |
1 files changed, 0 insertions, 469 deletions
diff --git a/docs/htmldoc/mathcomp.fingroup.perm.html b/docs/htmldoc/mathcomp.fingroup.perm.html deleted file mode 100644 index 7a984bf..0000000 --- a/docs/htmldoc/mathcomp.fingroup.perm.html +++ /dev/null @@ -1,469 +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.perm</title> -</head> - -<body> - -<div id="page"> - -<div id="header"> -</div> - -<div id="main"> - -<h1 class="libtitle">Library mathcomp.fingroup.perm</h1> - -<div class="code"> -<span class="comment">(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. <br/> - Distributed under the terms of CeCILL-B. *)</span><br/> - -<br/> -</div> - -<div class="doc"> - This file contains the definition and properties associated to the group - of permutations of an arbitrary finite type. - {perm T} == the type of permutations of a finite type T, i.e., - injective (finite) functions from T to T. Permutations - coerce to CiC functions. - 'S_n == the set of all permutations of 'I_n, i.e., of {0,.., n-1} - perm_on A u == u is a permutation with support A, i.e., u only displaces - elements of A (u x != x implies x \in A). - tperm x y == the transposition of x, y. - aperm x s == the image of x under the action of the permutation s. - := s x - pcycle s x == the set of all elements that are in the same cycle of the - permutation s as x, i.e., {x, s x, (s ^+ 2) x, ...}. - pcycles s == the set of all the cycles of the permutation s. - (s : bool) == s is an odd permutation (the coercion is called odd_perm). - dpair u == u is a pair (x, y) of distinct objects (i.e., x != y). - lift_perm i j s == the permutation obtained by lifting s : 'S_n.-1 over - (i |-> j), that maps i to j and lift i k to lift j (s k). - Canonical structures are defined allowing permutations to be an eqType, - choiceType, countType, finType, subType, finGroupType; permutations with - composition form a group, therefore inherit all generic group notations: - 1 == identity permutation, * == composition, ^-1 == inverse permutation. -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Set Implicit Arguments</span>.<br/> - -<br/> -<span class="id" title="keyword">Import</span> <span class="id" title="var">GroupScope</span>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="PermDefSection"><span class="id" title="section">PermDefSection</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="PermDefSection.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>.<br/> - -<br/> -<span class="id" title="keyword">Inductive</span> <a name="perm_type"><span class="id" title="inductive">perm_type</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#predArgType"><span class="id" title="definition">predArgType</span></a> :=<br/> - <a name="Perm"><span class="id" title="constructor">Perm</span></a> (<span class="id" title="var">pval</span> : <a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">ffun</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#PermDefSection.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.perm.html#PermDefSection.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.finfun.html#31493a873acc18a8368490ef56022c0c"><span class="id" title="notation">}</span></a>) & <a class="idref" href="mathcomp.ssreflect.fintype.html#injectiveb"><span class="id" title="definition">injectiveb</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#pval"><span class="id" title="variable">pval</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="pval"><span class="id" title="definition">pval</span></a> <span class="id" title="var">p</span> := <span class="id" title="keyword">let</span>: <a class="idref" href="mathcomp.fingroup.perm.html#Perm"><span class="id" title="constructor">Perm</span></a> <span class="id" title="var">f</span> <span class="id" title="var">_</span> := <a class="idref" href="mathcomp.fingroup.perm.html#p"><span class="id" title="variable">p</span></a> <span class="id" title="tactic">in</span> <span class="id" title="var">f</span>.<br/> -<span class="id" title="keyword">Definition</span> <a name="perm_of"><span class="id" title="definition">perm_of</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#phant"><span class="id" title="inductive">phant</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#PermDefSection.T"><span class="id" title="variable">T</span></a> := <a class="idref" href="mathcomp.fingroup.perm.html#perm_type"><span class="id" title="inductive">perm_type</span></a>.<br/> -<span class="id" title="keyword">Identity</span> <span class="id" title="keyword">Coercion</span> <span class="id" title="var">type_of_perm</span> : <span class="id" title="var">perm_of</span> >-> <span class="id" title="var">perm_type</span>.<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="pT"><span class="id" title="abbreviation">pT</span></a> := (<a class="idref" href="mathcomp.fingroup.perm.html#perm_of"><span class="id" title="definition">perm_of</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#PermDefSection.T"><span class="id" title="variable">T</span></a>)).<br/> - -<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_subType</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.ssreflect.eqtype.html#c2d02b544d823cdc1e1e08de552cdba4"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#c2d02b544d823cdc1e1e08de552cdba4"><span class="id" title="notation">subType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c2d02b544d823cdc1e1e08de552cdba4"><span class="id" title="notation">for</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#pval"><span class="id" title="definition">pval</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#c2d02b544d823cdc1e1e08de552cdba4"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="perm_eqMixin"><span class="id" title="definition">perm_eqMixin</span></a> := <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.ssreflect.eqtype.html#b361a0fe0b43cea5c506ee5eccc55542"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#b361a0fe0b43cea5c506ee5eccc55542"><span class="id" title="notation">eqMixin</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b361a0fe0b43cea5c506ee5eccc55542"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_type"><span class="id" title="inductive">perm_type</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b361a0fe0b43cea5c506ee5eccc55542"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b361a0fe0b43cea5c506ee5eccc55542"><span class="id" title="notation"><:]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_eqType</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.ssreflect.eqtype.html#Equality.Exports.EqType"><span class="id" title="abbreviation">EqType</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_type"><span class="id" title="inductive">perm_type</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_eqMixin"><span class="id" title="definition">perm_eqMixin</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="perm_choiceMixin"><span class="id" title="definition">perm_choiceMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#035054ba987e1c05f2985518b41ec31f"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#035054ba987e1c05f2985518b41ec31f"><span class="id" title="notation">choiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#035054ba987e1c05f2985518b41ec31f"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_type"><span class="id" title="inductive">perm_type</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#035054ba987e1c05f2985518b41ec31f"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#035054ba987e1c05f2985518b41ec31f"><span class="id" title="notation"><:]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_choiceType</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.ssreflect.choice.html#Choice.Exports.ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_type"><span class="id" title="inductive">perm_type</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_choiceMixin"><span class="id" title="definition">perm_choiceMixin</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="perm_countMixin"><span class="id" title="definition">perm_countMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#c2a823e7a76d1d303efdd00309d93aca"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#c2a823e7a76d1d303efdd00309d93aca"><span class="id" title="notation">countMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#c2a823e7a76d1d303efdd00309d93aca"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_type"><span class="id" title="inductive">perm_type</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#c2a823e7a76d1d303efdd00309d93aca"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#c2a823e7a76d1d303efdd00309d93aca"><span class="id" title="notation"><:]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_countType</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.ssreflect.choice.html#Countable.Exports.CountType"><span class="id" title="abbreviation">CountType</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_type"><span class="id" title="inductive">perm_type</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_countMixin"><span class="id" title="definition">perm_countMixin</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_subCountType</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.ssreflect.choice.html#9bbd910cbebcec91f8279b0711b4702d"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#9bbd910cbebcec91f8279b0711b4702d"><span class="id" title="notation">subCountType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#9bbd910cbebcec91f8279b0711b4702d"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_type"><span class="id" title="inductive">perm_type</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#9bbd910cbebcec91f8279b0711b4702d"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="perm_finMixin"><span class="id" title="definition">perm_finMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.fintype.html#fede21e6a36088be0833d2600143b39c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#fede21e6a36088be0833d2600143b39c"><span class="id" title="notation">finMixin</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#fede21e6a36088be0833d2600143b39c"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_type"><span class="id" title="inductive">perm_type</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#fede21e6a36088be0833d2600143b39c"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#fede21e6a36088be0833d2600143b39c"><span class="id" title="notation"><:]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_finType</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.ssreflect.fintype.html#Finite.Exports.FinType"><span class="id" title="abbreviation">FinType</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_type"><span class="id" title="inductive">perm_type</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_finMixin"><span class="id" title="definition">perm_finMixin</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_subFinType</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.ssreflect.fintype.html#ea70e506e168d39ce0ec3d3ecd2c349f"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#ea70e506e168d39ce0ec3d3ecd2c349f"><span class="id" title="notation">subFinType</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#ea70e506e168d39ce0ec3d3ecd2c349f"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_type"><span class="id" title="inductive">perm_type</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#ea70e506e168d39ce0ec3d3ecd2c349f"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_for_subType</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.ssreflect.eqtype.html#aa8c179e7d847b79500c7558a661edb0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#aa8c179e7d847b79500c7558a661edb0"><span class="id" title="notation">subType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#aa8c179e7d847b79500c7558a661edb0"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#pT"><span class="id" title="abbreviation">pT</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#aa8c179e7d847b79500c7558a661edb0"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_for_eqType</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.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">eqType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#pT"><span class="id" title="abbreviation">pT</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#2b9222c46a529018a8ebb5be6355801c"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_for_choiceType</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.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">choiceType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#pT"><span class="id" title="abbreviation">pT</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#6cecb3ca492751e55998eec154506328"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_for_countType</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.ssreflect.choice.html#3fd72847645c366340e6e9be05776bd8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#3fd72847645c366340e6e9be05776bd8"><span class="id" title="notation">countType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#3fd72847645c366340e6e9be05776bd8"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#pT"><span class="id" title="abbreviation">pT</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#3fd72847645c366340e6e9be05776bd8"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_for_subCountType</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.ssreflect.choice.html#9bbd910cbebcec91f8279b0711b4702d"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#9bbd910cbebcec91f8279b0711b4702d"><span class="id" title="notation">subCountType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#9bbd910cbebcec91f8279b0711b4702d"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#pT"><span class="id" title="abbreviation">pT</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#9bbd910cbebcec91f8279b0711b4702d"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_for_finType</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.ssreflect.fintype.html#0e3773306b0834fa9a0572c7b198b77f"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#0e3773306b0834fa9a0572c7b198b77f"><span class="id" title="notation">finType</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#0e3773306b0834fa9a0572c7b198b77f"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#pT"><span class="id" title="abbreviation">pT</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#0e3773306b0834fa9a0572c7b198b77f"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_for_subFinType</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.ssreflect.fintype.html#ea70e506e168d39ce0ec3d3ecd2c349f"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#ea70e506e168d39ce0ec3d3ecd2c349f"><span class="id" title="notation">subFinType</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#ea70e506e168d39ce0ec3d3ecd2c349f"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#pT"><span class="id" title="abbreviation">pT</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#ea70e506e168d39ce0ec3d3ecd2c349f"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="perm_proof"><span class="id" title="lemma">perm_proof</span></a> (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.fingroup.perm.html#PermDefSection.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.perm.html#PermDefSection.T"><span class="id" title="variable">T</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.perm.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.ssreflect.fintype.html#injectiveb"><span class="id" title="definition">injectiveb</span></a> (<a class="idref" href="mathcomp.ssreflect.finfun.html#finfun"><span class="id" title="abbreviation">finfun</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#f"><span class="id" title="variable">f</span></a>).<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.fingroup.perm.html#PermDefSection"><span class="id" title="section">PermDefSection</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">"</span></a>{ 'perm' T }" := (<a class="idref" href="mathcomp.fingroup.perm.html#perm_of"><span class="id" title="definition">perm_of</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#Phant"><span class="id" title="constructor">Phant</span></a> <span class="id" title="var">T</span>))<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "{ 'perm' T }") : <span class="id" title="var">type_scope</span>.<br/> - -<br/> - -<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="b84ec172b7d8a9cb94a7af117c5a31d6"><span class="id" title="notation">"</span></a>''S_' n" := <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.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_n</span></a><a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">}</span></a><br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8, <span class="id" title="var">n</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">format</span> "''S_' n").<br/> - -<br/> - -<br/> -<span class="id" title="keyword">Module</span> <span class="id" title="keyword">Type</span> <a name="PermDefSig"><span class="id" title="module">PermDefSig</span></a>.<br/> -<span class="id" title="keyword">Parameter</span> <a name="PermDefSig.fun_of_perm"><span class="id" title="axiom">fun_of_perm</span></a> : <span class="id" title="keyword">∀</span> <span class="id" title="var">T</span>, <a class="idref" href="mathcomp.fingroup.perm.html#perm_type"><span class="id" title="inductive">perm_type</span></a> <a class="idref" href="mathcomp.fingroup.perm.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.perm.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.perm.html#T"><span class="id" title="variable">T</span></a>.<br/> -<span class="id" title="keyword">Parameter</span> <a name="PermDefSig.perm"><span class="id" title="axiom">perm</span></a> : <span class="id" title="keyword">∀</span> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.fingroup.perm.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.perm.html#T"><span class="id" title="variable">T</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.perm.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.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.perm.html#T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">}</span></a>.<br/> -<span class="id" title="keyword">Axiom</span> <a name="PermDefSig.fun_of_permE"><span class="id" title="axiom">fun_of_permE</span></a> : <a class="idref" href="mathcomp.fingroup.perm.html#PermDefSig.fun_of_perm"><span class="id" title="axiom">fun_of_perm</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.perm.html#fun_of_perm_def"><span class="id" title="abbreviation">fun_of_perm_def</span></a>.<br/> -<span class="id" title="keyword">Axiom</span> <a name="PermDefSig.permE"><span class="id" title="axiom">permE</span></a> : <a class="idref" href="mathcomp.fingroup.perm.html#PermDefSig.perm"><span class="id" title="axiom">perm</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.perm.html#perm_def"><span class="id" title="abbreviation">perm_def</span></a>.<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.fingroup.perm.html#PermDefSig"><span class="id" title="module">PermDefSig</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Module</span> <a name="PermDef"><span class="id" title="module">PermDef</span></a> : <a class="idref" href="mathcomp.fingroup.perm.html#PermDefSig"><span class="id" title="module">PermDefSig</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="PermDef.fun_of_perm"><span class="id" title="definition">fun_of_perm</span></a> := <a class="idref" href="mathcomp.fingroup.perm.html#fun_of_perm_def"><span class="id" title="abbreviation">fun_of_perm_def</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="PermDef.perm"><span class="id" title="definition">perm</span></a> := <a class="idref" href="mathcomp.fingroup.perm.html#perm_def"><span class="id" title="abbreviation">perm_def</span></a>.<br/> -<span class="id" title="keyword">Lemma</span> <a name="PermDef.fun_of_permE"><span class="id" title="lemma">fun_of_permE</span></a> : <a class="idref" href="mathcomp.fingroup.perm.html#PermDef.fun_of_perm"><span class="id" title="definition">fun_of_perm</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.perm.html#fun_of_perm_def"><span class="id" title="abbreviation">fun_of_perm_def</span></a>. <br/> -<span class="id" title="keyword">Lemma</span> <a name="PermDef.permE"><span class="id" title="lemma">permE</span></a> : <a class="idref" href="mathcomp.fingroup.perm.html#PermDef.perm"><span class="id" title="definition">perm</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.perm.html#perm_def"><span class="id" title="abbreviation">perm_def</span></a>. <br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.fingroup.perm.html#PermDef"><span class="id" title="module">PermDef</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="fun_of_perm"><span class="id" title="abbreviation">fun_of_perm</span></a> := <a class="idref" href="mathcomp.fingroup.perm.html#fun_of_perm"><span class="id" title="axiom">PermDef.fun_of_perm</span></a>.<br/> -<span class="id" title="keyword">Notation</span> <a name="62bf0ee6e1af563ba54ed9489553a1f5"><span class="id" title="notation">"</span></a>@ 'perm'" := (@<a class="idref" href="mathcomp.fingroup.perm.html#perm"><span class="id" title="axiom">PermDef.perm</span></a>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 10, <span class="id" title="var">format</span> "@ 'perm'").<br/> -<span class="id" title="keyword">Notation</span> <a name="perm"><span class="id" title="abbreviation">perm</span></a> := (@<a class="idref" href="mathcomp.fingroup.perm.html#perm"><span class="id" title="axiom">PermDef.perm</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span>).<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">fun_of_perm_unlock</span> := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#Unlockable"><span class="id" title="constructor">Unlockable</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#fun_of_permE"><span class="id" title="axiom">PermDef.fun_of_permE</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_unlock</span> := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#Unlockable"><span class="id" title="constructor">Unlockable</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#permE"><span class="id" title="axiom">PermDef.permE</span></a>.<br/> -<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.fingroup.perm.html#fun_of_perm"><span class="id" title="axiom">fun_of_perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#fun_of_perm"><span class="id" title="axiom">:</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#fun_of_perm"><span class="id" title="axiom">perm_type</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#fun_of_perm"><span class="id" title="axiom">>-></span></a> <a class="idref" href="mathcomp.fingroup.perm.html#fun_of_perm"><span class="id" title="axiom">Funclass</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="Theory"><span class="id" title="section">Theory</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="Theory.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>.<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.fingroup.perm.html#Theory.T"><span class="id" title="variable">T</span></a>) (<span class="id" title="var">s</span> <span class="id" title="var">t</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.perm.html#Theory.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">S</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.perm.html#Theory.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>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="permP"><span class="id" title="lemma">permP</span></a> <span class="id" title="var">s</span> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</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.perm.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#4bfb4f2d0721ba668e3a802ab1b745a1"><span class="id" title="notation">↔</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</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.perm.html#t"><span class="id" title="variable">t</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="pvalE"><span class="id" title="lemma">pvalE</span></a> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.fingroup.perm.html#pval"><span class="id" title="definition">pval</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">:></span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.perm.html#Theory.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.perm.html#Theory.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#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">)</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="permE"><span class="id" title="lemma">permE</span></a> <span class="id" title="var">f</span> <span class="id" title="var">f_inj</span> : <a class="idref" href="mathcomp.fingroup.perm.html#62bf0ee6e1af563ba54ed9489553a1f5"><span class="id" title="notation">@</span></a><a class="idref" href="mathcomp.fingroup.perm.html#62bf0ee6e1af563ba54ed9489553a1f5"><span class="id" title="notation">perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#62bf0ee6e1af563ba54ed9489553a1f5"><span class="id" title="notation">T</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#62bf0ee6e1af563ba54ed9489553a1f5"><span class="id" title="notation">f</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#62bf0ee6e1af563ba54ed9489553a1f5"><span class="id" title="notation">f_inj</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.perm.html#f"><span class="id" title="variable">f</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="perm_inj"><span class="id" title="lemma">perm_inj</span></a> {<span class="id" title="var">s</span>} : <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.perm.html#s"><span class="id" title="variable">s</span></a>.<br/> - <span class="id" title="keyword">Hint Resolve</span> <span class="id" title="var">perm_inj</span> : <span class="id" title="var">core</span>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="perm_onto"><span class="id" title="lemma">perm_onto</span></a> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#codom"><span class="id" title="definition">codom</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#1e6a438ff685c38fcd9034a94f271777"><span class="id" title="notation">=</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#1e6a438ff685c38fcd9034a94f271777"><span class="id" title="notation">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#predT"><span class="id" title="definition">predT</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="perm_one"><span class="id" title="definition">perm_one</span></a> := <a class="idref" href="mathcomp.fingroup.perm.html#perm"><span class="id" title="abbreviation">perm</span></a> (@<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#inj_id"><span class="id" title="lemma">inj_id</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#Theory.T"><span class="id" title="variable">T</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="perm_invK"><span class="id" title="lemma">perm_invK</span></a> <span class="id" title="var">s</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">x</span> ⇒ <a class="idref" href="mathcomp.ssreflect.fintype.html#iinv"><span class="id" title="definition">iinv</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#perm_onto"><span class="id" title="lemma">perm_onto</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a>)) <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="perm_inv"><span class="id" title="definition">perm_inv</span></a> <span class="id" title="var">s</span> := <a class="idref" href="mathcomp.fingroup.perm.html#perm"><span class="id" title="abbreviation">perm</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#can_inj"><span class="id" title="lemma">can_inj</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#perm_invK"><span class="id" title="lemma">perm_invK</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a>)).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="perm_mul"><span class="id" title="definition">perm_mul</span></a> <span class="id" title="var">s</span> <span class="id" title="var">t</span> := <a class="idref" href="mathcomp.fingroup.perm.html#perm"><span class="id" title="abbreviation">perm</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#inj_comp"><span class="id" title="lemma">inj_comp</span></a> (@<a class="idref" href="mathcomp.fingroup.perm.html#perm_inj"><span class="id" title="lemma">perm_inj</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#t"><span class="id" title="variable">t</span></a>) (@<a class="idref" href="mathcomp.fingroup.perm.html#perm_inj"><span class="id" title="lemma">perm_inj</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a>)).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="perm_oneP"><span class="id" title="lemma">perm_oneP</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#left_id"><span class="id" title="definition">left_id</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_one"><span class="id" title="definition">perm_one</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_mul"><span class="id" title="definition">perm_mul</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="perm_invP"><span class="id" title="lemma">perm_invP</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#left_inverse"><span class="id" title="definition">left_inverse</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_one"><span class="id" title="definition">perm_one</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_inv"><span class="id" title="definition">perm_inv</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_mul"><span class="id" title="definition">perm_mul</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="perm_mulP"><span class="id" title="lemma">perm_mulP</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#associative"><span class="id" title="definition">associative</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_mul"><span class="id" title="definition">perm_mul</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="perm_of_baseFinGroupMixin"><span class="id" title="definition">perm_of_baseFinGroupMixin</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.mixin_of"><span class="id" title="record">FinGroup.mixin_of</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#perm_type"><span class="id" title="inductive">perm_type</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#Theory.T"><span class="id" title="variable">T</span></a>) :=<br/> - <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Mixin"><span class="id" title="definition">FinGroup.Mixin</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_mulP"><span class="id" title="lemma">perm_mulP</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_oneP"><span class="id" title="lemma">perm_oneP</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_invP"><span class="id" title="lemma">perm_invP</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_baseFinGroupType</span> :=<br/> - <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.fingroup.html#FinGroup.Exports.BaseFinGroupType"><span class="id" title="abbreviation">BaseFinGroupType</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#perm_type"><span class="id" title="inductive">perm_type</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#Theory.T"><span class="id" title="variable">T</span></a>) <a class="idref" href="mathcomp.fingroup.perm.html#perm_of_baseFinGroupMixin"><span class="id" title="definition">perm_of_baseFinGroupMixin</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_finGroupType</span> := @<a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.FinGroupType"><span class="id" title="abbreviation">FinGroupType</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_baseFinGroupType"><span class="id" title="definition">perm_baseFinGroupType</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#perm_invP"><span class="id" title="lemma">perm_invP</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_of_baseFinGroupType</span> :=<br/> - <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.fingroup.html#ac5c214a3d709d8519333b0f98027cc9"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ac5c214a3d709d8519333b0f98027cc9"><span class="id" title="notation">baseFinGroupType</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#ac5c214a3d709d8519333b0f98027cc9"><span class="id" title="notation">of</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.perm.html#Theory.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ac5c214a3d709d8519333b0f98027cc9"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">perm_of_finGroupType</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.fingroup.html#2bd77263376cf9e19a7b9689cc638b8a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#2bd77263376cf9e19a7b9689cc638b8a"><span class="id" title="notation">finGroupType</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#2bd77263376cf9e19a7b9689cc638b8a"><span class="id" title="notation">of</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.perm.html#Theory.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">}</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#2bd77263376cf9e19a7b9689cc638b8a"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="perm1"><span class="id" title="lemma">perm1</span></a> <span class="id" title="var">x</span> : (1 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#aed478b27f23b4f753c27c8ac393febc"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.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.perm.html#Theory.T"><span class="id" title="variable">T</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#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.perm.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="permM"><span class="id" title="lemma">permM</span></a> <span class="id" title="var">s</span> <span class="id" title="var">t</span> <span class="id" title="var">x</span> : (<a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#8b8794efbfbae1b793d9cb62ce802285"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#t"><span class="id" title="variable">t</span></a>) <a class="idref" href="mathcomp.fingroup.perm.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.perm.html#t"><span class="id" title="variable">t</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="permK"><span class="id" title="lemma">permK</span></a> <span class="id" title="var">s</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#766fd55608aa0e125ed6f55c83bcc09a"><span class="id" title="notation">^-1</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="permKV"><span class="id" title="lemma">permKV</span></a> <span class="id" title="var">s</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#766fd55608aa0e125ed6f55c83bcc09a"><span class="id" title="notation">^-1</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="permJ"><span class="id" title="lemma">permJ</span></a> <span class="id" title="var">s</span> <span class="id" title="var">t</span> <span class="id" title="var">x</span> : (<a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#746f7e4d3218aa2699eefc064b513fc2"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#t"><span class="id" title="variable">t</span></a>) (<a class="idref" href="mathcomp.fingroup.perm.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.fingroup.perm.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.perm.html#t"><span class="id" title="variable">t</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="permX"><span class="id" title="lemma">permX</span></a> <span class="id" title="var">s</span> <span class="id" title="var">x</span> <span class="id" title="var">n</span> : (<a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#06cdd2633d7788bac7abeac13b2dd91e"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#n"><span class="id" title="variable">n</span></a>) <a class="idref" href="mathcomp.fingroup.perm.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.ssreflect.ssrnat.html#iter"><span class="id" title="definition">iter</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="im_permV"><span class="id" title="lemma">im_permV</span></a> <span class="id" title="var">s</span> <span class="id" title="var">S</span> : <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#766fd55608aa0e125ed6f55c83bcc09a"><span class="id" title="notation">^-1</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#de2c3fcab69008133cce8f8fc06f2b4b"><span class="id" title="notation">@:</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#S"><span class="id" title="variable">S</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.perm.html#s"><span class="id" title="variable">s</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.perm.html#S"><span class="id" title="variable">S</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="preim_permV"><span class="id" title="lemma">preim_permV</span></a> <span class="id" title="var">s</span> <span class="id" title="var">S</span> : <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#766fd55608aa0e125ed6f55c83bcc09a"><span class="id" title="notation">^-1</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.perm.html#S"><span class="id" title="variable">S</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.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#de2c3fcab69008133cce8f8fc06f2b4b"><span class="id" title="notation">@:</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#S"><span class="id" title="variable">S</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="perm_on"><span class="id" title="definition">perm_on</span></a> <span class="id" title="var">S</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</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.perm.html#Theory.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">}</span></a> := <span class="id" title="keyword">fun</span> <span class="id" title="var">s</span> ⇒ <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#27dabc72ea2c2c768f2db80a79f42524"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#27dabc72ea2c2c768f2db80a79f42524"><span class="id" title="notation">pred</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#27dabc72ea2c2c768f2db80a79f42524"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.fingroup.perm.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#27dabc72ea2c2c768f2db80a79f42524"><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.perm.html#S"><span class="id" title="variable">S</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="perm_closed"><span class="id" title="lemma">perm_closed</span></a> <span class="id" title="var">S</span> <span class="id" title="var">s</span> <span class="id" title="var">x</span> : <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.perm.html#S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</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.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.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.perm.html#S"><span class="id" title="variable">S</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.perm.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.perm.html#S"><span class="id" title="variable">S</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="perm_on1"><span class="id" title="lemma">perm_on1</span></a> <span class="id" title="var">H</span> : <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.perm.html#H"><span class="id" title="variable">H</span></a> 1.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="perm_onM"><span class="id" title="lemma">perm_onM</span></a> <span class="id" title="var">H</span> <span class="id" title="var">s</span> <span class="id" title="var">t</span> : <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.perm.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</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.perm.html#perm_on"><span class="id" title="definition">perm_on</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.perm.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.perm.html#perm_on"><span class="id" title="definition">perm_on</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#H"><span class="id" title="variable">H</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#8b8794efbfbae1b793d9cb62ce802285"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#t"><span class="id" title="variable">t</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="out_perm"><span class="id" title="lemma">out_perm</span></a> <span class="id" title="var">S</span> <span class="id" title="var">u</span> <span class="id" title="var">x</span> : <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.perm.html#S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#u"><span class="id" title="variable">u</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.perm.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.perm.html#S"><span class="id" title="variable">S</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.perm.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.fingroup.perm.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.perm.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="im_perm_on"><span class="id" title="lemma">im_perm_on</span></a> <span class="id" title="var">u</span> <span class="id" title="var">S</span> : <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.perm.html#S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#u"><span class="id" title="variable">u</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.perm.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#de2c3fcab69008133cce8f8fc06f2b4b"><span class="id" title="notation">@:</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#S"><span class="id" title="variable">S</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.perm.html#S"><span class="id" title="variable">S</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="tperm_proof"><span class="id" title="lemma">tperm_proof</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#involutive"><span class="id" title="definition">involutive</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#5f847db88545de607ca99ef9077577ce"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#5f847db88545de607ca99ef9077577ce"><span class="id" title="notation">fun</span></a> <span class="id" title="var">z</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#5f847db88545de607ca99ef9077577ce"><span class="id" title="notation">⇒</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#5f847db88545de607ca99ef9077577ce"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#d74b61a39ba99967624d24970637896f"><span class="id" title="notation">|-></span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#5f847db88545de607ca99ef9077577ce"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#d74b61a39ba99967624d24970637896f"><span class="id" title="notation">|-></span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#5f847db88545de607ca99ef9077577ce"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="tperm"><span class="id" title="definition">tperm</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> := <a class="idref" href="mathcomp.fingroup.perm.html#perm"><span class="id" title="abbreviation">perm</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#can_inj"><span class="id" title="lemma">can_inj</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#tperm_proof"><span class="id" title="lemma">tperm_proof</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a>)).<br/> - -<br/> -<span class="id" title="keyword">Variant</span> <a name="tperm_spec"><span class="id" title="inductive">tperm_spec</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span> : <a class="idref" href="mathcomp.fingroup.perm.html#Theory.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> <span class="id" title="keyword">Type</span> :=<br/> - | <a name="TpermFirst"><span class="id" title="constructor">TpermFirst</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.fingroup.perm.html#z"><span class="id" title="variable">z</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.perm.html#x"><span class="id" title="variable">x</span></a> : <a class="idref" href="mathcomp.fingroup.perm.html#tperm_spec"><span class="id" title="inductive">tperm_spec</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a><br/> - | <a name="TpermSecond"><span class="id" title="constructor">TpermSecond</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.fingroup.perm.html#z"><span class="id" title="variable">z</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.perm.html#y"><span class="id" title="variable">y</span></a> : <a class="idref" href="mathcomp.fingroup.perm.html#tperm_spec"><span class="id" title="inductive">tperm_spec</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a><br/> - | <a name="TpermNone"><span class="id" title="constructor">TpermNone</span></a> <span class="id" title="keyword">of</span> <a class="idref" href="mathcomp.fingroup.perm.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a0a5068f83a704fcfbda8cd473a6cfea"><span class="id" title="notation">≠</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> & <a class="idref" href="mathcomp.fingroup.perm.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a0a5068f83a704fcfbda8cd473a6cfea"><span class="id" title="notation">≠</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> : <a class="idref" href="mathcomp.fingroup.perm.html#tperm_spec"><span class="id" title="inductive">tperm_spec</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#z"><span class="id" title="variable">z</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="tpermP"><span class="id" title="lemma">tpermP</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span> : <a class="idref" href="mathcomp.fingroup.perm.html#tperm_spec"><span class="id" title="inductive">tperm_spec</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#z"><span class="id" title="variable">z</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#z"><span class="id" title="variable">z</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="tpermL"><span class="id" title="lemma">tpermL</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.perm.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.perm.html#y"><span class="id" title="variable">y</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="tpermR"><span class="id" title="lemma">tpermR</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.perm.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.perm.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="tpermD"><span class="id" title="lemma">tpermD</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span> : <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#z"><span class="id" title="variable">z</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.perm.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#z"><span class="id" title="variable">z</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.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#z"><span class="id" title="variable">z</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.perm.html#z"><span class="id" title="variable">z</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="tpermC"><span class="id" title="lemma">tpermC</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.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.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="tperm1"><span class="id" title="lemma">tperm1</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.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> 1.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="tpermK"><span class="id" title="lemma">tpermK</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#involutive"><span class="id" title="definition">involutive</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="tpermKg"><span class="id" title="lemma">tpermKg</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#involutive"><span class="id" title="definition">involutive</span></a> (<a class="idref" href="mathcomp.fingroup.fingroup.html#mulg"><span class="id" title="definition">mulg</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a>)).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="tpermV"><span class="id" title="lemma">tpermV</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#766fd55608aa0e125ed6f55c83bcc09a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#766fd55608aa0e125ed6f55c83bcc09a"><span class="id" title="notation">)^-1</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.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="tperm2"><span class="id" title="lemma">tperm2</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#8b8794efbfbae1b793d9cb62ce802285"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.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> 1.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="card_perm"><span class="id" title="lemma">card_perm</span></a> <span class="id" title="var">A</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><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.perm.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#fb85b56582e20c3ab47a4e55b1f6f111"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.fingroup.perm.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#fb85b56582e20c3ab47a4e55b1f6f111"><span class="id" title="notation">)`!</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.fingroup.perm.html#Theory"><span class="id" title="section">Theory</span></a>.<br/> - -<br/> - -<br/> -</div> - -<div class="doc"> - Shorthand for using a permutation to reindex a bigop. -</div> -<div class="code"> -<span class="id" title="keyword">Notation</span> <a name="reindex_perm"><span class="id" title="abbreviation">reindex_perm</span></a> <span class="id" title="var">s</span> := (<a class="idref" href="mathcomp.ssreflect.bigop.html#reindex_inj"><span class="id" title="lemma">reindex_inj</span></a> (@<a class="idref" href="mathcomp.fingroup.perm.html#perm_inj"><span class="id" title="lemma">perm_inj</span></a> <span class="id" title="var">_</span> <span class="id" title="var">s</span>)).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="inj_tperm"><span class="id" title="lemma">inj_tperm</span></a> (<span class="id" title="var">T</span> <span class="id" title="var">T'</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.fingroup.perm.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.perm.html#T'"><span class="id" title="variable">T'</span></a>) <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span> :<br/> - <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.perm.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.perm.html#f"><span class="id" title="variable">f</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#z"><span class="id" title="variable">z</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.perm.html#tperm"><span class="id" title="definition">tperm</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.fingroup.perm.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a>) (<a class="idref" href="mathcomp.fingroup.perm.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#z"><span class="id" title="variable">z</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="tpermJ"><span class="id" title="lemma">tpermJ</span></a> (<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) <span class="id" title="var">x</span> <span class="id" title="var">y</span> (<span class="id" title="var">s</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.perm.html#T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">}</span></a>) :<br/> - <a class="idref" href="mathcomp.fingroup.fingroup.html#746f7e4d3218aa2699eefc064b513fc2"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.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.fingroup.html#746f7e4d3218aa2699eefc064b513fc2"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</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.perm.html#tperm"><span class="id" title="definition">tperm</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="tuple_permP"><span class="id" title="lemma">tuple_permP</span></a> {<span class="id" title="var">T</span> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.eqType"><span class="id" title="abbreviation">eqType</span></a>} {<span class="id" title="var">n</span>} {<span class="id" title="var">s</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#T"><span class="id" title="variable">T</span></a>} {<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.fingroup.perm.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#c3913abe839346eb60d82da74b0b1f67"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#T"><span class="id" title="variable">T</span></a>} :<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.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.fingroup.perm.html#b84ec172b7d8a9cb94a7af117c5a31d6"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.perm.html#b84ec172b7d8a9cb94a7af117c5a31d6"><span class="id" title="notation">S_n</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#9d5b9af75768e306a1218aacdf8c3490"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#9d5b9af75768e306a1218aacdf8c3490"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#t"><span class="id" title="variable">t</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a>) <a class="idref" href="mathcomp.ssreflect.tuple.html#9d5b9af75768e306a1218aacdf8c3490"><span class="id" title="notation">|</span></a> <span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.tuple.html#9d5b9af75768e306a1218aacdf8c3490"><span class="id" title="notation"><</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#9d5b9af75768e306a1218aacdf8c3490"><span class="id" title="notation">]</span></a>) (<a class="idref" href="mathcomp.ssreflect.seq.html#perm_eq"><span class="id" title="definition">perm_eq</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#t"><span class="id" title="variable">t</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="PermutationParity"><span class="id" title="section">PermutationParity</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="PermutationParity.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>.<br/> - -<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">s</span> <span class="id" title="var">t</span> <span class="id" title="var">u</span> <span class="id" title="var">v</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.perm.html#PermutationParity.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.fingroup.perm.html#683bed2e43e8b9b52492c89e618e34b6"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span> : <a class="idref" href="mathcomp.fingroup.perm.html#PermutationParity.T"><span class="id" title="variable">T</span></a>).<br/> - -<br/> -</div> - -<div class="doc"> - Note that pcycle s x is the orbit of x by < [s]> under the action aperm. - Hence, the pcycle lemmas below are special cases of more general lemmas - on orbits that will be stated in action.v. - Defining pcycle directly here avoids a dependency of matrix.v on - action.v and hence morphism.v. -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="aperm"><span class="id" title="definition">aperm</span></a> <span class="id" title="var">x</span> <span class="id" title="var">s</span> := <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="pcycle"><span class="id" title="definition">pcycle</span></a> <span class="id" title="var">s</span> <span class="id" title="var">x</span> := <a class="idref" href="mathcomp.fingroup.perm.html#aperm"><span class="id" title="definition">aperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#de2c3fcab69008133cce8f8fc06f2b4b"><span class="id" title="notation">@:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#5e5825d099c952c2db2842c142cbde94"><span class="id" title="notation"><[</span></a><a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#5e5825d099c952c2db2842c142cbde94"><span class="id" title="notation">]></span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="pcycles"><span class="id" title="definition">pcycles</span></a> <span class="id" title="var">s</span> := <a class="idref" href="mathcomp.fingroup.perm.html#pcycle"><span class="id" title="definition">pcycle</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#de2c3fcab69008133cce8f8fc06f2b4b"><span class="id" title="notation">@:</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#PermutationParity.T"><span class="id" title="variable">T</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="odd_perm"><span class="id" title="definition">odd_perm</span></a> (<span class="id" title="var">s</span> : <a class="idref" href="mathcomp.fingroup.perm.html#perm_type"><span class="id" title="inductive">perm_type</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#PermutationParity.T"><span class="id" title="variable">T</span></a>) := <a class="idref" href="mathcomp.ssreflect.ssrnat.html#odd"><span class="id" title="definition">odd</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.fingroup.perm.html#PermutationParity.T"><span class="id" title="variable">T</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#a60537c464e134477471443dd91ae651"><span class="id" title="notation">(+)</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#odd"><span class="id" title="definition">odd</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.fingroup.perm.html#pcycles"><span class="id" title="definition">pcycles</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="apermE"><span class="id" title="lemma">apermE</span></a> <span class="id" title="var">x</span> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.fingroup.perm.html#aperm"><span class="id" title="definition">aperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</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.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a>. <br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="mem_pcycle"><span class="id" title="lemma">mem_pcycle</span></a> <span class="id" title="var">s</span> <span class="id" title="var">i</span> <span class="id" title="var">x</span> : (<a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#06cdd2633d7788bac7abeac13b2dd91e"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a>) <a class="idref" href="mathcomp.fingroup.perm.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.perm.html#pcycle"><span class="id" title="definition">pcycle</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="pcycle_id"><span class="id" title="lemma">pcycle_id</span></a> <span class="id" title="var">s</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.fingroup.perm.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.perm.html#pcycle"><span class="id" title="definition">pcycle</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="uniq_traject_pcycle"><span class="id" title="lemma">uniq_traject_pcycle</span></a> <span class="id" title="var">s</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#uniq"><span class="id" title="definition">uniq</span></a> (<a class="idref" href="mathcomp.ssreflect.path.html#traject"><span class="id" title="definition">traject</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.fingroup.perm.html#pcycle"><span class="id" title="definition">pcycle</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="pcycle_traject"><span class="id" title="lemma">pcycle_traject</span></a> <span class="id" title="var">s</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.fingroup.perm.html#pcycle"><span class="id" title="definition">pcycle</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.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#1e6a438ff685c38fcd9034a94f271777"><span class="id" title="notation">=</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#1e6a438ff685c38fcd9034a94f271777"><span class="id" title="notation">i</span></a> <a class="idref" href="mathcomp.ssreflect.path.html#traject"><span class="id" title="definition">traject</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.fingroup.perm.html#pcycle"><span class="id" title="definition">pcycle</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="iter_pcycle"><span class="id" title="lemma">iter_pcycle</span></a> <span class="id" title="var">s</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.ssrnat.html#iter"><span class="id" title="definition">iter</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.fingroup.perm.html#pcycle"><span class="id" title="definition">pcycle</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.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.perm.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="eq_pcycle_mem"><span class="id" title="lemma">eq_pcycle_mem</span></a> <span class="id" title="var">s</span> <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.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.perm.html#pcycle"><span class="id" title="definition">pcycle</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#pcycle"><span class="id" title="definition">pcycle</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.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="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.perm.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.perm.html#pcycle"><span class="id" title="definition">pcycle</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.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>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="pcycle_sym"><span class="id" title="lemma">pcycle_sym</span></a> <span class="id" title="var">s</span> <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.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.perm.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.perm.html#pcycle"><span class="id" title="definition">pcycle</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.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="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.perm.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.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.perm.html#pcycle"><span class="id" title="definition">pcycle</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.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>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="pcycle_perm"><span class="id" title="lemma">pcycle_perm</span></a> <span class="id" title="var">s</span> <span class="id" title="var">i</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.fingroup.perm.html#pcycle"><span class="id" title="definition">pcycle</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> ((<a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#06cdd2633d7788bac7abeac13b2dd91e"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a>) <a class="idref" href="mathcomp.fingroup.perm.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.perm.html#pcycle"><span class="id" title="definition">pcycle</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="ncycles_mul_tperm"><span class="id" title="lemma">ncycles_mul_tperm</span></a> <span class="id" title="var">s</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <span class="id" title="keyword">let</span> <span class="id" title="var">t</span> := <a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> <span class="id" title="tactic">in</span><br/> - <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.fingroup.perm.html#pcycles"><span class="id" title="definition">pcycles</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#8b8794efbfbae1b793d9cb62ce802285"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a>)<a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#bff172cdafaf4b86cefb300b16285e42"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.perm.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.perm.html#pcycle"><span class="id" title="definition">pcycle</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bff172cdafaf4b86cefb300b16285e42"><span class="id" title="notation">).*2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.fingroup.perm.html#pcycles"><span class="id" title="definition">pcycles</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">)</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="odd_perm1"><span class="id" title="lemma">odd_perm1</span></a> : <a class="idref" href="mathcomp.fingroup.perm.html#odd_perm"><span class="id" title="definition">odd_perm</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> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="odd_mul_tperm"><span class="id" title="lemma">odd_mul_tperm</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.fingroup.perm.html#odd_perm"><span class="id" title="definition">odd_perm</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#8b8794efbfbae1b793d9cb62ce802285"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</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.ssr.ssrbool.html#a60537c464e134477471443dd91ae651"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.fingroup.perm.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.ssrbool.html#a60537c464e134477471443dd91ae651"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#a60537c464e134477471443dd91ae651"><span class="id" title="notation">(+)</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#odd_perm"><span class="id" title="definition">odd_perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="odd_tperm"><span class="id" title="lemma">odd_tperm</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.fingroup.perm.html#odd_perm"><span class="id" title="definition">odd_perm</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.perm.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="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.perm.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.fingroup.perm.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>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="dpair"><span class="id" title="definition">dpair</span></a> (<span class="id" title="var">eT</span> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.eqType"><span class="id" title="abbreviation">eqType</span></a>) := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#27dabc72ea2c2c768f2db80a79f42524"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#27dabc72ea2c2c768f2db80a79f42524"><span class="id" title="notation">pred</span></a> <span class="id" title="var">t</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#27dabc72ea2c2c768f2db80a79f42524"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e0817251e7d67ad994b4d9b1aa82a412"><span class="id" title="notation">.1</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#228e85e3c31a939cba019f255574c875"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#675082cc4d4538da052b547bdc6ea4c9"><span class="id" title="notation">.2</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#228e85e3c31a939cba019f255574c875"><span class="id" title="notation">:></span></a> <a class="idref" href="mathcomp.fingroup.perm.html#eT"><span class="id" title="variable">eT</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#27dabc72ea2c2c768f2db80a79f42524"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="prod_tpermP"><span class="id" title="lemma">prod_tpermP</span></a> <span class="id" title="var">s</span> :<br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">{</span></a><span class="id" title="var">ts</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#PermutationParity.T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#PermutationParity.T"><span class="id" title="variable">T</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</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#a6fcb2cd7cc8744b73250ec95fc4cde7"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a6fcb2cd7cc8744b73250ec95fc4cde7"><span class="id" title="notation">prod_</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a6fcb2cd7cc8744b73250ec95fc4cde7"><span class="id" title="notation">(</span></a><span class="id" title="var">t</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#a6fcb2cd7cc8744b73250ec95fc4cde7"><span class="id" title="notation"><-</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#ts"><span class="id" title="variable">ts</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a6fcb2cd7cc8744b73250ec95fc4cde7"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e0817251e7d67ad994b4d9b1aa82a412"><span class="id" title="notation">.1</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#675082cc4d4538da052b547bdc6ea4c9"><span class="id" title="notation">.2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#all"><span class="id" title="definition">all</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#dpair"><span class="id" title="definition">dpair</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#ts"><span class="id" title="variable">ts</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="odd_perm_prod"><span class="id" title="lemma">odd_perm_prod</span></a> <span class="id" title="var">ts</span> :<br/> - <a class="idref" href="mathcomp.ssreflect.seq.html#all"><span class="id" title="definition">all</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#dpair"><span class="id" title="definition">dpair</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#ts"><span class="id" title="variable">ts</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.perm.html#odd_perm"><span class="id" title="definition">odd_perm</span></a> (<a class="idref" href="mathcomp.fingroup.fingroup.html#a6fcb2cd7cc8744b73250ec95fc4cde7"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a6fcb2cd7cc8744b73250ec95fc4cde7"><span class="id" title="notation">prod_</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a6fcb2cd7cc8744b73250ec95fc4cde7"><span class="id" title="notation">(</span></a><span class="id" title="var">t</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#a6fcb2cd7cc8744b73250ec95fc4cde7"><span class="id" title="notation"><-</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#ts"><span class="id" title="variable">ts</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a6fcb2cd7cc8744b73250ec95fc4cde7"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#tperm"><span class="id" title="definition">tperm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e0817251e7d67ad994b4d9b1aa82a412"><span class="id" title="notation">.1</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#675082cc4d4538da052b547bdc6ea4c9"><span class="id" title="notation">.2</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#odd"><span class="id" title="definition">odd</span></a> (<a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#ts"><span class="id" title="variable">ts</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="odd_permM"><span class="id" title="lemma">odd_permM</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#odd_perm"><span class="id" title="definition">odd_perm</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><span class="id" title="notation">:</span></a> <span class="id" title="var">s1</span> <span class="id" title="var">s2</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s1"><span class="id" title="variable">s1</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#8b8794efbfbae1b793d9cb62ce802285"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s2"><span class="id" title="variable">s2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s1"><span class="id" title="variable">s1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#a60537c464e134477471443dd91ae651"><span class="id" title="notation">(+)</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s2"><span class="id" title="variable">s2</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#40d800f6f36c47cb5f4f2f42555867a8"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="odd_permV"><span class="id" title="lemma">odd_permV</span></a> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.fingroup.perm.html#odd_perm"><span class="id" title="definition">odd_perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#766fd55608aa0e125ed6f55c83bcc09a"><span class="id" title="notation">^-1</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.perm.html#odd_perm"><span class="id" title="definition">odd_perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="odd_permJ"><span class="id" title="lemma">odd_permJ</span></a> <span class="id" title="var">s1</span> <span class="id" title="var">s2</span> : <a class="idref" href="mathcomp.fingroup.perm.html#odd_perm"><span class="id" title="definition">odd_perm</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#s1"><span class="id" title="variable">s1</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#746f7e4d3218aa2699eefc064b513fc2"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s2"><span class="id" title="variable">s2</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.perm.html#odd_perm"><span class="id" title="definition">odd_perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s1"><span class="id" title="variable">s1</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.fingroup.perm.html#PermutationParity"><span class="id" title="section">PermutationParity</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Coercion</span> <a class="idref" href="mathcomp.fingroup.perm.html#odd_perm"><span class="id" title="definition">odd_perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#odd_perm"><span class="id" title="definition">:</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#odd_perm"><span class="id" title="definition">perm_type</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#odd_perm"><span class="id" title="definition">>-></span></a> <a class="idref" href="mathcomp.fingroup.perm.html#odd_perm"><span class="id" title="definition">bool</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="LiftPerm"><span class="id" title="section">LiftPerm</span></a>.<br/> -</div> - -<div class="doc"> - Somewhat more specialised constructs for permutations on ordinals. -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="LiftPerm.n"><span class="id" title="variable">n</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">i</span> <span class="id" title="var">j</span> : <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a>.<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">s</span> <span class="id" title="var">t</span> : <a class="idref" href="mathcomp.fingroup.perm.html#b84ec172b7d8a9cb94a7af117c5a31d6"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.perm.html#b84ec172b7d8a9cb94a7af117c5a31d6"><span class="id" title="notation">S_n</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="lift_perm_fun"><span class="id" title="definition">lift_perm_fun</span></a> <span class="id" title="var">i</span> <span class="id" title="var">j</span> <span class="id" title="var">s</span> <span class="id" title="var">k</span> :=<br/> - <span class="id" title="keyword">if</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#unlift"><span class="id" title="definition">unlift</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#k"><span class="id" title="variable">k</span></a> <span class="id" title="keyword">is</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">k'</span> <span class="id" title="keyword">then</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#lift"><span class="id" title="definition">lift</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#j"><span class="id" title="variable">j</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <span class="id" title="var">k'</span>) <span class="id" title="keyword">else</span> <a class="idref" href="mathcomp.fingroup.perm.html#j"><span class="id" title="variable">j</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="lift_permK"><span class="id" title="lemma">lift_permK</span></a> <span class="id" title="var">i</span> <span class="id" title="var">j</span> <span class="id" title="var">s</span> :<br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#lift_perm_fun"><span class="id" title="definition">lift_perm_fun</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#j"><span class="id" title="variable">j</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a>) (<a class="idref" href="mathcomp.fingroup.perm.html#lift_perm_fun"><span class="id" title="definition">lift_perm_fun</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#j"><span class="id" title="variable">j</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#766fd55608aa0e125ed6f55c83bcc09a"><span class="id" title="notation">^-1</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="lift_perm"><span class="id" title="definition">lift_perm</span></a> <span class="id" title="var">i</span> <span class="id" title="var">j</span> <span class="id" title="var">s</span> := <a class="idref" href="mathcomp.fingroup.perm.html#perm"><span class="id" title="abbreviation">perm</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#can_inj"><span class="id" title="lemma">can_inj</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#lift_permK"><span class="id" title="lemma">lift_permK</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#j"><span class="id" title="variable">j</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a>)).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="lift_perm_id"><span class="id" title="lemma">lift_perm_id</span></a> <span class="id" title="var">i</span> <span class="id" title="var">j</span> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.fingroup.perm.html#lift_perm"><span class="id" title="definition">lift_perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#j"><span class="id" title="variable">j</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</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.perm.html#j"><span class="id" title="variable">j</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="lift_perm_lift"><span class="id" title="lemma">lift_perm_lift</span></a> <span class="id" title="var">i</span> <span class="id" title="var">j</span> <span class="id" title="var">s</span> <span class="id" title="var">k'</span> :<br/> - <a class="idref" href="mathcomp.fingroup.perm.html#lift_perm"><span class="id" title="definition">lift_perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#j"><span class="id" title="variable">j</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> (<a class="idref" href="mathcomp.ssreflect.fintype.html#lift"><span class="id" title="definition">lift</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#k'"><span class="id" title="variable">k'</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#lift"><span class="id" title="definition">lift</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#j"><span class="id" title="variable">j</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#k'"><span class="id" title="variable">k'</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">:></span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#545d9d6249a673300f950a2a8b8a930b"><span class="id" title="notation">I_n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="lift_permM"><span class="id" title="lemma">lift_permM</span></a> <span class="id" title="var">i</span> <span class="id" title="var">j</span> <span class="id" title="var">k</span> <span class="id" title="var">s</span> <span class="id" title="var">t</span> :<br/> - <a class="idref" href="mathcomp.fingroup.perm.html#lift_perm"><span class="id" title="definition">lift_perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#j"><span class="id" title="variable">j</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#8b8794efbfbae1b793d9cb62ce802285"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#lift_perm"><span class="id" title="definition">lift_perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#j"><span class="id" title="variable">j</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.fingroup.perm.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#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#lift_perm"><span class="id" title="definition">lift_perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#k"><span class="id" title="variable">k</span></a> (<a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#8b8794efbfbae1b793d9cb62ce802285"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#t"><span class="id" title="variable">t</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="lift_perm1"><span class="id" title="lemma">lift_perm1</span></a> <span class="id" title="var">i</span> : <a class="idref" href="mathcomp.fingroup.perm.html#lift_perm"><span class="id" title="definition">lift_perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 1.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="lift_permV"><span class="id" title="lemma">lift_permV</span></a> <span class="id" title="var">i</span> <span class="id" title="var">j</span> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#766fd55608aa0e125ed6f55c83bcc09a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.fingroup.perm.html#lift_perm"><span class="id" title="definition">lift_perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#j"><span class="id" title="variable">j</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#766fd55608aa0e125ed6f55c83bcc09a"><span class="id" title="notation">)^-1</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.perm.html#lift_perm"><span class="id" title="definition">lift_perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#j"><span class="id" title="variable">j</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#766fd55608aa0e125ed6f55c83bcc09a"><span class="id" title="notation">^-1</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="odd_lift_perm"><span class="id" title="lemma">odd_lift_perm</span></a> <span class="id" title="var">i</span> <span class="id" title="var">j</span> <span class="id" title="var">s</span> : <a class="idref" href="mathcomp.fingroup.perm.html#lift_perm"><span class="id" title="definition">lift_perm</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#j"><span class="id" title="variable">j</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#odd"><span class="id" title="definition">odd</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#i"><span class="id" title="variable">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#a60537c464e134477471443dd91ae651"><span class="id" title="notation">(+)</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#odd"><span class="id" title="definition">odd</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#j"><span class="id" title="variable">j</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#a60537c464e134477471443dd91ae651"><span class="id" title="notation">(+)</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">:></span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.fingroup.perm.html#LiftPerm"><span class="id" title="section">LiftPerm</span></a>.<br/> - -<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="tuple_perm_eqP"><span class="id" title="abbreviation">tuple_perm_eqP</span></a> :=<br/> - (<a class="idref" href="mathcomp.ssreflect.ssreflect.html#Deprecation.Exports.deprecate"><span class="id" title="abbreviation">deprecate</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#tuple_perm_eqP"><span class="id" title="variable">tuple_perm_eqP</span></a> <a class="idref" href="mathcomp.fingroup.perm.html#tuple_permP"><span class="id" title="variable">tuple_permP</span></a>) (<span class="id" title="var">only</span> <span class="id" title="var">parsing</span>).<br/> - -<br/> -</div> -</div> - -<div id="footer"> -<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a> -</div> - -</div> - -</body> -</html>
\ No newline at end of file |