diff options
| author | Enrico Tassi | 2018-04-20 10:54:22 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-04-20 10:54:22 +0200 |
| commit | ed05182cece6bb3706e09b2ce14af4a41a2e8141 (patch) | |
| tree | e850d7314b6372d0476cf2ffaf7d3830721db7b1 /docs/htmldoc/mathcomp.solvable.primitive_action.html | |
| parent | 3d196f44681fb3b23ff8a79fbd44e12308680531 (diff) | |
generate the documentation for 1.7
Diffstat (limited to 'docs/htmldoc/mathcomp.solvable.primitive_action.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.solvable.primitive_action.html | 244 |
1 files changed, 244 insertions, 0 deletions
diff --git a/docs/htmldoc/mathcomp.solvable.primitive_action.html b/docs/htmldoc/mathcomp.solvable.primitive_action.html new file mode 100644 index 0000000..ee8d1dc --- /dev/null +++ b/docs/htmldoc/mathcomp.solvable.primitive_action.html @@ -0,0 +1,244 @@ +<!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/> +<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#"><span class="id" title="library">mathcomp.ssreflect.ssreflect</span></a>.<br/> + +<br/> +</div> + +<div class="doc"> + 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#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#PrimitiveDef.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><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#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#PrimitiveDef.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><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#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><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#5c606fa2629c1fac8f3ee3f6e9ad2934"><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#5c606fa2629c1fac8f3ee3f6e9ad2934"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#2e9317c5f71a1305fb695cdc49716482"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#2e9317c5f71a1305fb695cdc49716482"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><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#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><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#4fabb88b896fd67dca370ff89a430b72"><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#495b9dab41eed2da7a7d91b1cb8498af"><span class="id" title="notation">^*</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2e9317c5f71a1305fb695cdc49716482"><span class="id" title="notation">&</span></a> 1 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#432e31800fc09abd260feb634dbbd1af"><span class="id" title="notation"><</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#Q"><span class="id" title="variable">Q</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#432e31800fc09abd260feb634dbbd1af"><span class="id" title="notation"><</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#PrimitiveDef.S"><span class="id" title="variable">S</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2e9317c5f71a1305fb695cdc49716482"><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#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><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#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><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#ad5f1da050fedbae022d48bb21530fba"><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#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">&&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">~~</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#e1fcc6c8b4370f06a39f9b1b3c9764b2"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#e1fcc6c8b4370f06a39f9b1b3c9764b2"><span class="id" title="notation">∃</span></a> <span class="id" title="var">Q</span><a class="idref" href="mathcomp.ssreflect.fintype.html#46e5a4123d46e6b126f7788a77176785"><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#e1fcc6c8b4370f06a39f9b1b3c9764b2"><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="bf1de9b65ed5a2d92747e69c4b09154a"><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/> + +<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#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><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#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><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#5c606fa2629c1fac8f3ee3f6e9ad2934"><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#5c606fa2629c1fac8f3ee3f6e9ad2934"><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#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><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#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><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#ad5f1da050fedbae022d48bb21530fba"><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#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.solvable.primitive_action.html#bf1de9b65ed5a2d92747e69c4b09154a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#bf1de9b65ed5a2d92747e69c4b09154a"><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#bf1de9b65ed5a2d92747e69c4b09154a"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#bf1de9b65ed5a2d92747e69c4b09154a"><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#bf1de9b65ed5a2d92747e69c4b09154a"><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#bf1de9b65ed5a2d92747e69c4b09154a"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.gseries.html#maximal_eq"><span class="id" title="definition">maximal_eq</span></a> <a class="idref" href="mathcomp.fingroup.action.html#d6d8c6555a0082b6cbf651a274d2a4d6"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#d6d8c6555a0082b6cbf651a274d2a4d6"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.action.html#d6d8c6555a0082b6cbf651a274d2a4d6"><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#d6d8c6555a0082b6cbf651a274d2a4d6"><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#d6d8c6555a0082b6cbf651a274d2a4d6"><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#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#Primitive.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) :<br/> + <a class="idref" href="mathcomp.solvable.primitive_action.html#bf1de9b65ed5a2d92747e69c4b09154a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#bf1de9b65ed5a2d92747e69c4b09154a"><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#bf1de9b65ed5a2d92747e69c4b09154a"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#bf1de9b65ed5a2d92747e69c4b09154a"><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#bf1de9b65ed5a2d92747e69c4b09154a"><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#bf1de9b65ed5a2d92747e69c4b09154a"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <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#c27c638e534bbb5b7de2d4b4aa0a3e82"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.action.html#652d6cc67746e5361142d90686607781"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#652d6cc67746e5361142d90686607781"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.action.html#652d6cc67746e5361142d90686607781"><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#652d6cc67746e5361142d90686607781"><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#652d6cc67746e5361142d90686607781"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#7a45dffb109c3069e5c675be68643e60"><span class="id" title="notation">∨</span></a> <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><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#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><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#ad5f1da050fedbae022d48bb21530fba"><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#ad5f1da050fedbae022d48bb21530fba"><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#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><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#5c606fa2629c1fac8f3ee3f6e9ad2934"><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#5c606fa2629c1fac8f3ee3f6e9ad2934"><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/8.8.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#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><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#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><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/8.8.0/stdlib//Coq.ssr.ssrfun.html#8f28bbd804547edd8de802d63ef85617"><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#a561cbd02120e729eb821f52665c6080"><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="a34aaddd6f4c8073b4fe8bc7ff30e5ca"><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/8.8.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#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a>) (<a name="NTransitive.S"><span class="id" title="variable">S</span></a> : <a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitive.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><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#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><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#5c606fa2629c1fac8f3ee3f6e9ad2934"><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#5c606fa2629c1fac8f3ee3f6e9ad2934"><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#92573f9b19c03e948cd1a21ac092cb5a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#92573f9b19c03e948cd1a21ac092cb5a"><span class="id" title="notation">set</span></a> <span class="id" title="var">t</span> <a class="idref" href="mathcomp.ssreflect.finset.html#92573f9b19c03e948cd1a21ac092cb5a"><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#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><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#92573f9b19c03e948cd1a21ac092cb5a"><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#92573f9b19c03e948cd1a21ac092cb5a"><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#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><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#92573f9b19c03e948cd1a21ac092cb5a"><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#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><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#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><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#ad5f1da050fedbae022d48bb21530fba"><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#a34aaddd6f4c8073b4fe8bc7ff30e5ca"><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#ad5f1da050fedbae022d48bb21530fba"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.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/8.8.0/stdlib//Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.action.html#f49be8276ad4d3d8f37fd1509306940d"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#f49be8276ad4d3d8f37fd1509306940d"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.action.html#f49be8276ad4d3d8f37fd1509306940d"><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#f49be8276ad4d3d8f37fd1509306940d"><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#f49be8276ad4d3d8f37fd1509306940d"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><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="5f51beb025db273255fdc323c01f6d9b"><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="6abf84fd2a8ca766f4f91521880db61d"><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#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><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#5c606fa2629c1fac8f3ee3f6e9ad2934"><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#5c606fa2629c1fac8f3ee3f6e9ad2934"><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#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<a name="NTransitveProp.S"><span class="id" title="variable">S</span></a> : <a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><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#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#t"><span class="id" title="variable">t</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.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#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#95c7c3a184a96e438da77f66df3029e3"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#95c7c3a184a96e438da77f66df3029e3"><span class="id" title="notation">tuple</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#95c7c3a184a96e438da77f66df3029e3"><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#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><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#d7fed0909a58e41c49e3ee117361b0a5"><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#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><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#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">dtuple</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><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#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2e9317c5f71a1305fb695cdc49716482"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#2e9317c5f71a1305fb695cdc49716482"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#ad6d23746eb1a3b62e52010d3945a1db"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ad6d23746eb1a3b62e52010d3945a1db"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#2e9317c5f71a1305fb695cdc49716482"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><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#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">dtuple</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><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#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2e9317c5f71a1305fb695cdc49716482"><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#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><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#d7fed0909a58e41c49e3ee117361b0a5"><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#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><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#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">dtuple</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><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#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><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/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">&&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><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#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">dtuple</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><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#67a75c8b7ac489919adc46e74581b83e"><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#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><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#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><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#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><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#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">dtuple</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><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#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><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#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><span class="id" title="notation">dtuple</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#5f51beb025db273255fdc323c01f6d9b"><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#5f51beb025db273255fdc323c01f6d9b"><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#d8866adbd4a602b7b4cc275d73486ace"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#d8866adbd4a602b7b4cc275d73486ace"><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#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><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#d7fed0909a58e41c49e3ee117361b0a5"><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#a561cbd02120e729eb821f52665c6080"><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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><span class="id" title="notation">tuple</span></a> <a class="idref" href="mathcomp.ssreflect.tuple.html#a561cbd02120e729eb821f52665c6080"><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#d7fed0909a58e41c49e3ee117361b0a5"><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#a561cbd02120e729eb821f52665c6080"><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#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">transitive</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><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#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><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#6abf84fd2a8ca766f4f91521880db61d"><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#6abf84fd2a8ca766f4f91521880db61d"><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#9b077c369e19739ef880736ba34623ff"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">transitive</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><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#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><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#6abf84fd2a8ca766f4f91521880db61d"><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#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">transitive</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><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#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><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#6abf84fd2a8ca766f4f91521880db61d"><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#6abf84fd2a8ca766f4f91521880db61d"><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#989c98e7ddd65d5bf37c334ff2076de8"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">transitive</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><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#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><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#6abf84fd2a8ca766f4f91521880db61d"><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#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><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#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><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#ad5f1da050fedbae022d48bb21530fba"><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#ad5f1da050fedbae022d48bb21530fba"><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#989c98e7ddd65d5bf37c334ff2076de8"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">transitive</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><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#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><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#6abf84fd2a8ca766f4f91521880db61d"><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#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#bf1de9b65ed5a2d92747e69c4b09154a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#bf1de9b65ed5a2d92747e69c4b09154a"><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#bf1de9b65ed5a2d92747e69c4b09154a"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#bf1de9b65ed5a2d92747e69c4b09154a"><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#bf1de9b65ed5a2d92747e69c4b09154a"><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#bf1de9b65ed5a2d92747e69c4b09154a"><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#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><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#5c606fa2629c1fac8f3ee3f6e9ad2934"><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#5c606fa2629c1fac8f3ee3f6e9ad2934"><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#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<a name="NTransitveProp1.S"><span class="id" title="variable">S</span></a> : <a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#NTransitveProp1.sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><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#989c98e7ddd65d5bf37c334ff2076de8"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">transitive</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><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#361454269931ea8643f7b402f2ab7222"><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#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><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#6abf84fd2a8ca766f4f91521880db61d"><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#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">transitive</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><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#d6d8c6555a0082b6cbf651a274d2a4d6"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#d6d8c6555a0082b6cbf651a274d2a4d6"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.action.html#d6d8c6555a0082b6cbf651a274d2a4d6"><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#d6d8c6555a0082b6cbf651a274d2a4d6"><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#d6d8c6555a0082b6cbf651a274d2a4d6"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><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#67a75c8b7ac489919adc46e74581b83e"><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#6abf84fd2a8ca766f4f91521880db61d"><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#6abf84fd2a8ca766f4f91521880db61d"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><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#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><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#ad5f1da050fedbae022d48bb21530fba"><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#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">transitive</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><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#d6d8c6555a0082b6cbf651a274d2a4d6"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#d6d8c6555a0082b6cbf651a274d2a4d6"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.action.html#d6d8c6555a0082b6cbf651a274d2a4d6"><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#d6d8c6555a0082b6cbf651a274d2a4d6"><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#d6d8c6555a0082b6cbf651a274d2a4d6"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><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#67a75c8b7ac489919adc46e74581b83e"><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#6abf84fd2a8ca766f4f91521880db61d"><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#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">transitive</span></a><a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><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#361454269931ea8643f7b402f2ab7222"><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#6abf84fd2a8ca766f4f91521880db61d"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.primitive_action.html#6abf84fd2a8ca766f4f91521880db61d"><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#6abf84fd2a8ca766f4f91521880db61d"><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#6abf84fd2a8ca766f4f91521880db61d"><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 |