diff options
Diffstat (limited to 'docs/htmldoc/mathcomp.solvable.primitive_action.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.solvable.primitive_action.html | 241 |
1 files changed, 0 insertions, 241 deletions
diff --git a/docs/htmldoc/mathcomp.solvable.primitive_action.html b/docs/htmldoc/mathcomp.solvable.primitive_action.html deleted file mode 100644 index fcf9d4a..0000000 --- a/docs/htmldoc/mathcomp.solvable.primitive_action.html +++ /dev/null @@ -1,241 +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.solvable.primitive_action</title> -</head> - -<body> - -<div id="page"> - -<div id="header"> -</div> - -<div id="main"> - -<h1 class="libtitle">Library mathcomp.solvable.primitive_action</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"> - n-transitive and primitive actions: - [primitive A, on S | to] <=> - A acts on S in a primitive manner, i.e., A is transitive on S and - A does not act on any nontrivial partition of S. - imprimitivity_system A to S Q <=> - Q is a non-trivial primitivity system for the action of A on S via - to, i.e., Q is a non-trivial partiiton of S on which A acts. - to * n == in the %act scope, the total action induced by the total - action to on n.-tuples. via n_act to n. - n.-dtuple S == the set of n-tuples with distinct values in S. - [transitive^n A, on S | to] <=> - A is n-transitive on S, i.e., A is transitive on n.-dtuple S - == the set of n-tuples with distinct values in S. -</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="PrimitiveDef"><span class="id" title="section">PrimitiveDef</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="PrimitiveDef.aT"><span class="id" title="variable">aT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<a name="PrimitiveDef.sT"><span class="id" title="variable">sT</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">Variables</span> (<a name="PrimitiveDef.A"><span class="id" title="variable">A</span></a> : <a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#PrimitiveDef.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>) (<a name="PrimitiveDef.S"><span class="id" title="variable">S</span></a> : <a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#PrimitiveDef.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>) (<a name="PrimitiveDef.to"><span class="id" title="variable">to</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">action</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#PrimitiveDef.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">&-></span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#PrimitiveDef.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">}</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="imprimitivity_system"><span class="id" title="definition">imprimitivity_system</span></a> <span class="id" title="var">Q</span> :=<br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5a7d806905be2a0d04047156433535f1"><span class="id" title="notation">[&&</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#partition"><span class="id" title="definition">partition</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#PrimitiveDef.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#5a7d806905be2a0d04047156433535f1"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">acts</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#PrimitiveDef.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Q"><span class="id" title="variable">Q</span></a> <a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#PrimitiveDef.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#1ebbed7bbef8371b25df9685ff0f4361"><span class="id" title="notation">^*</span></a><a class="idref" href="mathcomp.fingroup.action.html#915e8fb7bcea89ddadab4deff6ea659e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5a7d806905be2a0d04047156433535f1"><span class="id" title="notation">&</span></a> 1 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#cf4676be165a6295cd8b63fc45b45d8a"><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.solvable.primitive_action.html#Q"><span class="id" title="variable">Q</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#cf4676be165a6295cd8b63fc45b45d8a"><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.solvable.primitive_action.html#PrimitiveDef.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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5a7d806905be2a0d04047156433535f1"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="primitive"><span class="id" title="definition">primitive</span></a> :=<br/> - <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">transitive</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#PrimitiveDef.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#PrimitiveDef.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#PrimitiveDef.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">&&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b3ebd0deddd84fd60e149cb5ef719351"><span class="id" title="notation">~~</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#ea6c97f834d69613538d4da1fb704b25"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#ea6c97f834d69613538d4da1fb704b25"><span class="id" title="notation">∃</span></a> <span class="id" title="var">Q</span><a class="idref" href="mathcomp.ssreflect.fintype.html#f3be25edeb0349b0a76405eded9d0b98"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#imprimitivity_system"><span class="id" title="definition">imprimitivity_system</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Q"><span class="id" title="variable">Q</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#ea6c97f834d69613538d4da1fb704b25"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.primitive_action.html#PrimitiveDef"><span class="id" title="section">PrimitiveDef</span></a>.<br/> - -<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">"</span></a>[ 'primitive' A , 'on' S | to ]" := (<a class="idref" href="mathcomp.solvable.primitive_action.html#primitive"><span class="id" title="definition">primitive</span></a> <span class="id" title="var">A</span> <span class="id" title="var">S</span> <span class="id" title="var">to</span>)<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">format</span> "[ 'primitive' A , 'on' S | to ]") : <span class="id" title="var">form_scope</span>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="Primitive"><span class="id" title="section">Primitive</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="Primitive.aT"><span class="id" title="variable">aT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<a name="Primitive.sT"><span class="id" title="variable">sT</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">Variables</span> (<a name="Primitive.G"><span class="id" title="variable">G</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) (<a name="Primitive.to"><span class="id" title="variable">to</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">action</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.aT"><span class="id" title="variable">aT</span></a> <a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">&-></span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">}</span></a>) (<a name="Primitive.S"><span class="id" title="variable">S</span></a> : <a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.sT"><span class="id" title="variable">sT</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="trans_prim_astab"><span class="id" title="lemma">trans_prim_astab</span></a> <span class="id" title="var">x</span> :<br/> - <a class="idref" href="mathcomp.solvable.primitive_action.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.solvable.primitive_action.html#Primitive.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.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">transitive</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">primitive</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><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.solvable.gseries.html#maximal_eq"><span class="id" title="definition">maximal_eq</span></a> <a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="prim_trans_norm"><span class="id" title="lemma">prim_trans_norm</span></a> (<span class="id" title="var">H</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) :<br/> - <a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">primitive</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7e8095b432e7aa5c3c22bb87584658b7"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.solvable.primitive_action.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.action.html#6998185c5f7a5efd284e9c25133c5e71"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#6998185c5f7a5efd284e9c25133c5e71"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.action.html#6998185c5f7a5efd284e9c25133c5e71"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.action.html#6998185c5f7a5efd284e9c25133c5e71"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#6998185c5f7a5efd284e9c25133c5e71"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#f031fe1957c4a4a8e217aa46af2b4e25"><span class="id" title="notation">∨</span></a> <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">transitive</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive"><span class="id" title="section">Primitive</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="NactionDef"><span class="id" title="section">NactionDef</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="NactionDef.gT"><span class="id" title="variable">gT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<a name="NactionDef.sT"><span class="id" title="variable">sT</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">Variables</span> (<a name="NactionDef.to"><span class="id" title="variable">to</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">action</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NactionDef.gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">&-></span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NactionDef.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">}</span></a>) (<a name="NactionDef.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/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="n_act"><span class="id" title="definition">n_act</span></a> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.solvable.primitive_action.html#NactionDef.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.solvable.primitive_action.html#NactionDef.sT"><span class="id" title="variable">sT</span></a>) <span class="id" title="var">a</span> := <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#map"><span class="id" title="definition">map</span></a> (<a class="idref" href="mathcomp.solvable.primitive_action.html#NactionDef.to"><span class="id" title="variable">to</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#d89396f990d6b54d736cfe259e498cf4"><span class="id" title="notation">^~</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#a"><span class="id" title="variable">a</span></a>) <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Fact</span> <a name="n_act_is_action"><span class="id" title="lemma">n_act_is_action</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#is_action"><span class="id" title="definition">is_action</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#setT"><span class="id" title="abbreviation">setT</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#n_act"><span class="id" title="definition">n_act</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">n_act_action</span> := <a class="idref" href="mathcomp.fingroup.action.html#Action"><span class="id" title="constructor">Action</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#n_act_is_action"><span class="id" title="lemma">n_act_is_action</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.primitive_action.html#NactionDef"><span class="id" title="section">NactionDef</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="7472b0b72b7b3e0244b040606fd1fa69"><span class="id" title="notation">"</span></a>to * n" := (<a class="idref" href="mathcomp.solvable.primitive_action.html#n_act_action"><span class="id" title="definition">n_act_action</span></a> <span class="id" title="var">to</span> <span class="id" title="var">n</span>) : <span class="id" title="var">action_scope</span>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="NTransitive"><span class="id" title="section">NTransitive</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="NTransitive.gT"><span class="id" title="variable">gT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<a name="NTransitive.sT"><span class="id" title="variable">sT</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">Variables</span> (<a name="NTransitive.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>) (<a name="NTransitive.A"><span class="id" title="variable">A</span></a> : <a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>) (<a name="NTransitive.S"><span class="id" title="variable">S</span></a> : <a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>) (<a name="NTransitive.to"><span class="id" title="variable">to</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">action</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive.gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">&-></span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">}</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="dtuple_on"><span class="id" title="definition">dtuple_on</span></a> := <a class="idref" href="mathcomp.ssreflect.finset.html#3e9d12914c7607378976c499a50a47c7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#3e9d12914c7607378976c499a50a47c7"><span class="id" title="notation">set</span></a> <span class="id" title="var">t</span> <a class="idref" href="mathcomp.ssreflect.finset.html#3e9d12914c7607378976c499a50a47c7"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive.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.solvable.primitive_action.html#NTransitive.sT"><span class="id" title="variable">sT</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#3e9d12914c7607378976c499a50a47c7"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#uniq"><span class="id" title="definition">uniq</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#3e9d12914c7607378976c499a50a47c7"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</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.solvable.primitive_action.html#NTransitive.S"><span class="id" title="variable">S</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#3e9d12914c7607378976c499a50a47c7"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="ntransitive"><span class="id" title="definition">ntransitive</span></a> := <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">transitive</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#dtuple_on"><span class="id" title="definition">dtuple_on</span></a> <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#7472b0b72b7b3e0244b040606fd1fa69"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive.n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="dtuple_onP"><span class="id" title="lemma">dtuple_onP</span></a> <span class="id" title="var">t</span> :<br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#injective"><span class="id" title="definition">injective</span></a> (<a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.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#ba2b0e492d2b4675a0acf3ea92aabadd"><span class="id" title="notation">∧</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">i</span>, <a class="idref" href="mathcomp.ssreflect.tuple.html#tnth"><span class="id" title="definition">tnth</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.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#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.solvable.primitive_action.html#NTransitive.S"><span class="id" title="variable">S</span></a>) (<a class="idref" href="mathcomp.solvable.primitive_action.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.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.solvable.primitive_action.html#dtuple_on"><span class="id" title="definition">dtuple_on</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="n_act_dtuple"><span class="id" title="lemma">n_act_dtuple</span></a> <span class="id" title="var">t</span> <span class="id" title="var">a</span> :<br/> - <a class="idref" href="mathcomp.solvable.primitive_action.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.action.html#c0af106a0ada6310ccb2e8e8c7766282"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#c0af106a0ada6310ccb2e8e8c7766282"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.action.html#c0af106a0ada6310ccb2e8e8c7766282"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.action.html#c0af106a0ada6310ccb2e8e8c7766282"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#c0af106a0ada6310ccb2e8e8c7766282"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.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.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.solvable.primitive_action.html#dtuple_on"><span class="id" title="definition">dtuple_on</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.solvable.primitive_action.html#n_act"><span class="id" title="definition">n_act</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#dtuple_on"><span class="id" title="definition">dtuple_on</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive"><span class="id" title="section">NTransitive</span></a>.<br/> - -<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="9437d70414518cee40513da45e8f965b"><span class="id" title="notation">"</span></a>n .-dtuple ( S )" := (<a class="idref" href="mathcomp.solvable.primitive_action.html#dtuple_on"><span class="id" title="definition">dtuple_on</span></a> <span class="id" title="var">n</span> <span class="id" title="var">S</span>)<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8, <span class="id" title="var">format</span> "n .-dtuple ( S )") : <span class="id" title="var">set_scope</span>.<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">"</span></a>[ 'transitive' ^ n A , 'on' S | to ]" := (<a class="idref" href="mathcomp.solvable.primitive_action.html#ntransitive"><span class="id" title="definition">ntransitive</span></a> <span class="id" title="var">n</span> <span class="id" title="var">A</span> <span class="id" title="var">S</span> <span class="id" title="var">to</span>)<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">n</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8,<br/> - <span class="id" title="var">format</span> "[ 'transitive' ^ n A , 'on' S | to ]") : <span class="id" title="var">form_scope</span>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="NTransitveProp"><span class="id" title="section">NTransitveProp</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="NTransitveProp.gT"><span class="id" title="variable">gT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<a name="NTransitveProp.sT"><span class="id" title="variable">sT</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">Variables</span> (<a name="NTransitveProp.to"><span class="id" title="variable">to</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">action</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">&-></span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">}</span></a>) (<a name="NTransitveProp.G"><span class="id" title="variable">G</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) (<a name="NTransitveProp.S"><span class="id" title="variable">S</span></a> : <a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.sT"><span class="id" title="variable">sT</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="card_uniq_tuple"><span class="id" title="lemma">card_uniq_tuple</span></a> <span class="id" title="var">n</span> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.solvable.primitive_action.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.solvable.primitive_action.html#NTransitveProp.sT"><span class="id" title="variable">sT</span></a>) : <a class="idref" href="mathcomp.ssreflect.seq.html#uniq"><span class="id" title="definition">uniq</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.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.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#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.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#n"><span class="id" title="variable">n</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="n_act0"><span class="id" title="lemma">n_act0</span></a> (<span class="id" title="var">t</span> : 0<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.solvable.primitive_action.html#NTransitveProp.sT"><span class="id" title="variable">sT</span></a>) <span class="id" title="var">a</span> : <a class="idref" href="mathcomp.solvable.primitive_action.html#n_act"><span class="id" title="definition">n_act</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#40a2c8face21f18a7058a916d5f839b8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#40a2c8face21f18a7058a916d5f839b8"><span class="id" title="notation">tuple</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#40a2c8face21f18a7058a916d5f839b8"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="dtuple_on_add"><span class="id" title="lemma">dtuple_on_add</span></a> <span class="id" title="var">n</span> <span class="id" title="var">x</span> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.solvable.primitive_action.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.solvable.primitive_action.html#NTransitveProp.sT"><span class="id" title="variable">sT</span></a>) :<br/> - <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#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#407cde5b61fbf27196d1a7c5a475e083"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><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">\</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.solvable.primitive_action.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">dtuple</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><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><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5a7d806905be2a0d04047156433535f1"><span class="id" title="notation">[&&</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.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.solvable.primitive_action.html#NTransitveProp.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#5a7d806905be2a0d04047156433535f1"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.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.solvable.primitive_action.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.ssrbool.html#5a7d806905be2a0d04047156433535f1"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.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.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.solvable.primitive_action.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">dtuple</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5a7d806905be2a0d04047156433535f1"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="dtuple_on_add_D1"><span class="id" title="lemma">dtuple_on_add_D1</span></a> <span class="id" title="var">n</span> <span class="id" title="var">x</span> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.solvable.primitive_action.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.solvable.primitive_action.html#NTransitveProp.sT"><span class="id" title="variable">sT</span></a>) :<br/> - <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#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#407cde5b61fbf27196d1a7c5a475e083"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><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">\</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.solvable.primitive_action.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">dtuple</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><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><br/> - <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#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.primitive_action.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.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">&&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.primitive_action.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.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.solvable.primitive_action.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">dtuple</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#c91810fcd799fcd960468c603a6be0a6"><span class="id" title="notation">:\</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">)</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="dtuple_on_subset"><span class="id" title="lemma">dtuple_on_subset</span></a> <span class="id" title="var">n</span> (<span class="id" title="var">S1</span> <span class="id" title="var">S2</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.solvable.primitive_action.html#NTransitveProp.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>) <span class="id" title="var">t</span> :<br/> - <a class="idref" href="mathcomp.solvable.primitive_action.html#S1"><span class="id" title="variable">S1</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.solvable.primitive_action.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#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.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.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.solvable.primitive_action.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">dtuple</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#S1"><span class="id" title="variable">S1</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.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.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.solvable.primitive_action.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">dtuple</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#S2"><span class="id" title="variable">S2</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#9437d70414518cee40513da45e8f965b"><span class="id" title="notation">)</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="n_act_add"><span class="id" title="lemma">n_act_add</span></a> <span class="id" title="var">n</span> <span class="id" title="var">x</span> (<span class="id" title="var">t</span> : <a class="idref" href="mathcomp.solvable.primitive_action.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.solvable.primitive_action.html#NTransitveProp.sT"><span class="id" title="variable">sT</span></a>) <span class="id" title="var">a</span> :<br/> - <a class="idref" href="mathcomp.solvable.primitive_action.html#n_act"><span class="id" title="definition">n_act</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#407cde5b61fbf27196d1a7c5a475e083"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#407cde5b61fbf27196d1a7c5a475e083"><span class="id" title="notation">::</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#n_act"><span class="id" title="definition">n_act</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.to"><span class="id" title="variable">to</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#1c05412e4f131fc504427f72854c7514"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="ntransitive0"><span class="id" title="lemma">ntransitive0</span></a> : <a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">transitive</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">^</span></a>0 <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="ntransitive_weak"><span class="id" title="lemma">ntransitive_weak</span></a> <span class="id" title="var">k</span> <span class="id" title="var">m</span> :<br/> - <a class="idref" href="mathcomp.solvable.primitive_action.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#cb53cf0ee22c036a03b4a9281c68b5a3"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#m"><span class="id" title="variable">m</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.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">transitive</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">transitive</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="ntransitive1"><span class="id" title="lemma">ntransitive1</span></a> <span class="id" title="var">m</span> :<br/> - 0 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#00fe0eaf5e6949f0a31725357afa4bba"><span class="id" title="notation"><</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#m"><span class="id" title="variable">m</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.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">transitive</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">transitive</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="ntransitive_primitive"><span class="id" title="lemma">ntransitive_primitive</span></a> <span class="id" title="var">m</span> :<br/> - 1 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#00fe0eaf5e6949f0a31725357afa4bba"><span class="id" title="notation"><</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#m"><span class="id" title="variable">m</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.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">transitive</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">primitive</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#db20e6712a48d61e28e7d8d79ac8def7"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp"><span class="id" title="section">NTransitveProp</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="NTransitveProp1"><span class="id" title="section">NTransitveProp1</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="NTransitveProp1.gT"><span class="id" title="variable">gT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<a name="NTransitveProp1.sT"><span class="id" title="variable">sT</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">Variables</span> (<a name="NTransitveProp1.to"><span class="id" title="variable">to</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">action</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">&-></span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">}</span></a>) (<a name="NTransitveProp1.G"><span class="id" title="variable">G</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) (<a name="NTransitveProp1.S"><span class="id" title="variable">S</span></a> : <a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>).<br/> - -<br/> -</div> - -<div class="doc"> - This is the forward implication of Aschbacher (15.12).1 -</div> -<div class="code"> -<span class="id" title="keyword">Theorem</span> <a name="stab_ntransitive"><span class="id" title="lemma">stab_ntransitive</span></a> <span class="id" title="var">m</span> <span class="id" title="var">x</span> :<br/> - 0 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#00fe0eaf5e6949f0a31725357afa4bba"><span class="id" title="notation"><</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#m"><span class="id" title="variable">m</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.solvable.primitive_action.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.solvable.primitive_action.html#NTransitveProp1.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.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">transitive</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">transitive</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#c91810fcd799fcd960468c603a6be0a6"><span class="id" title="notation">:\</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - This is the converse implication of Aschbacher (15.12).1 -</div> -<div class="code"> -<span class="id" title="keyword">Theorem</span> <a name="stab_ntransitiveI"><span class="id" title="lemma">stab_ntransitiveI</span></a> <span class="id" title="var">m</span> <span class="id" title="var">x</span> :<br/> - <a class="idref" href="mathcomp.solvable.primitive_action.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.solvable.primitive_action.html#NTransitveProp1.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.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">transitive</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">transitive</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#c91810fcd799fcd960468c603a6be0a6"><span class="id" title="notation">:\</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">transitive</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#fb3dbd6f7f05761f6e9db7f43f231a18"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1"><span class="id" title="section">NTransitveProp1</span></a>.<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 |