diff options
Diffstat (limited to 'docs/htmldoc/mathcomp.solvable.finmodule.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.solvable.finmodule.html | 422 |
1 files changed, 422 insertions, 0 deletions
diff --git a/docs/htmldoc/mathcomp.solvable.finmodule.html b/docs/htmldoc/mathcomp.solvable.finmodule.html new file mode 100644 index 0000000..543d986 --- /dev/null +++ b/docs/htmldoc/mathcomp.solvable.finmodule.html @@ -0,0 +1,422 @@ +<!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.finmodule</title> +</head> + +<body> + +<div id="page"> + +<div id="header"> +</div> + +<div id="main"> + +<h1 class="libtitle">Library mathcomp.solvable.finmodule</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"> + This file regroups constructions and results that are based on the most + primitive version of representation theory -- viewing an abelian group as + the additive group of a (finite) Z-module. This includes the Gaschutz + splitting and transitivity theorem, from which we will later derive the + Schur-Zassenhaus theorem and the elementary abelian special case of + Maschke's theorem, the coprime abelian centraliser/commutator trivial + intersection theorem, which is used to show that p-groups under coprime + action factor into special groups, and the construction of the transfer + homomorphism and its expansion relative to a cycle, from which we derive + the Higman Focal Subgroup and the Burnside Normal Complement theorems. + The definitions and lemmas for the finite Z-module induced by an abelian + are packaged in an auxiliary FiniteModule submodule: they should not be + needed much outside this file, which contains all the results that exploit + this construction. + FiniteModule defines the Z[N(A) ]-module associated with a finite abelian + abelian group A, given a proof (abelA : abelian A) : + fmod_of abelA == the type of elements of the module (similar to but + distinct from [subg A]). + fmod abelA x == the injection of x into fmod_of abelA if x \in A, else 0 + fmval u == the projection of u : fmod_of abelA onto A + u ^@ x == the action of x \in 'N(A) on u : fmod_of abelA + The transfer morphism is be constructed from a morphism f : H >-> rT, and + a group G, along with the two assumptions sHG : H \subset G and + abfH : abelian (f @* H): + transfer sGH abfH == the function gT -> FiniteModule.fmod_of abfH that + implements the transfer morphism induced by f on G. + The Lemma transfer_indep states that the transfer morphism can be expanded + using any transversal of the partition HG := rcosets H G of G. + Further, for any g \in G, HG :* < [g]> is also a partition of G (Lemma + rcosets_cycle_partition), and for any transversal X of HG :* < [g]> the + function r mapping x : gT to rcosets (H :* x) < [g]> is (constructively) a + bijection from X to the < [g]>-orbit partition of HG, and Lemma + transfer_pcycle_def gives a simplified expansion of the transfer morphism. +</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> <span class="id" title="var">GRing.Theory</span> <span class="id" title="var">FinRing.Theory</span>.<br/> +<span class="id" title="keyword">Local Open</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">ring_scope</span>.<br/> + +<br/> +<span class="id" title="keyword">Module</span> <a name="FiniteModule"><span class="id" title="module">FiniteModule</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Reserved Notation</span> "u ^@ x" (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 31, <span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>).<br/> + +<br/> +<span class="id" title="keyword">Inductive</span> <a name="FiniteModule.fmod_of"><span class="id" title="inductive">fmod_of</span></a> (<span class="id" title="var">gT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<span class="id" title="var">A</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.finmodule.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">abelA</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#abelian"><span class="id" title="definition">abelian</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#A"><span class="id" title="variable">A</span></a>) :=<br/> + <a name="FiniteModule.Fmod"><span class="id" title="constructor">Fmod</span></a> <span class="id" title="var">x</span> & <a class="idref" href="mathcomp.solvable.finmodule.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.finmodule.html#A"><span class="id" title="variable">A</span></a>.<br/> + +<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="FiniteModule.OneFinMod"><span class="id" title="section">OneFinMod</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Let</span> <a name="FiniteModule.OneFinMod.f2sub"><span class="id" title="variable">f2sub</span></a> (<span class="id" title="var">gT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<span class="id" title="var">A</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.finmodule.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">abA</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#abelian"><span class="id" title="definition">abelian</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#A"><span class="id" title="variable">A</span></a>) :=<br/> + <span class="id" title="keyword">fun</span> <span class="id" title="var">u</span> : <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmod_of"><span class="id" title="inductive">fmod_of</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#abA"><span class="id" title="variable">abA</span></a> ⇒ <span class="id" title="keyword">let</span> : <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.Fmod"><span class="id" title="constructor">Fmod</span></a> <span class="id" title="var">x</span> <span class="id" title="var">Ax</span> := <a class="idref" href="mathcomp.solvable.finmodule.html#u"><span class="id" title="variable">u</span></a> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.fingroup.fingroup.html#Subg"><span class="id" title="constructor">Subg</span></a> <span class="id" title="var">Ax</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#4509b22bf26e3d6d771897e22bd8bc8f"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.arg_sort"><span class="id" title="definition">FinGroup.arg_sort</span></a> <span class="id" title="var">_</span>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="FiniteModule.OneFinMod.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="FiniteModule.OneFinMod.A"><span class="id" title="variable">A</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.finmodule.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<a name="FiniteModule.OneFinMod.abelA"><span class="id" title="variable">abelA</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#abelian"><span class="id" title="definition">abelian</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#A"><span class="id" title="variable">A</span></a>).<br/> +<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">z</span> : <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.OneFinMod.gT"><span class="id" title="variable">gT</span></a>) (<span class="id" title="var">u</span> <span class="id" title="var">v</span> <span class="id" title="var">w</span> : <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmodA"><span class="id" title="abbreviation">fmodA</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Let</span> <a name="FiniteModule.OneFinMod.sub2f"><span class="id" title="variable">sub2f</span></a> (<span class="id" title="var">s</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#201e4acf667e39ca76e3abd16ac27375"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#201e4acf667e39ca76e3abd16ac27375"><span class="id" title="notation">subg</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.OneFinMod.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#201e4acf667e39ca76e3abd16ac27375"><span class="id" title="notation">]</span></a>) := <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.Fmod"><span class="id" title="constructor">Fmod</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.OneFinMod.abelA"><span class="id" title="variable">abelA</span></a> (<a class="idref" href="mathcomp.ssreflect.eqtype.html#valP"><span class="id" title="lemma">valP</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#s"><span class="id" title="variable">s</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="FiniteModule.fmval"><span class="id" title="definition">fmval</span></a> <span class="id" title="var">u</span> := <a class="idref" href="mathcomp.ssreflect.eqtype.html#val"><span class="id" title="projection">val</span></a> (<a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.OneFinMod.f2sub"><span class="id" title="variable">f2sub</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#u"><span class="id" title="variable">u</span></a>).<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">fmod_subType</span> := <a class="idref" href="mathcomp.ssreflect.eqtype.html#341c160c3e7b20d967b85d1852a7f89f"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#341c160c3e7b20d967b85d1852a7f89f"><span class="id" title="notation">subType</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#341c160c3e7b20d967b85d1852a7f89f"><span class="id" title="notation">for</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmval"><span class="id" title="definition">fmval</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#341c160c3e7b20d967b85d1852a7f89f"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="FiniteModule.fmod_eqMixin"><span class="id" title="definition">fmod_eqMixin</span></a> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">eqMixin</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmodA"><span class="id" title="abbreviation">fmodA</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#4bc2d2dce12edef0fb9c71d4a902ae5d"><span class="id" title="notation"><:]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">fmod_eqType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.eqtype.html#Equality.Exports.EqType"><span class="id" title="abbreviation">EqType</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmodA"><span class="id" title="abbreviation">fmodA</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmod_eqMixin"><span class="id" title="definition">fmod_eqMixin</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="FiniteModule.fmod_choiceMixin"><span class="id" title="definition">fmod_choiceMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">choiceMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmodA"><span class="id" title="abbreviation">fmodA</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#6c8b2d90ff1fbb8e9926bbf12495cb70"><span class="id" title="notation"><:]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">fmod_choiceType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Choice.Exports.ChoiceType"><span class="id" title="abbreviation">ChoiceType</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmodA"><span class="id" title="abbreviation">fmodA</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmod_choiceMixin"><span class="id" title="definition">fmod_choiceMixin</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="FiniteModule.fmod_countMixin"><span class="id" title="definition">fmod_countMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">countMixin</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmodA"><span class="id" title="abbreviation">fmodA</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#99c739c8f4212f142296b27d3077c65e"><span class="id" title="notation"><:]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">fmod_countType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#Countable.Exports.CountType"><span class="id" title="abbreviation">CountType</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmodA"><span class="id" title="abbreviation">fmodA</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmod_countMixin"><span class="id" title="definition">fmod_countMixin</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">fmod_subCountType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">subCountType</span></a> <a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmodA"><span class="id" title="abbreviation">fmodA</span></a><a class="idref" href="mathcomp.ssreflect.choice.html#8a7192fa64a42310658fd5be07ae4fcc"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="FiniteModule.fmod_finMixin"><span class="id" title="definition">fmod_finMixin</span></a> := <a class="idref" href="mathcomp.ssreflect.fintype.html#8c180561768185dd10396a5d3615104a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#8c180561768185dd10396a5d3615104a"><span class="id" title="notation">finMixin</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#8c180561768185dd10396a5d3615104a"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmodA"><span class="id" title="abbreviation">fmodA</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#8c180561768185dd10396a5d3615104a"><span class="id" title="notation">by</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#8c180561768185dd10396a5d3615104a"><span class="id" title="notation"><:]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">fmod_finType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.FinType"><span class="id" title="abbreviation">FinType</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmodA"><span class="id" title="abbreviation">fmodA</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmod_finMixin"><span class="id" title="definition">fmod_finMixin</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">fmod_subFinType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">subFinType</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmodA"><span class="id" title="abbreviation">fmodA</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#a701c7b60b4a16f07950761d8bf90924"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="FiniteModule.fmod"><span class="id" title="definition">fmod</span></a> <span class="id" title="var">x</span> := <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.OneFinMod.sub2f"><span class="id" title="variable">sub2f</span></a> (<a class="idref" href="mathcomp.fingroup.fingroup.html#subg"><span class="id" title="definition">subg</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.OneFinMod.A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#x"><span class="id" title="variable">x</span></a>).<br/> +<span class="id" title="keyword">Definition</span> <a name="FiniteModule.actr"><span class="id" title="definition">actr</span></a> <span class="id" title="var">u</span> <span class="id" title="var">x</span> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.solvable.finmodule.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.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.OneFinMod.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">then</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmod"><span class="id" title="definition">fmod</span></a> (<a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmval"><span class="id" title="definition">fmval</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#808c6b8e35e792f23899f360a21e4638"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.solvable.finmodule.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.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">else</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#u"><span class="id" title="variable">u</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="FiniteModule.fmod_opp"><span class="id" title="definition">fmod_opp</span></a> <span class="id" title="var">u</span> := <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.OneFinMod.sub2f"><span class="id" title="variable">sub2f</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a605acbeae7597f74f5a9b816ed8a717"><span class="id" title="notation">^-1</span></a>.<br/> +<span class="id" title="keyword">Definition</span> <a name="FiniteModule.fmod_add"><span class="id" title="definition">fmod_add</span></a> <span class="id" title="var">u</span> <span class="id" title="var">v</span> := <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.OneFinMod.sub2f"><span class="id" title="variable">sub2f</span></a> (<a class="idref" href="mathcomp.solvable.finmodule.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#v"><span class="id" title="variable">v</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Fact</span> <a name="FiniteModule.fmod_add0r"><span class="id" title="lemma">fmod_add0r</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#left_id"><span class="id" title="definition">left_id</span></a> (<a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.OneFinMod.sub2f"><span class="id" title="variable">sub2f</span></a> 1) <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmod_add"><span class="id" title="definition">fmod_add</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Fact</span> <a name="FiniteModule.fmod_addrA"><span class="id" title="lemma">fmod_addrA</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#associative"><span class="id" title="definition">associative</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmod_add"><span class="id" title="definition">fmod_add</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Fact</span> <a name="FiniteModule.fmod_addNr"><span class="id" title="lemma">fmod_addNr</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#left_inverse"><span class="id" title="definition">left_inverse</span></a> (<a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.OneFinMod.sub2f"><span class="id" title="variable">sub2f</span></a> 1) <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmod_opp"><span class="id" title="definition">fmod_opp</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmod_add"><span class="id" title="definition">fmod_add</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Fact</span> <a name="FiniteModule.fmod_addrC"><span class="id" title="lemma">fmod_addrC</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#commutative"><span class="id" title="definition">commutative</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmod_add"><span class="id" title="definition">fmod_add</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="FiniteModule.fmod_zmodMixin"><span class="id" title="definition">fmod_zmodMixin</span></a> := <br/> + <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Zmodule.Exports.ZmodMixin"><span class="id" title="abbreviation">ZmodMixin</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmod_addrA"><span class="id" title="lemma">fmod_addrA</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmod_addrC"><span class="id" title="lemma">fmod_addrC</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmod_add0r"><span class="id" title="lemma">fmod_add0r</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmod_addNr"><span class="id" title="lemma">fmod_addNr</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">fmod_zmodType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Zmodule.Exports.ZmodType"><span class="id" title="abbreviation">ZmodType</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmodA"><span class="id" title="abbreviation">fmodA</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmod_zmodMixin"><span class="id" title="definition">fmod_zmodMixin</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">fmod_finZmodType</span> := <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.finalg.html#2980bb304205aec85bc1eeb5d0a573a5"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#2980bb304205aec85bc1eeb5d0a573a5"><span class="id" title="notation">finZmodType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#2980bb304205aec85bc1eeb5d0a573a5"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmodA"><span class="id" title="abbreviation">fmodA</span></a><a class="idref" href="mathcomp.algebra.finalg.html#2980bb304205aec85bc1eeb5d0a573a5"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">fmod_baseFinGroupType</span> :=<br/> + <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.finalg.html#ee332ddd6e3626489ee70ea4c624f1cd"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#ee332ddd6e3626489ee70ea4c624f1cd"><span class="id" title="notation">baseFinGroupType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#ee332ddd6e3626489ee70ea4c624f1cd"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmodA"><span class="id" title="abbreviation">fmodA</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#ee332ddd6e3626489ee70ea4c624f1cd"><span class="id" title="notation">for</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#ee332ddd6e3626489ee70ea4c624f1cd"><span class="id" title="notation">+%</span></a><a class="idref" href="mathcomp.algebra.finalg.html#ee332ddd6e3626489ee70ea4c624f1cd"><span class="id" title="notation">R</span></a><a class="idref" href="mathcomp.algebra.finalg.html#ee332ddd6e3626489ee70ea4c624f1cd"><span class="id" title="notation">]</span></a>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">fmod_finGroupType</span> :=<br/> + <span class="id" title="keyword">Eval</span> <span class="id" title="tactic">hnf</span> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.algebra.finalg.html#ad4d9ed93eeed8e8e57c81c6e35699c4"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.finalg.html#ad4d9ed93eeed8e8e57c81c6e35699c4"><span class="id" title="notation">finGroupType</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#ad4d9ed93eeed8e8e57c81c6e35699c4"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmodA"><span class="id" title="abbreviation">fmodA</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#ad4d9ed93eeed8e8e57c81c6e35699c4"><span class="id" title="notation">for</span></a> <a class="idref" href="mathcomp.algebra.finalg.html#ad4d9ed93eeed8e8e57c81c6e35699c4"><span class="id" title="notation">+%</span></a><a class="idref" href="mathcomp.algebra.finalg.html#ad4d9ed93eeed8e8e57c81c6e35699c4"><span class="id" title="notation">R</span></a><a class="idref" href="mathcomp.algebra.finalg.html#ad4d9ed93eeed8e8e57c81c6e35699c4"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="FiniteModule.fmodP"><span class="id" title="lemma">fmodP</span></a> <span class="id" title="var">u</span> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#val"><span class="id" title="projection">val</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#u"><span class="id" title="variable">u</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.finmodule.html#FiniteModule.OneFinMod.A"><span class="id" title="variable">A</span></a>. <br/> +<span class="id" title="keyword">Lemma</span> <a name="FiniteModule.fmod_inj"><span class="id" title="lemma">fmod_inj</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.solvable.finmodule.html#FiniteModule.fmval"><span class="id" title="definition">fmval</span></a>. <br/> +<span class="id" title="keyword">Lemma</span> <a name="FiniteModule.congr_fmod"><span class="id" title="lemma">congr_fmod</span></a> <span class="id" title="var">u</span> <span class="id" title="var">v</span> : <a class="idref" href="mathcomp.solvable.finmodule.html#u"><span class="id" title="variable">u</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.finmodule.html#v"><span class="id" title="variable">v</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.finmodule.html#FiniteModule.fmval"><span class="id" title="definition">fmval</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#u"><span class="id" title="variable">u</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.finmodule.html#FiniteModule.fmval"><span class="id" title="definition">fmval</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#v"><span class="id" title="variable">v</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="FiniteModule.fmvalA"><span class="id" title="lemma">fmvalA</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.valA"><span class="id" title="abbreviation">valA</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#ae4d81913e6239182a9ac7467ffde8cd"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">>-></span></a> (<a class="idref" href="mathcomp.solvable.finmodule.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#y"><span class="id" title="variable">y</span></a>)%<span class="id" title="var">g</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">}</span></a>. <br/> +<span class="id" title="keyword">Lemma</span> <a name="FiniteModule.fmvalN"><span class="id" title="lemma">fmvalN</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.valA"><span class="id" title="abbreviation">valA</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#941c6d086004545bd62614d0213e75e5"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.solvable.finmodule.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.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a605acbeae7597f74f5a9b816ed8a717"><span class="id" title="notation">^-1</span></a>%<span class="id" title="var">g</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">}</span></a>. <br/> +<span class="id" title="keyword">Lemma</span> <a name="FiniteModule.fmval0"><span class="id" title="lemma">fmval0</span></a> : <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.valA"><span class="id" title="abbreviation">valA</span></a> 0 <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> 1%<span class="id" title="var">g</span>. <br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">fmval_morphism</span> := @<a class="idref" href="mathcomp.fingroup.morphism.html#Morphism"><span class="id" title="constructor">Morphism</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <a class="idref" href="mathcomp.ssreflect.finset.html#setT"><span class="id" title="abbreviation">setT</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmval"><span class="id" title="definition">fmval</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#in2W"><span class="id" title="lemma">in2W</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmvalA"><span class="id" title="lemma">fmvalA</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="FiniteModule.fmval_sum"><span class="id" title="definition">fmval_sum</span></a> := <a class="idref" href="mathcomp.ssreflect.bigop.html#big_morph"><span class="id" title="lemma">big_morph</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmval"><span class="id" title="definition">fmval</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmvalA"><span class="id" title="lemma">fmvalA</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmval0"><span class="id" title="lemma">fmval0</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="FiniteModule.fmvalZ"><span class="id" title="lemma">fmvalZ</span></a> <span class="id" title="var">n</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.valA"><span class="id" title="abbreviation">valA</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#891e51846c7d1d63a9cb5458374cf308"><span class="id" title="notation">*+</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">>-></span></a> (<a class="idref" href="mathcomp.solvable.finmodule.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#86a04fb564fb97d388cad84a3a204260"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#n"><span class="id" title="variable">n</span></a>)%<span class="id" title="var">g</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="FiniteModule.fmodKcond"><span class="id" title="lemma">fmodKcond</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.eqtype.html#val"><span class="id" title="projection">val</span></a> (<a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmod"><span class="id" title="definition">fmod</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#x"><span class="id" title="variable">x</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.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.solvable.finmodule.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.finmodule.html#FiniteModule.OneFinMod.A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">then</span></a> <a class="idref" href="mathcomp.solvable.finmodule.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.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">else</span></a> 1%<span class="id" title="var">g</span>.<br/> + <span class="id" title="keyword">Lemma</span> <a name="FiniteModule.fmodK"><span class="id" title="lemma">fmodK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.OneFinMod.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#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmod"><span class="id" title="definition">fmod</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#val"><span class="id" title="projection">val</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</span></a>. <br/> +<span class="id" title="keyword">Lemma</span> <a name="FiniteModule.fmvalK"><span class="id" title="lemma">fmvalK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#val"><span class="id" title="projection">val</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmod"><span class="id" title="definition">fmod</span></a>.<br/> + <span class="id" title="keyword">Lemma</span> <a name="FiniteModule.fmod1"><span class="id" title="lemma">fmod1</span></a> : <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmod"><span class="id" title="definition">fmod</span></a> 1 <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> 0. <br/> +<span class="id" title="keyword">Lemma</span> <a name="FiniteModule.fmodM"><span class="id" title="lemma">fmodM</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.OneFinMod.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#2bba53854f326a714d377124cccec593"><span class="id" title="notation">&,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmod"><span class="id" title="definition">fmod</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">/</span></a> (<a class="idref" href="mathcomp.solvable.finmodule.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#y"><span class="id" title="variable">y</span></a>)%<span class="id" title="var">g</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#ae4d81913e6239182a9ac7467ffde8cd"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">}</span></a>.<br/> + <span class="id" title="keyword">Canonical</span> <span class="id" title="var">fmod_morphism</span> := <a class="idref" href="mathcomp.fingroup.morphism.html#Morphism"><span class="id" title="constructor">Morphism</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmodM"><span class="id" title="lemma">fmodM</span></a>.<br/> +<span class="id" title="keyword">Lemma</span> <a name="FiniteModule.fmodX"><span class="id" title="lemma">fmodX</span></a> <span class="id" title="var">n</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.OneFinMod.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#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmod"><span class="id" title="definition">fmod</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">/</span></a> (<a class="idref" href="mathcomp.solvable.finmodule.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#86a04fb564fb97d388cad84a3a204260"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#n"><span class="id" title="variable">n</span></a>)%<span class="id" title="var">g</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#891e51846c7d1d63a9cb5458374cf308"><span class="id" title="notation">*+</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</span></a>.<br/> + <span class="id" title="keyword">Lemma</span> <a name="FiniteModule.fmodV"><span class="id" title="lemma">fmodV</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmod"><span class="id" title="definition">fmod</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a605acbeae7597f74f5a9b816ed8a717"><span class="id" title="notation">^-1</span></a>%<span class="id" title="var">g</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#941c6d086004545bd62614d0213e75e5"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.solvable.finmodule.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.ssrfun.html#59b5bb4add86e1e9ecbe874e74b2216e"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="FiniteModule.injm_fmod"><span class="id" title="lemma">injm_fmod</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#14bfb149f00fa839cfb11397f4fe629f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#14bfb149f00fa839cfb11397f4fe629f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.fmod"><span class="id" title="definition">fmod</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="bc26690a2016cb60816a8e086f236946"><span class="id" title="notation">"</span></a>u ^@ x" := (<a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.actr"><span class="id" title="definition">actr</span></a> <span class="id" title="var">u</span> <span class="id" title="var">x</span>) : <span class="id" title="var">ring_scope</span>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="FiniteModule.fmvalJcond"><span class="id" title="lemma">fmvalJcond</span></a> <span class="id" title="var">u</span> <span class="id" title="var">x</span> :<br/> + <a class="idref" href="mathcomp.ssreflect.eqtype.html#val"><span class="id" title="projection">val</span></a> (<a class="idref" href="mathcomp.solvable.finmodule.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#bc26690a2016cb60816a8e086f236946"><span class="id" title="notation">^@</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#x"><span class="id" title="variable">x</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.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">if</span></a> <a class="idref" href="mathcomp.solvable.finmodule.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.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.OneFinMod.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">then</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#val"><span class="id" title="projection">val</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#808c6b8e35e792f23899f360a21e4638"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.solvable.finmodule.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.ssreflect.html#0348819abaa88c2cd747e8fa60dde7ae"><span class="id" title="notation">else</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#val"><span class="id" title="projection">val</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#u"><span class="id" title="variable">u</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="FiniteModule.fmvalJ"><span class="id" title="lemma">fmvalJ</span></a> <span class="id" title="var">u</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.solvable.finmodule.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.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.OneFinMod.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><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.ssreflect.eqtype.html#val"><span class="id" title="projection">val</span></a> (<a class="idref" href="mathcomp.solvable.finmodule.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#bc26690a2016cb60816a8e086f236946"><span class="id" title="notation">^@</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#x"><span class="id" title="variable">x</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.eqtype.html#val"><span class="id" title="projection">val</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#808c6b8e35e792f23899f360a21e4638"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="FiniteModule.fmodJ"><span class="id" title="lemma">fmodJ</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.solvable.finmodule.html#y"><span class="id" title="variable">y</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.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.OneFinMod.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><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.finmodule.html#FiniteModule.fmod"><span class="id" title="definition">fmod</span></a> (<a class="idref" href="mathcomp.solvable.finmodule.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#808c6b8e35e792f23899f360a21e4638"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#y"><span class="id" title="variable">y</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.finmodule.html#FiniteModule.fmod"><span class="id" title="definition">fmod</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#bc26690a2016cb60816a8e086f236946"><span class="id" title="notation">^@</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#y"><span class="id" title="variable">y</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Fact</span> <a name="FiniteModule.actr_is_action"><span class="id" title="lemma">actr_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.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.OneFinMod.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.actr"><span class="id" title="definition">actr</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">actr_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.finmodule.html#FiniteModule.actr_is_action"><span class="id" title="lemma">actr_is_action</span></a>.<br/> +<span class="id" title="keyword">Notation</span> <a name="7c98bb3aae09ec8defcde60e1fe9fd1a"><span class="id" title="notation">"</span></a>''M'" := <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.actr_action"><span class="id" title="definition">actr_action</span></a> (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8) : <span class="id" title="var">action_scope</span>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="FiniteModule.act0r"><span class="id" title="lemma">act0r</span></a> <span class="id" title="var">x</span> : 0 <a class="idref" href="mathcomp.solvable.finmodule.html#bc26690a2016cb60816a8e086f236946"><span class="id" title="notation">^@</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#x"><span class="id" title="variable">x</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> 0.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="FiniteModule.actAr"><span class="id" title="lemma">actAr</span></a> <span class="id" title="var">x</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.actr"><span class="id" title="definition">actr</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.finmodule.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.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">:</span></a> <span class="id" title="var">u</span> <span class="id" title="var">v</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#ae4d81913e6239182a9ac7467ffde8cd"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#v"><span class="id" title="variable">v</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#3014e73af2a90fd800d8681479d76336"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="FiniteModule.actr_sum"><span class="id" title="definition">actr_sum</span></a> <span class="id" title="var">x</span> := <a class="idref" href="mathcomp.ssreflect.bigop.html#big_morph"><span class="id" title="lemma">big_morph</span></a> <span class="id" title="var">_</span> (<a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.actAr"><span class="id" title="lemma">actAr</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.act0r"><span class="id" title="lemma">act0r</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#x"><span class="id" title="variable">x</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="FiniteModule.actNr"><span class="id" title="lemma">actNr</span></a> <span class="id" title="var">x</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.actr"><span class="id" title="definition">actr</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.finmodule.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.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">:</span></a> <span class="id" title="var">u</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#941c6d086004545bd62614d0213e75e5"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="FiniteModule.actZr"><span class="id" title="lemma">actZr</span></a> <span class="id" title="var">x</span> <span class="id" title="var">n</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.actr"><span class="id" title="definition">actr</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.finmodule.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.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">:</span></a> <span class="id" title="var">u</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#891e51846c7d1d63a9cb5458374cf308"><span class="id" title="notation">*+</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#c3c88e2b30b681cd767a54649faf5973"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Fact</span> <a name="FiniteModule.actr_is_groupAction"><span class="id" title="lemma">actr_is_groupAction</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#is_groupAction"><span class="id" title="definition">is_groupAction</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.finmodule.html#7c98bb3aae09ec8defcde60e1fe9fd1a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.finmodule.html#7c98bb3aae09ec8defcde60e1fe9fd1a"><span class="id" title="notation">M</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">actr_groupAction</span> := <a class="idref" href="mathcomp.fingroup.action.html#GroupAction"><span class="id" title="constructor">GroupAction</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.actr_is_groupAction"><span class="id" title="lemma">actr_is_groupAction</span></a>.<br/> +<span class="id" title="keyword">Notation</span> <a name="fc9edd19efe07e751389113a56e73526"><span class="id" title="notation">"</span></a>''M'" := <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.actr_groupAction"><span class="id" title="definition">actr_groupAction</span></a> (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8) : <span class="id" title="var">groupAction_scope</span>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="FiniteModule.actr1"><span class="id" title="lemma">actr1</span></a> <span class="id" title="var">u</span> : <a class="idref" href="mathcomp.solvable.finmodule.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#bc26690a2016cb60816a8e086f236946"><span class="id" title="notation">^@</span></a> 1 <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.finmodule.html#u"><span class="id" title="variable">u</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="FiniteModule.actrM"><span class="id" title="lemma">actrM</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.OneFinMod.A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">&,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <span class="id" title="var">u</span>, <a class="idref" href="mathcomp.solvable.finmodule.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#bc26690a2016cb60816a8e086f236946"><span class="id" title="notation">^@</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#bc26690a2016cb60816a8e086f236946"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.finmodule.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.solvable.finmodule.html#bc26690a2016cb60816a8e086f236946"><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.finmodule.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#bc26690a2016cb60816a8e086f236946"><span class="id" title="notation">^@</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#bc26690a2016cb60816a8e086f236946"><span class="id" title="notation">^@</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="FiniteModule.actrK"><span class="id" title="lemma">actrK</span></a> <span class="id" title="var">x</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> (<a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.actr"><span class="id" title="definition">actr</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.finmodule.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.actr"><span class="id" title="definition">actr</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.finmodule.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a605acbeae7597f74f5a9b816ed8a717"><span class="id" title="notation">^-1</span></a>%<span class="id" title="var">g</span>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="FiniteModule.actrKV"><span class="id" title="lemma">actrKV</span></a> <span class="id" title="var">x</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#cancel"><span class="id" title="definition">cancel</span></a> (<a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.actr"><span class="id" title="definition">actr</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.finmodule.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a605acbeae7597f74f5a9b816ed8a717"><span class="id" title="notation">^-1</span></a>%<span class="id" title="var">g</span>) (<a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.actr"><span class="id" title="definition">actr</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.finmodule.html#x"><span class="id" title="variable">x</span></a>).<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.OneFinMod"><span class="id" title="section">OneFinMod</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Notation</span> <a name="5265ec8bf0e3eb99e5b993065d871eb7"><span class="id" title="notation">"</span></a>u ^@ x" := (<a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.actr"><span class="id" title="definition">actr</span></a> <span class="id" title="var">u</span> <span class="id" title="var">x</span>) : <span class="id" title="var">ring_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="5f85997305decc6e43bdcd4369b88e63"><span class="id" title="notation">"</span></a>''M'" := <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.actr_action"><span class="id" title="definition">actr_action</span></a> (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 8) : <span class="id" title="var">action_scope</span>.<br/> +<span class="id" title="keyword">Notation</span> <a name="1665aa361c9febc77836f6e34002c85d"><span class="id" title="notation">"</span></a>''M'" := <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule.actr_groupAction"><span class="id" title="definition">actr_groupAction</span></a> : <span class="id" title="var">groupAction_scope</span>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.finmodule.html#FiniteModule"><span class="id" title="module">FiniteModule</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">FiniteModule.fmod_subType</span>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">FiniteModule.fmod_eqType</span>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">FiniteModule.fmod_choiceType</span>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">FiniteModule.fmod_countType</span>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">FiniteModule.fmod_finType</span>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">FiniteModule.fmod_subCountType</span>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">FiniteModule.fmod_subFinType</span>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">FiniteModule.fmod_zmodType</span>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">FiniteModule.fmod_finZmodType</span>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">FiniteModule.fmod_baseFinGroupType</span>.<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">FiniteModule.fmod_finGroupType</span>.<br/> + +<br/> +</div> + +<div class="doc"> + Still allow ring notations, but give priority to groups now. +</div> +<div class="code"> +<span class="id" title="keyword">Import</span> <span class="id" title="var">FiniteModule</span> <span class="id" title="var">GroupScope</span>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="Gaschutz"><span class="id" title="section">Gaschutz</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="Gaschutz.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="Gaschutz.G"><span class="id" title="variable">G</span></a> <a name="Gaschutz.H"><span class="id" title="variable">H</span></a> <a name="Gaschutz.P"><span class="id" title="variable">P</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.finmodule.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>).<br/> +<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">K</span> <span class="id" title="var">L</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.finmodule.html#Gaschutz.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>.<br/> + +<br/> +<span class="id" title="keyword">Hypotheses</span> (<a name="Gaschutz.nsHG"><span class="id" title="variable">nsHG</span></a> : <a class="idref" href="mathcomp.solvable.finmodule.html#Gaschutz.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.finmodule.html#Gaschutz.G"><span class="id" title="variable">G</span></a>) (<a name="Gaschutz.sHP"><span class="id" title="variable">sHP</span></a> : <a class="idref" href="mathcomp.solvable.finmodule.html#Gaschutz.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.solvable.finmodule.html#Gaschutz.P"><span class="id" title="variable">P</span></a>) (<a name="Gaschutz.sPG"><span class="id" title="variable">sPG</span></a> : <a class="idref" href="mathcomp.solvable.finmodule.html#Gaschutz.P"><span class="id" title="variable">P</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.finmodule.html#Gaschutz.G"><span class="id" title="variable">G</span></a>).<br/> +<span class="id" title="keyword">Hypotheses</span> (<a name="Gaschutz.abelH"><span class="id" title="variable">abelH</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#abelian"><span class="id" title="definition">abelian</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Gaschutz.H"><span class="id" title="variable">H</span></a>) (<a name="Gaschutz.coHiPG"><span class="id" title="variable">coHiPG</span></a> : <a class="idref" href="mathcomp.ssreflect.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.finmodule.html#Gaschutz.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.finmodule.html#Gaschutz.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Gaschutz.P"><span class="id" title="variable">P</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">|</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Let</span> <a name="Gaschutz.sHG"><span class="id" title="variable">sHG</span></a> := <a class="idref" href="mathcomp.fingroup.fingroup.html#normal_sub"><span class="id" title="lemma">normal_sub</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Gaschutz.nsHG"><span class="id" title="variable">nsHG</span></a>.<br/> +<span class="id" title="keyword">Let</span> <a name="Gaschutz.nHG"><span class="id" title="variable">nHG</span></a> := <a class="idref" href="mathcomp.ssreflect.fintype.html#subsetP"><span class="id" title="lemma">subsetP</span></a> (<a class="idref" href="mathcomp.fingroup.fingroup.html#normal_norm"><span class="id" title="lemma">normal_norm</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Gaschutz.nsHG"><span class="id" title="variable">nsHG</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Let</span> <a name="Gaschutz.m"><span class="id" title="variable">m</span></a> := (<a class="idref" href="mathcomp.solvable.cyclic.html#expg_invn"><span class="id" title="definition">expg_invn</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Gaschutz.H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.finmodule.html#Gaschutz.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Gaschutz.P"><span class="id" title="variable">P</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">|</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">a</span> <span class="id" title="var">b</span> : <a class="idref" href="mathcomp.solvable.finmodule.html#fmod_of"><span class="id" title="inductive">fmod_of</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Gaschutz.abelH"><span class="id" title="variable">abelH</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Theorem</span> <a name="Gaschutz_split"><span class="id" title="lemma">Gaschutz_split</span></a> : <a class="idref" href="mathcomp.fingroup.gproduct.html#0a7352dd0cab58f1c154ca74b1d45ebb"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.gproduct.html#0a7352dd0cab58f1c154ca74b1d45ebb"><span class="id" title="notation">splits</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Gaschutz.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.gproduct.html#0a7352dd0cab58f1c154ca74b1d45ebb"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#0a7352dd0cab58f1c154ca74b1d45ebb"><span class="id" title="notation">over</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Gaschutz.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.gproduct.html#0a7352dd0cab58f1c154ca74b1d45ebb"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#0a7352dd0cab58f1c154ca74b1d45ebb"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.gproduct.html#0a7352dd0cab58f1c154ca74b1d45ebb"><span class="id" title="notation">splits</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Gaschutz.P"><span class="id" title="variable">P</span></a><a class="idref" href="mathcomp.fingroup.gproduct.html#0a7352dd0cab58f1c154ca74b1d45ebb"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#0a7352dd0cab58f1c154ca74b1d45ebb"><span class="id" title="notation">over</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Gaschutz.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.gproduct.html#0a7352dd0cab58f1c154ca74b1d45ebb"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Theorem</span> <a name="Gaschutz_transitive"><span class="id" title="lemma">Gaschutz_transitive</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#44af7d5c4de43cd8d378a56e587bd9b2"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.gproduct.html#44af7d5c4de43cd8d378a56e587bd9b2"><span class="id" title="notation">complements</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#44af7d5c4de43cd8d378a56e587bd9b2"><span class="id" title="notation">to</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Gaschutz.H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#44af7d5c4de43cd8d378a56e587bd9b2"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Gaschutz.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.gproduct.html#44af7d5c4de43cd8d378a56e587bd9b2"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">&,</span></a><br/> + <span class="id" title="keyword">∀</span> <span class="id" title="var">K</span> <span class="id" title="var">L</span>, <a class="idref" href="mathcomp.solvable.finmodule.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#cb41714a5a23482f7a48a98975fa8c59"><span class="id" title="notation">:&:</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Gaschutz.P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#L"><span class="id" title="variable">L</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#cb41714a5a23482f7a48a98975fa8c59"><span class="id" title="notation">:&:</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Gaschutz.P"><span class="id" title="variable">P</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.finmodule.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.finmodule.html#Gaschutz.H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#L"><span class="id" title="variable">L</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#67291ec55239f54fa5aa0b0bb974446c"><span class="id" title="notation">:=:</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1deb3845cf16de446ae6619879e9d6db"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.finmodule.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#2bba53854f326a714d377124cccec593"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.finmodule.html#Gaschutz"><span class="id" title="section">Gaschutz</span></a>.<br/> + +<br/> +</div> + +<div class="doc"> + This is the TI part of B & G, Proposition 1.6(d). + We go with B & G rather than Aschbacher and will derive 1.6(e) from (d), + rather than the converse, because the derivation of 24.6 from 24.3 in + Aschbacher requires a separate reduction to p-groups to yield 1.6(d), + making it altogether longer than the direct Gaschutz-style proof. + This Lemma is used in maximal.v for the proof of Aschbacher 24.7. +</div> +<div class="code"> +<span class="id" title="keyword">Lemma</span> <a name="coprime_abel_cent_TI"><span class="id" title="lemma">coprime_abel_cent_TI</span></a> (<span class="id" title="var">gT</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<span class="id" title="var">A</span> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) :<br/> + <a class="idref" href="mathcomp.solvable.finmodule.html#A"><span class="id" title="variable">A</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.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.finmodule.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><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.ssreflect.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.finmodule.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.finmodule.html#A"><span class="id" title="variable">A</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#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#abelian"><span class="id" title="definition">abelian</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">C_</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">[~:</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#44ce2df89b693f6f5ca2acfcd54d16b4"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.finmodule.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><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> 1.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="Transfer"><span class="id" title="section">Transfer</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="Transfer.gT"><span class="id" title="variable">gT</span></a> <a name="Transfer.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="Transfer.G"><span class="id" title="variable">G</span></a> <a name="Transfer.H"><span class="id" title="variable">H</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.finmodule.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>).<br/> +<span class="id" title="keyword">Variable</span> <a name="Transfer.alpha"><span class="id" title="variable">alpha</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.aT"><span class="id" title="variable">aT</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Hypotheses</span> (<a name="Transfer.sHG"><span class="id" title="variable">sHG</span></a> : <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.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.solvable.finmodule.html#Transfer.G"><span class="id" title="variable">G</span></a>) (<a name="Transfer.abelA"><span class="id" title="variable">abelA</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#abelian"><span class="id" title="definition">abelian</span></a> (<a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.alpha"><span class="id" title="variable">alpha</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.H"><span class="id" title="variable">H</span></a>)).<br/> + +<br/> + +<br/> +<span class="id" title="keyword">Fact</span> <a name="transfer_morph_subproof"><span class="id" title="lemma">transfer_morph_subproof</span></a> : <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.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.solvable.finmodule.html#Transfer.alpha"><span class="id" title="variable">alpha</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#619a2190d60a66179f3396458e2a09ae"><span class="id" title="notation">@*^-1</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#619a2190d60a66179f3396458e2a09ae"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.alpha"><span class="id" title="variable">alpha</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#48cff845c81518398138031392d44c93"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#619a2190d60a66179f3396458e2a09ae"><span class="id" title="notation">)</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Let</span> <a name="Transfer.fmalpha"><span class="id" title="variable">fmalpha</span></a> := <a class="idref" href="mathcomp.fingroup.morphism.html#restrm"><span class="id" title="definition">restrm</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#transfer_morph_subproof"><span class="id" title="lemma">transfer_morph_subproof</span></a> (<a class="idref" href="mathcomp.solvable.finmodule.html#fmod"><span class="id" title="definition">fmod</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.abelA"><span class="id" title="variable">abelA</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#1b4394c5c1740ef3dc9e4224084970bb"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#1b4394c5c1740ef3dc9e4224084970bb"><span class="id" title="notation">o</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.alpha"><span class="id" title="variable">alpha</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Let</span> <a name="Transfer.V"><span class="id" title="variable">V</span></a> (<span class="id" title="var">rX</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.finmodule.html#Transfer.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a> <a class="idref" href="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.finmodule.html#Transfer.gT"><span class="id" title="variable">gT</span></a>) <span class="id" title="var">g</span> :=<br/> + <a class="idref" href="mathcomp.algebra.ssralg.html#0c791dbdc1655ae690f0a6c159a384c0"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0c791dbdc1655ae690f0a6c159a384c0"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0c791dbdc1655ae690f0a6c159a384c0"><span class="id" title="notation">(</span></a><span class="id" title="var">Hx</span> <a class="idref" href="mathcomp.algebra.ssralg.html#0c791dbdc1655ae690f0a6c159a384c0"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#rcosets"><span class="id" title="definition">rcosets</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0c791dbdc1655ae690f0a6c159a384c0"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.fmalpha"><span class="id" title="variable">fmalpha</span></a> (<a class="idref" href="mathcomp.solvable.finmodule.html#rX"><span class="id" title="variable">rX</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Hx"><span class="id" title="variable">Hx</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#g"><span class="id" title="variable">g</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#a605acbeae7597f74f5a9b816ed8a717"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.finmodule.html#rX"><span class="id" title="variable">rX</span></a> (<a class="idref" href="mathcomp.solvable.finmodule.html#Hx"><span class="id" title="variable">Hx</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#291276ea06db0b00a2747a79d012bbe0"><span class="id" title="notation">:*</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#g"><span class="id" title="variable">g</span></a>)<a class="idref" href="mathcomp.fingroup.fingroup.html#a605acbeae7597f74f5a9b816ed8a717"><span class="id" title="notation">)^-1</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="transfer"><span class="id" title="definition">transfer</span></a> <span class="id" title="var">g</span> := <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.V"><span class="id" title="variable">V</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#repr"><span class="id" title="definition">repr</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#g"><span class="id" title="variable">g</span></a>.<br/> + +<br/> +</div> + +<div class="doc"> + This is Aschbacher (37.2). +</div> +<div class="code"> +<span class="id" title="keyword">Lemma</span> <a name="transferM"><span class="id" title="lemma">transferM</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">&,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">morph</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#transfer"><span class="id" title="definition">transfer</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">:</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">/</span></a> (<a class="idref" href="mathcomp.solvable.finmodule.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#y"><span class="id" title="variable">y</span></a>)%<span class="id" title="var">g</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#ae4d81913e6239182a9ac7467ffde8cd"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#a0fd72584f326d7220475d01d3fceccd"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Canonical</span> <span class="id" title="var">transfer_morphism</span> := <a class="idref" href="mathcomp.fingroup.morphism.html#Morphism"><span class="id" title="constructor">Morphism</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#transferM"><span class="id" title="lemma">transferM</span></a>.<br/> + +<br/> +</div> + +<div class="doc"> + This is Aschbacher (37.1). +</div> +<div class="code"> +<span class="id" title="keyword">Lemma</span> <a name="transfer_indep"><span class="id" title="lemma">transfer_indep</span></a> <span class="id" title="var">X</span> (<span class="id" title="var">rX</span> := <a class="idref" href="mathcomp.ssreflect.finset.html#transversal_repr"><span class="id" title="definition">transversal_repr</span></a> 1 <a class="idref" href="mathcomp.solvable.finmodule.html#X"><span class="id" title="variable">X</span></a>) :<br/> + <a class="idref" href="mathcomp.ssreflect.finset.html#is_transversal"><span class="id" title="definition">is_transversal</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#X"><span class="id" title="variable">X</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#HG"><span class="id" title="abbreviation">HG</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.G"><span class="id" title="variable">G</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#transfer"><span class="id" title="definition">transfer</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrfun.html#2500d48ed8e862ccfda98a44dff88963"><span class="id" title="notation">=1</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.V"><span class="id" title="variable">V</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#rX"><span class="id" title="variable">rX</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="Transfer.FactorTransfer"><span class="id" title="section">FactorTransfer</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variable</span> <a name="Transfer.FactorTransfer.g"><span class="id" title="variable">g</span></a> : <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.gT"><span class="id" title="variable">gT</span></a>.<br/> +<span class="id" title="keyword">Hypothesis</span> <a name="Transfer.FactorTransfer.Gg"><span class="id" title="variable">Gg</span></a> : <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.FactorTransfer.g"><span class="id" title="variable">g</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.finmodule.html#Transfer.G"><span class="id" title="variable">G</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Let</span> <a name="Transfer.FactorTransfer.sgG"><span class="id" title="variable">sgG</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#30152704c0ab4066186d0284456667e8"><span class="id" title="notation"><[</span></a><a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.FactorTransfer.g"><span class="id" title="variable">g</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#30152704c0ab4066186d0284456667e8"><span class="id" title="notation">]></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.finmodule.html#Transfer.G"><span class="id" title="variable">G</span></a>. <br/> +<span class="id" title="keyword">Let</span> <a name="Transfer.FactorTransfer.H_g_rcosets"><span class="id" title="variable">H_g_rcosets</span></a> <span class="id" title="var">x</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.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.finmodule.html#Transfer.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}}</span></a> := <a class="idref" href="mathcomp.fingroup.fingroup.html#rcosets"><span class="id" title="definition">rcosets</span></a> (<a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#291276ea06db0b00a2747a79d012bbe0"><span class="id" title="notation">:*</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="mathcomp.fingroup.fingroup.html#30152704c0ab4066186d0284456667e8"><span class="id" title="notation"><[</span></a><a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.FactorTransfer.g"><span class="id" title="variable">g</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#30152704c0ab4066186d0284456667e8"><span class="id" title="notation">]></span></a>.<br/> +<span class="id" title="keyword">Let</span> <a name="Transfer.FactorTransfer.n_"><span class="id" title="variable">n_</span></a> <span class="id" title="var">x</span> := <a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#30152704c0ab4066186d0284456667e8"><span class="id" title="notation"><[</span></a><a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.FactorTransfer.g"><span class="id" title="variable">g</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#30152704c0ab4066186d0284456667e8"><span class="id" title="notation">]></span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#291276ea06db0b00a2747a79d012bbe0"><span class="id" title="notation">:*</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">|</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="mulg_exp_card_rcosets"><span class="id" title="lemma">mulg_exp_card_rcosets</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.solvable.finmodule.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.FactorTransfer.g"><span class="id" title="variable">g</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#86a04fb564fb97d388cad84a3a204260"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.FactorTransfer.n_"><span class="id" title="variable">n_</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#169fb610eeaa28cebf8ec36928167473"><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.finmodule.html#Transfer.H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#291276ea06db0b00a2747a79d012bbe0"><span class="id" title="notation">:*</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Let</span> <a name="Transfer.FactorTransfer.HGg"><span class="id" title="variable">HGg</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.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.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.finmodule.html#Transfer.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}}}</span></a> := <a class="idref" href="mathcomp.fingroup.action.html#orbit"><span class="id" title="definition">orbit</span></a> <a class="idref" href="mathcomp.fingroup.action.html#45b5ed5ec521d3d65513a2c70294928a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#45b5ed5ec521d3d65513a2c70294928a"><span class="id" title="notation">Rs</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#30152704c0ab4066186d0284456667e8"><span class="id" title="notation"><[</span></a><a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.FactorTransfer.g"><span class="id" title="variable">g</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#30152704c0ab4066186d0284456667e8"><span class="id" title="notation">]></span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#f2bdcb40cf423bf8d54f091f6cec6964"><span class="id" title="notation">@:</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#HG"><span class="id" title="abbreviation">HG</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Let</span> <a name="Transfer.FactorTransfer.partHG"><span class="id" title="variable">partHG</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.finmodule.html#HG"><span class="id" title="abbreviation">HG</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.G"><span class="id" title="variable">G</span></a> := <a class="idref" href="mathcomp.fingroup.fingroup.html#rcosets_partition"><span class="id" title="lemma">rcosets_partition</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.sHG"><span class="id" title="variable">sHG</span></a>.<br/> +<span class="id" title="keyword">Let</span> <a name="Transfer.FactorTransfer.actsgHG"><span class="id" title="variable">actsgHG</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.fingroup.fingroup.html#30152704c0ab4066186d0284456667e8"><span class="id" title="notation"><[</span></a><a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.FactorTransfer.g"><span class="id" title="variable">g</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#30152704c0ab4066186d0284456667e8"><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">on</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#HG"><span class="id" title="abbreviation">HG</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#45b5ed5ec521d3d65513a2c70294928a"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#45b5ed5ec521d3d65513a2c70294928a"><span class="id" title="notation">Rs</span></a><a class="idref" href="mathcomp.fingroup.action.html#4fabb88b896fd67dca370ff89a430b72"><span class="id" title="notation">]</span></a>.<br/> + <span class="id" title="keyword">Let</span> <a name="Transfer.FactorTransfer.partHGg"><span class="id" title="variable">partHGg</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.finmodule.html#Transfer.FactorTransfer.HGg"><span class="id" title="variable">HGg</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#HG"><span class="id" title="abbreviation">HG</span></a> := <a class="idref" href="mathcomp.fingroup.action.html#orbit_partition"><span class="id" title="lemma">orbit_partition</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.FactorTransfer.actsgHG"><span class="id" title="variable">actsgHG</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Let</span> <a name="Transfer.FactorTransfer.injHGg"><span class="id" title="variable">injHGg</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.FactorTransfer.HGg"><span class="id" title="variable">HGg</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">&,</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.finset.html#cover"><span class="id" title="definition">cover</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Let</span> <a name="Transfer.FactorTransfer.defHGg"><span class="id" title="variable">defHGg</span></a> : <a class="idref" href="mathcomp.solvable.finmodule.html#HG"><span class="id" title="abbreviation">HG</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#291276ea06db0b00a2747a79d012bbe0"><span class="id" title="notation">:*</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#30152704c0ab4066186d0284456667e8"><span class="id" title="notation"><[</span></a><a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.FactorTransfer.g"><span class="id" title="variable">g</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#30152704c0ab4066186d0284456667e8"><span class="id" title="notation">]></span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#cover"><span class="id" title="definition">cover</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#f2bdcb40cf423bf8d54f091f6cec6964"><span class="id" title="notation">@:</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.FactorTransfer.HGg"><span class="id" title="variable">HGg</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="rcosets_cycle_partition"><span class="id" title="lemma">rcosets_cycle_partition</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.finmodule.html#HG"><span class="id" title="abbreviation">HG</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#291276ea06db0b00a2747a79d012bbe0"><span class="id" title="notation">:*</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#30152704c0ab4066186d0284456667e8"><span class="id" title="notation"><[</span></a><a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.FactorTransfer.g"><span class="id" title="variable">g</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#30152704c0ab4066186d0284456667e8"><span class="id" title="notation">]></span></a>) <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.G"><span class="id" title="variable">G</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variable</span> <a name="Transfer.FactorTransfer.X"><span class="id" title="variable">X</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.finmodule.html#Transfer.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>.<br/> +<span class="id" title="keyword">Hypothesis</span> <a name="Transfer.FactorTransfer.trX"><span class="id" title="variable">trX</span></a> : <a class="idref" href="mathcomp.ssreflect.finset.html#is_transversal"><span class="id" title="definition">is_transversal</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.FactorTransfer.X"><span class="id" title="variable">X</span></a> (<a class="idref" href="mathcomp.solvable.finmodule.html#HG"><span class="id" title="abbreviation">HG</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#291276ea06db0b00a2747a79d012bbe0"><span class="id" title="notation">:*</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#30152704c0ab4066186d0284456667e8"><span class="id" title="notation"><[</span></a><a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.FactorTransfer.g"><span class="id" title="variable">g</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#30152704c0ab4066186d0284456667e8"><span class="id" title="notation">]></span></a>) <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.G"><span class="id" title="variable">G</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Let</span> <a name="Transfer.FactorTransfer.sXG"><span class="id" title="variable">sXG</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.FactorTransfer.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#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.G"><span class="id" title="variable">G</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">}</span></a>. <br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="rcosets_cycle_transversal"><span class="id" title="lemma">rcosets_cycle_transversal</span></a> : <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.FactorTransfer.H_g_rcosets"><span class="id" title="variable">H_g_rcosets</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#f2bdcb40cf423bf8d54f091f6cec6964"><span class="id" title="notation">@:</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.FactorTransfer.X"><span class="id" title="variable">X</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.finmodule.html#Transfer.FactorTransfer.HGg"><span class="id" title="variable">HGg</span></a>.<br/> + +<br/> + +<br/> +<span class="id" title="keyword">Let</span> <a name="Transfer.FactorTransfer.injHg"><span class="id" title="variable">injHg</span></a>: <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.FactorTransfer.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#2bba53854f326a714d377124cccec593"><span class="id" title="notation">&,</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.solvable.finmodule.html#Transfer.FactorTransfer.H_g_rcosets"><span class="id" title="variable">H_g_rcosets</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="sum_index_rcosets_cycle"><span class="id" title="lemma">sum_index_rcosets_cycle</span></a> : (<a class="idref" href="mathcomp.ssreflect.bigop.html#537ae7c18e428d4642a9dfb8520f03ee"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#537ae7c18e428d4642a9dfb8520f03ee"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#537ae7c18e428d4642a9dfb8520f03ee"><span class="id" title="notation">(</span></a><span class="id" title="var">x</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#537ae7c18e428d4642a9dfb8520f03ee"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.FactorTransfer.X"><span class="id" title="variable">X</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#537ae7c18e428d4642a9dfb8520f03ee"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.FactorTransfer.n_"><span class="id" title="variable">n_</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#x"><span class="id" title="variable">x</span></a>)%<span class="id" title="var">N</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">|</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="transfer_cycle_expansion"><span class="id" title="lemma">transfer_cycle_expansion</span></a> :<br/> + <a class="idref" href="mathcomp.solvable.finmodule.html#transfer"><span class="id" title="definition">transfer</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.FactorTransfer.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#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#0c791dbdc1655ae690f0a6c159a384c0"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0c791dbdc1655ae690f0a6c159a384c0"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0c791dbdc1655ae690f0a6c159a384c0"><span class="id" title="notation">(</span></a><span class="id" title="var">x</span> <a class="idref" href="mathcomp.algebra.ssralg.html#0c791dbdc1655ae690f0a6c159a384c0"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.FactorTransfer.X"><span class="id" title="variable">X</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0c791dbdc1655ae690f0a6c159a384c0"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.fmalpha"><span class="id" title="variable">fmalpha</span></a> (<a class="idref" href="mathcomp.fingroup.fingroup.html#808c6b8e35e792f23899f360a21e4638"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.FactorTransfer.g"><span class="id" title="variable">g</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#86a04fb564fb97d388cad84a3a204260"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.FactorTransfer.n_"><span class="id" title="variable">n_</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#808c6b8e35e792f23899f360a21e4638"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#808c6b8e35e792f23899f360a21e4638"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.solvable.finmodule.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#a605acbeae7597f74f5a9b816ed8a717"><span class="id" title="notation">^-1</span></a>).<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer.FactorTransfer"><span class="id" title="section">FactorTransfer</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.finmodule.html#Transfer"><span class="id" title="section">Transfer</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 |