diff options
| author | Cyril Cohen | 2019-10-16 11:26:43 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2019-10-16 11:26:43 +0200 |
| commit | 6b59540a2460633df4e3d8347cb4dfe2fb3a3afb (patch) | |
| tree | 1239c1d5553d51a7d73f2f8b465f6a23178ff8a0 /docs/htmldoc/mathcomp.solvable.frobenius.html | |
| parent | dd82aaeae7e9478efc178ce8430986649555b032 (diff) | |
removing everything but index which redirects to the new page
Diffstat (limited to 'docs/htmldoc/mathcomp.solvable.frobenius.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.solvable.frobenius.html | 437 |
1 files changed, 0 insertions, 437 deletions
diff --git a/docs/htmldoc/mathcomp.solvable.frobenius.html b/docs/htmldoc/mathcomp.solvable.frobenius.html deleted file mode 100644 index 16cd5fa..0000000 --- a/docs/htmldoc/mathcomp.solvable.frobenius.html +++ /dev/null @@ -1,437 +0,0 @@ -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" -"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> -<html xmlns="http://www.w3.org/1999/xhtml"> -<head> -<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> -<link href="coqdoc.css" rel="stylesheet" type="text/css" /> -<title>mathcomp.solvable.frobenius</title> -</head> - -<body> - -<div id="page"> - -<div id="header"> -</div> - -<div id="main"> - -<h1 class="libtitle">Library mathcomp.solvable.frobenius</h1> - -<div class="code"> -<span class="comment">(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. <br/> - Distributed under the terms of CeCILL-B. *)</span><br/> - -<br/> -</div> - -<div class="doc"> - Definition of Frobenius groups, some basic results, and the Frobenius - theorem on the number of solutions of x ^+ n = 1. - semiregular K H <-> - the internal action of H on K is semiregular, i.e., no nontrivial - elements of H and K commute; note that this is actually a symmetric - condition. - semiprime K H <-> - the internal action of H on K is "prime", i.e., an element of K that - centralises a nontrivial element of H must centralise all of H. - normedTI A G L <=> - A is nonempty, strictly disjoint from its conjugates in G, and has - normaliser L in G. - [Frobenius G = K ><| H] <=> - G is (isomorphic to) a Frobenius group with kernel K and complement - H. This is an effective predicate (in bool), which tests the - equality with the semidirect product, and then the fact that H is a - proper self-normalizing TI-subgroup of G. - [Frobenius G with kernel H] <=> - G is (isomorphic to) a Frobenius group with kernel K; same as above, - but without the semi-direct product. - [Frobenius G with complement H] <=> - G is (isomorphic to) a Frobenius group with complement H; same as - above, but without the semi-direct product. The proof that this form - is equivalent to the above (i.e., the existence of Frobenius - kernels) requires character theory and will only be proved in the - vcharacter.v file. - [Frobenius G] <=> G is a Frobenius group. - Frobenius_action G H S to <-> - The action to of G on S defines an isomorphism of G with a - (permutation) Frobenius group, i.e., to is faithful and transitive - on S, no nontrivial element of G fixes more than one point in S, and - H is the stabilizer of some element of S, and non-trivial. Thus, - Frobenius_action G H S 'P - asserts that G is a Frobenius group in the classic sense. - has_Frobenius_action G H <-> - Frobenius_action G H S to holds for some sT : finType, S : {set st} - and to : {action gT &-> sT}. This is a predicate in Prop, but is - exactly reflected by [Frobenius G with complement H] : bool. -</div> -<div class="code"> - -<br/> -<span class="id" title="keyword">Set Implicit Arguments</span>.<br/> - -<br/> -<span class="id" title="keyword">Import</span> <span class="id" title="var">GroupScope</span>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="Definitions"><span class="id" title="section">Definitions</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="Definitions.gT"><span class="id" title="variable">gT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>.<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">A</span> <span class="id" title="var">G</span> <span class="id" title="var">K</span> <span class="id" title="var">H</span> <span class="id" title="var">L</span> : <a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#Definitions.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - Corresponds to "H acts on K in a regular manner" in B & G. -</div> -<div class="code"> -<span class="id" title="keyword">Definition</span> <a name="semiregular"><span class="id" title="definition">semiregular</span></a> <span class="id" title="var">K</span> <span class="id" title="var">H</span> := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ca7f9c8131cd704a6703ad86f415c132"><span class="id" title="notation">^#</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">C_K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 1<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -</div> - -<div class="doc"> - Corresponds to "H acts on K in a prime manner" in B & G. -</div> -<div class="code"> -<span class="id" title="keyword">Definition</span> <a name="semiprime"><span class="id" title="definition">semiprime</span></a> <span class="id" title="var">K</span> <span class="id" title="var">H</span> := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ca7f9c8131cd704a6703ad86f415c132"><span class="id" title="notation">^#</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">C_K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">C_K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="normedTI"><span class="id" title="definition">normedTI</span></a> <span class="id" title="var">A</span> <span class="id" title="var">G</span> <span class="id" title="var">L</span> := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5a7d806905be2a0d04047156433535f1"><span class="id" title="notation">[&&</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#set0"><span class="id" title="definition">set0</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5a7d806905be2a0d04047156433535f1"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#trivIset"><span class="id" title="definition">trivIset</span></a> (<a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#9034a9c14f90b74fd311ece73a2afd4b"><span class="id" title="notation">:^:</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5a7d806905be2a0d04047156433535f1"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#ee98cf35a816a182ecdf169a5f07c7f5"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ee98cf35a816a182ecdf169a5f07c7f5"><span class="id" title="notation">N_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ee98cf35a816a182ecdf169a5f07c7f5"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ee98cf35a816a182ecdf169a5f07c7f5"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#L"><span class="id" title="variable">L</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5a7d806905be2a0d04047156433535f1"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="Frobenius_group_with_complement"><span class="id" title="definition">Frobenius_group_with_complement</span></a> <span class="id" title="var">G</span> <span class="id" title="var">H</span> := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">&&</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#normedTI"><span class="id" title="definition">normedTI</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ca7f9c8131cd704a6703ad86f415c132"><span class="id" title="notation">^#</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="Frobenius_group"><span class="id" title="definition">Frobenius_group</span></a> <span class="id" title="var">G</span> :=<br/> - <a class="idref" href="mathcomp.ssreflect.fintype.html#9b7547477b3531f14d89d6b13ad78482"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#9b7547477b3531f14d89d6b13ad78482"><span class="id" title="notation">∃</span></a> <span class="id" title="var">H</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#9b7547477b3531f14d89d6b13ad78482"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#Definitions.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f3be25edeb0349b0a76405eded9d0b98"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#Frobenius_group_with_complement"><span class="id" title="definition">Frobenius_group_with_complement</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#9b7547477b3531f14d89d6b13ad78482"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="Frobenius_group_with_kernel_and_complement"><span class="id" title="definition">Frobenius_group_with_kernel_and_complement</span></a> <span class="id" title="var">G</span> <span class="id" title="var">K</span> <span class="id" title="var">H</span> :=<br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#4c7b411f14f1faa861c7c0ade82faf76"><span class="id" title="notation">><|</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">&&</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#Frobenius_group_with_complement"><span class="id" title="definition">Frobenius_group_with_complement</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="Frobenius_group_with_kernel"><span class="id" title="definition">Frobenius_group_with_kernel</span></a> <span class="id" title="var">G</span> <span class="id" title="var">K</span> :=<br/> - <a class="idref" href="mathcomp.ssreflect.fintype.html#9b7547477b3531f14d89d6b13ad78482"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#9b7547477b3531f14d89d6b13ad78482"><span class="id" title="notation">∃</span></a> <span class="id" title="var">H</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#9b7547477b3531f14d89d6b13ad78482"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#Definitions.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f3be25edeb0349b0a76405eded9d0b98"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#Frobenius_group_with_kernel_and_complement"><span class="id" title="definition">Frobenius_group_with_kernel_and_complement</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#9b7547477b3531f14d89d6b13ad78482"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="Definitions.FrobeniusAction"><span class="id" title="section">FrobeniusAction</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> <a name="Definitions.FrobeniusAction.G"><span class="id" title="variable">G</span></a> <a name="Definitions.FrobeniusAction.H"><span class="id" title="variable">H</span></a> : <a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#Definitions.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>.<br/> -<span class="id" title="keyword">Variables</span> (<a name="Definitions.FrobeniusAction.sT"><span class="id" title="variable">sT</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#Finite.Exports.finType"><span class="id" title="abbreviation">finType</span></a>) (<a name="Definitions.FrobeniusAction.S"><span class="id" title="variable">S</span></a> : <a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>) (<a name="Definitions.FrobeniusAction.to"><span class="id" title="variable">to</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">action</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#Definitions.gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">&-></span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.fingroup.action.html#5567a34191268487a9ef0120f668a04c"><span class="id" title="notation">}</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="Frobenius_action"><span class="id" title="definition">Frobenius_action</span></a> :=<br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b76985613d3b3ca583bb3217c76109bb"><span class="id" title="notation">[/\</span></a> <a class="idref" href="mathcomp.fingroup.action.html#b33bbd7f4609361a5f6c220c33141a0c"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#b33bbd7f4609361a5f6c220c33141a0c"><span class="id" title="notation">faithful</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#Definitions.FrobeniusAction.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.action.html#b33bbd7f4609361a5f6c220c33141a0c"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#b33bbd7f4609361a5f6c220c33141a0c"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#Definitions.FrobeniusAction.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.action.html#b33bbd7f4609361a5f6c220c33141a0c"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#Definitions.FrobeniusAction.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#b33bbd7f4609361a5f6c220c33141a0c"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b76985613d3b3ca583bb3217c76109bb"><span class="id" title="notation">,</span></a><br/> - <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">transitive</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#Definitions.FrobeniusAction.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#Definitions.FrobeniusAction.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#Definitions.FrobeniusAction.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#7ff4d7c306e2eb723a4b0e54810870ae"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b76985613d3b3ca583bb3217c76109bb"><span class="id" title="notation">,</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#Definitions.FrobeniusAction.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ca7f9c8131cd704a6703ad86f415c132"><span class="id" title="notation">^#</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.fingroup.action.html#2bb94d3d01f9b00932888c009233b945"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#2bb94d3d01f9b00932888c009233b945"><span class="id" title="notation">Fix_</span></a><a class="idref" href="mathcomp.fingroup.action.html#2bb94d3d01f9b00932888c009233b945"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#Definitions.FrobeniusAction.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.action.html#2bb94d3d01f9b00932888c009233b945"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#Definitions.FrobeniusAction.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#2bb94d3d01f9b00932888c009233b945"><span class="id" title="notation">)[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.action.html#2bb94d3d01f9b00932888c009233b945"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#cb53cf0ee22c036a03b4a9281c68b5a3"><span class="id" title="notation">≤</span></a> 1<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b76985613d3b3ca583bb3217c76109bb"><span class="id" title="notation">,</span></a><br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#Definitions.FrobeniusAction.H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 1<br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b76985613d3b3ca583bb3217c76109bb"><span class="id" title="notation">&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">u</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#Definitions.FrobeniusAction.S"><span class="id" title="variable">S</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#Definitions.FrobeniusAction.H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#Definitions.FrobeniusAction.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#395ebe95a73fc3c95c78bb1b65adcef4"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b76985613d3b3ca583bb3217c76109bb"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.frobenius.html#Definitions.FrobeniusAction"><span class="id" title="section">FrobeniusAction</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variant</span> <a name="has_Frobenius_action"><span class="id" title="inductive">has_Frobenius_action</span></a> <span class="id" title="var">G</span> <span class="id" title="var">H</span> : <span class="id" title="keyword">Prop</span> :=<br/> - <a name="HasFrobeniusAction"><span class="id" title="constructor">HasFrobeniusAction</span></a> <span class="id" title="var">sT</span> <span class="id" title="var">S</span> <span class="id" title="var">to</span> <span class="id" title="keyword">of</span> @<a class="idref" href="mathcomp.solvable.frobenius.html#Frobenius_action"><span class="id" title="definition">Frobenius_action</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#sT"><span class="id" title="variable">sT</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#to"><span class="id" title="variable">to</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.frobenius.html#Definitions"><span class="id" title="section">Definitions</span></a>.<br/> - -<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="73516a680e9150542d49d1098b491775"><span class="id" title="notation">"</span></a>[ 'Frobenius' G 'with' 'complement' H ]" :=<br/> - (<a class="idref" href="mathcomp.solvable.frobenius.html#Frobenius_group_with_complement"><span class="id" title="definition">Frobenius_group_with_complement</span></a> <span class="id" title="var">G</span> <span class="id" title="var">H</span>)<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">G</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 50, <span class="id" title="var">H</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 35,<br/> - <span class="id" title="var">format</span> "[ 'Frobenius' G 'with' 'complement' H ]") : <span class="id" title="var">group_scope</span>.<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">"</span></a>[ 'Frobenius' G 'with' 'kernel' K ]" :=<br/> - (<a class="idref" href="mathcomp.solvable.frobenius.html#Frobenius_group_with_kernel"><span class="id" title="definition">Frobenius_group_with_kernel</span></a> <span class="id" title="var">G</span> <span class="id" title="var">K</span>)<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">G</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 50, <span class="id" title="var">K</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 35,<br/> - <span class="id" title="var">format</span> "[ 'Frobenius' G 'with' 'kernel' K ]") : <span class="id" title="var">group_scope</span>.<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="09bb2faa2af76eddba9b801e0b61cec9"><span class="id" title="notation">"</span></a>[ 'Frobenius' G ]" :=<br/> - (<a class="idref" href="mathcomp.solvable.frobenius.html#Frobenius_group"><span class="id" title="definition">Frobenius_group</span></a> <span class="id" title="var">G</span>)<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">G</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 50,<br/> - <span class="id" title="var">format</span> "[ 'Frobenius' G ]") : <span class="id" title="var">group_scope</span>.<br/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">"</span></a>[ 'Frobenius' G = K ><| H ]" :=<br/> - (<a class="idref" href="mathcomp.solvable.frobenius.html#Frobenius_group_with_kernel_and_complement"><span class="id" title="definition">Frobenius_group_with_kernel_and_complement</span></a> <span class="id" title="var">G</span> <span class="id" title="var">K</span> <span class="id" title="var">H</span>)<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 0, <span class="id" title="var">G</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 50, <span class="id" title="var">K</span>, <span class="id" title="var">H</span> <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 35,<br/> - <span class="id" title="var">format</span> "[ 'Frobenius' G = K ><| H ]") : <span class="id" title="var">group_scope</span>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="FrobeniusBasics"><span class="id" title="section">FrobeniusBasics</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="FrobeniusBasics.gT"><span class="id" title="variable">gT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>.<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">A</span> <span class="id" title="var">B</span> : <a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#d8708f36d374a98f4d683c7593d1ea6a"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">G</span> <span class="id" title="var">H</span> <span class="id" title="var">K</span> <span class="id" title="var">L</span> <span class="id" title="var">R</span> <span class="id" title="var">X</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="semiregular1l"><span class="id" title="lemma">semiregular1l</span></a> <span class="id" title="var">H</span> : <a class="idref" href="mathcomp.solvable.frobenius.html#semiregular"><span class="id" title="definition">semiregular</span></a> 1 <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="semiregular1r"><span class="id" title="lemma">semiregular1r</span></a> <span class="id" title="var">K</span> : <a class="idref" href="mathcomp.solvable.frobenius.html#semiregular"><span class="id" title="definition">semiregular</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> 1.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="semiregular_sym"><span class="id" title="lemma">semiregular_sym</span></a> <span class="id" title="var">H</span> <span class="id" title="var">K</span> : <a class="idref" href="mathcomp.solvable.frobenius.html#semiregular"><span class="id" title="definition">semiregular</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#semiregular"><span class="id" title="definition">semiregular</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="semiregularS"><span class="id" title="lemma">semiregularS</span></a> <span class="id" title="var">K1</span> <span class="id" title="var">K2</span> <span class="id" title="var">A1</span> <span class="id" title="var">A2</span> :<br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#K1"><span class="id" title="variable">K1</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K2"><span class="id" title="variable">K2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A1"><span class="id" title="variable">A1</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A2"><span class="id" title="variable">A2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#semiregular"><span class="id" title="definition">semiregular</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K2"><span class="id" title="variable">K2</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A2"><span class="id" title="variable">A2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#semiregular"><span class="id" title="definition">semiregular</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K1"><span class="id" title="variable">K1</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A1"><span class="id" title="variable">A1</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="semiregular_prime"><span class="id" title="lemma">semiregular_prime</span></a> <span class="id" title="var">H</span> <span class="id" title="var">K</span> : <a class="idref" href="mathcomp.solvable.frobenius.html#semiregular"><span class="id" title="definition">semiregular</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#semiprime"><span class="id" title="definition">semiprime</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="semiprime_regular"><span class="id" title="lemma">semiprime_regular</span></a> <span class="id" title="var">H</span> <span class="id" title="var">K</span> : <a class="idref" href="mathcomp.solvable.frobenius.html#semiprime"><span class="id" title="definition">semiprime</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">C_K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#semiregular"><span class="id" title="definition">semiregular</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="semiprimeS"><span class="id" title="lemma">semiprimeS</span></a> <span class="id" title="var">K1</span> <span class="id" title="var">K2</span> <span class="id" title="var">A1</span> <span class="id" title="var">A2</span> :<br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#K1"><span class="id" title="variable">K1</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K2"><span class="id" title="variable">K2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A1"><span class="id" title="variable">A1</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A2"><span class="id" title="variable">A2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#semiprime"><span class="id" title="definition">semiprime</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K2"><span class="id" title="variable">K2</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A2"><span class="id" title="variable">A2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#semiprime"><span class="id" title="definition">semiprime</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K1"><span class="id" title="variable">K1</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A1"><span class="id" title="variable">A1</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="cent_semiprime"><span class="id" title="lemma">cent_semiprime</span></a> <span class="id" title="var">H</span> <span class="id" title="var">K</span> <span class="id" title="var">X</span> :<br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#semiprime"><span class="id" title="definition">semiprime</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#X"><span class="id" title="variable">X</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#X"><span class="id" title="variable">X</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#be2f022a539ec6d4d51932b5ea998e57"><span class="id" title="notation">:!=:</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">C_K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#X"><span class="id" title="variable">X</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">C_K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">)</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="stab_semiprime"><span class="id" title="lemma">stab_semiprime</span></a> <span class="id" title="var">H</span> <span class="id" title="var">K</span> <span class="id" title="var">X</span> :<br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#semiprime"><span class="id" title="definition">semiprime</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#X"><span class="id" title="variable">X</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">C_H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#X"><span class="id" title="variable">X</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">C_H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#X"><span class="id" title="variable">X</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="cent_semiregular"><span class="id" title="lemma">cent_semiregular</span></a> <span class="id" title="var">H</span> <span class="id" title="var">K</span> <span class="id" title="var">X</span> :<br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#semiregular"><span class="id" title="definition">semiregular</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#X"><span class="id" title="variable">X</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#X"><span class="id" title="variable">X</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#be2f022a539ec6d4d51932b5ea998e57"><span class="id" title="notation">:!=:</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">C_K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#X"><span class="id" title="variable">X</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 1.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="regular_norm_dvd_pred"><span class="id" title="lemma">regular_norm_dvd_pred</span></a> <span class="id" title="var">K</span> <span class="id" title="var">H</span> :<br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#semiregular"><span class="id" title="definition">semiregular</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#bde82eab2fe4a0799bc2419e587505d4"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f953bf7095e0da1cb644443fd0e17d6d"><span class="id" title="notation">.-1</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="regular_norm_coprime"><span class="id" title="lemma">regular_norm_coprime</span></a> <span class="id" title="var">K</span> <span class="id" title="var">H</span> :<br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#semiregular"><span class="id" title="definition">semiregular</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="semiregularJ"><span class="id" title="lemma">semiregularJ</span></a> <span class="id" title="var">K</span> <span class="id" title="var">H</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.solvable.frobenius.html#semiregular"><span class="id" title="definition">semiregular</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#semiregular"><span class="id" title="definition">semiregular</span></a> (<a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#x"><span class="id" title="variable">x</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="semiprimeJ"><span class="id" title="lemma">semiprimeJ</span></a> <span class="id" title="var">K</span> <span class="id" title="var">H</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.solvable.frobenius.html#semiprime"><span class="id" title="definition">semiprime</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#semiprime"><span class="id" title="definition">semiprime</span></a> (<a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#x"><span class="id" title="variable">x</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="normedTI_P"><span class="id" title="lemma">normedTI_P</span></a> <span class="id" title="var">A</span> <span class="id" title="var">G</span> <span class="id" title="var">L</span> : <br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">[/\</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#set0"><span class="id" title="definition">set0</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#L"><span class="id" title="variable">L</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#ee98cf35a816a182ecdf169a5f07c7f5"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ee98cf35a816a182ecdf169a5f07c7f5"><span class="id" title="notation">N_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ee98cf35a816a182ecdf169a5f07c7f5"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ee98cf35a816a182ecdf169a5f07c7f5"><span class="id" title="notation">)</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">g</span>, <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b3ebd0deddd84fd60e149cb5ef719351"><span class="id" title="notation">~~</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#1c170b7d9dd618ec64d5610e390a3afe"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#1c170b7d9dd618ec64d5610e390a3afe"><span class="id" title="notation">disjoint</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#1c170b7d9dd618ec64d5610e390a3afe"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#g"><span class="id" title="variable">g</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#1c170b7d9dd618ec64d5610e390a3afe"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#g"><span class="id" title="variable">g</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#L"><span class="id" title="variable">L</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">]</span></a><br/> - (<a class="idref" href="mathcomp.solvable.frobenius.html#normedTI"><span class="id" title="definition">normedTI</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#L"><span class="id" title="variable">L</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="normedTI_memJ_P"><span class="id" title="lemma">normedTI_memJ_P</span></a> <span class="id" title="var">A</span> <span class="id" title="var">G</span> <span class="id" title="var">L</span> :<br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">[/\</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#set0"><span class="id" title="definition">set0</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#L"><span class="id" title="variable">L</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5f76d9959f82823e4253cd67e7dc0e96"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5f76d9959f82823e4253cd67e7dc0e96"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5f76d9959f82823e4253cd67e7dc0e96"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5f76d9959f82823e4253cd67e7dc0e96"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">a</span> <span class="id" title="var">g</span>, <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#a"><span class="id" title="variable">a</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#746f7e4d3218aa2699eefc064b513fc2"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#g"><span class="id" title="variable">g</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#g"><span class="id" title="variable">g</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#L"><span class="id" title="variable">L</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5f76d9959f82823e4253cd67e7dc0e96"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">]</span></a><br/> - (<a class="idref" href="mathcomp.solvable.frobenius.html#normedTI"><span class="id" title="definition">normedTI</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#L"><span class="id" title="variable">L</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="partition_class_support"><span class="id" title="lemma">partition_class_support</span></a> <span class="id" title="var">A</span> <span class="id" title="var">G</span> :<br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#set0"><span class="id" title="definition">set0</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#trivIset"><span class="id" title="definition">trivIset</span></a> (<a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#9034a9c14f90b74fd311ece73a2afd4b"><span class="id" title="notation">:^:</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#partition"><span class="id" title="definition">partition</span></a> (<a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#9034a9c14f90b74fd311ece73a2afd4b"><span class="id" title="notation">:^:</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a>) (<a class="idref" href="mathcomp.fingroup.fingroup.html#class_support"><span class="id" title="definition">class_support</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="partition_normedTI"><span class="id" title="lemma">partition_normedTI</span></a> <span class="id" title="var">A</span> <span class="id" title="var">G</span> <span class="id" title="var">L</span> :<br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#normedTI"><span class="id" title="definition">normedTI</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#L"><span class="id" title="variable">L</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#partition"><span class="id" title="definition">partition</span></a> (<a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#9034a9c14f90b74fd311ece73a2afd4b"><span class="id" title="notation">:^:</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a>) (<a class="idref" href="mathcomp.fingroup.fingroup.html#class_support"><span class="id" title="definition">class_support</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="card_support_normedTI"><span class="id" title="lemma">card_support_normedTI</span></a> <span class="id" title="var">A</span> <span class="id" title="var">G</span> <span class="id" title="var">L</span> :<br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#normedTI"><span class="id" title="definition">normedTI</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#L"><span class="id" title="variable">L</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#class_support"><span class="id" title="definition">class_support</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> (<a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ea2ff3d561159081cea6fb2e8113cc54"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#L"><span class="id" title="variable">L</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">|</span></a>)%<span class="id" title="var">N</span>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="normedTI_S"><span class="id" title="lemma">normedTI_S</span></a> <span class="id" title="var">A</span> <span class="id" title="var">B</span> <span class="id" title="var">G</span> <span class="id" title="var">L</span> : <br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#set0"><span class="id" title="definition">set0</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#L"><span class="id" title="variable">L</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#B"><span class="id" title="variable">B</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#normedTI"><span class="id" title="definition">normedTI</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#B"><span class="id" title="variable">B</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#L"><span class="id" title="variable">L</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#normedTI"><span class="id" title="definition">normedTI</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#L"><span class="id" title="variable">L</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="cent1_normedTI"><span class="id" title="lemma">cent1_normedTI</span></a> <span class="id" title="var">A</span> <span class="id" title="var">G</span> <span class="id" title="var">L</span> :<br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#normedTI"><span class="id" title="definition">normedTI</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#L"><span class="id" title="variable">L</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#L"><span class="id" title="variable">L</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Frobenius_actionP"><span class="id" title="lemma">Frobenius_actionP</span></a> <span class="id" title="var">G</span> <span class="id" title="var">H</span> :<br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="mathcomp.solvable.frobenius.html#has_Frobenius_action"><span class="id" title="inductive">has_Frobenius_action</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a>) <a class="idref" href="mathcomp.solvable.frobenius.html#73516a680e9150542d49d1098b491775"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#73516a680e9150542d49d1098b491775"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#73516a680e9150542d49d1098b491775"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#73516a680e9150542d49d1098b491775"><span class="id" title="notation">complement</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#73516a680e9150542d49d1098b491775"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="FrobeniusBasics.FrobeniusProperties"><span class="id" title="section">FrobeniusProperties</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> <a name="FrobeniusBasics.FrobeniusProperties.G"><span class="id" title="variable">G</span></a> <a name="FrobeniusBasics.FrobeniusProperties.H"><span class="id" title="variable">H</span></a> <a name="FrobeniusBasics.FrobeniusProperties.K"><span class="id" title="variable">K</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>.<br/> -<span class="id" title="keyword">Hypothesis</span> <a name="FrobeniusBasics.FrobeniusProperties.frobG"><span class="id" title="variable">frobG</span></a> : <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">><|</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="FrobeniusWker"><span class="id" title="lemma">FrobeniusWker</span></a> : <a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">kernel</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="FrobeniusWcompl"><span class="id" title="lemma">FrobeniusWcompl</span></a> : <a class="idref" href="mathcomp.solvable.frobenius.html#73516a680e9150542d49d1098b491775"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#73516a680e9150542d49d1098b491775"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#73516a680e9150542d49d1098b491775"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#73516a680e9150542d49d1098b491775"><span class="id" title="notation">complement</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#73516a680e9150542d49d1098b491775"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="FrobeniusW"><span class="id" title="lemma">FrobeniusW</span></a> : <a class="idref" href="mathcomp.solvable.frobenius.html#09bb2faa2af76eddba9b801e0b61cec9"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#09bb2faa2af76eddba9b801e0b61cec9"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#09bb2faa2af76eddba9b801e0b61cec9"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Frobenius_context"><span class="id" title="lemma">Frobenius_context</span></a> :<br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b76985613d3b3ca583bb3217c76109bb"><span class="id" title="notation">[/\</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#4c7b411f14f1faa861c7c0ade82faf76"><span class="id" title="notation">><|</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.G"><span class="id" title="variable">G</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b76985613d3b3ca583bb3217c76109bb"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#be2f022a539ec6d4d51932b5ea998e57"><span class="id" title="notation">:!=:</span></a> 1<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b76985613d3b3ca583bb3217c76109bb"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#be2f022a539ec6d4d51932b5ea998e57"><span class="id" title="notation">:!=:</span></a> 1<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b76985613d3b3ca583bb3217c76109bb"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f8a5284fd4c86e7670efa54241b49929"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f8a5284fd4c86e7670efa54241b49929"><span class="id" title="notation">proper</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b76985613d3b3ca583bb3217c76109bb"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f8a5284fd4c86e7670efa54241b49929"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f8a5284fd4c86e7670efa54241b49929"><span class="id" title="notation">proper</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.G"><span class="id" title="variable">G</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b76985613d3b3ca583bb3217c76109bb"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Frobenius_partition"><span class="id" title="lemma">Frobenius_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.fingroup.fingroup.html#gval"><span class="id" title="projection">gval</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#c07c66784631827a3968dee93baba0d0"><span class="id" title="notation">|:</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#c07c66784631827a3968dee93baba0d0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ca7f9c8131cd704a6703ad86f415c132"><span class="id" title="notation">^#</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#9034a9c14f90b74fd311ece73a2afd4b"><span class="id" title="notation">:^:</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#c07c66784631827a3968dee93baba0d0"><span class="id" title="notation">)</span></a>) <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.G"><span class="id" title="variable">G</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Frobenius_cent1_ker"><span class="id" title="lemma">Frobenius_cent1_ker</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ca7f9c8131cd704a6703ad86f415c132"><span class="id" title="notation">^#</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.K"><span class="id" title="variable">K</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Frobenius_reg_ker"><span class="id" title="lemma">Frobenius_reg_ker</span></a> : <a class="idref" href="mathcomp.solvable.frobenius.html#semiregular"><span class="id" title="definition">semiregular</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.H"><span class="id" title="variable">H</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Frobenius_reg_compl"><span class="id" title="lemma">Frobenius_reg_compl</span></a> : <a class="idref" href="mathcomp.solvable.frobenius.html#semiregular"><span class="id" title="definition">semiregular</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.K"><span class="id" title="variable">K</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Frobenius_dvd_ker1"><span class="id" title="lemma">Frobenius_dvd_ker1</span></a> : <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#bde82eab2fe4a0799bc2419e587505d4"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f953bf7095e0da1cb644443fd0e17d6d"><span class="id" title="notation">.-1</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="ltn_odd_Frobenius_ker"><span class="id" title="lemma">ltn_odd_Frobenius_ker</span></a> : <a class="idref" href="mathcomp.ssreflect.ssrnat.html#odd"><span class="id" title="definition">odd</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#bff172cdafaf4b86cefb300b16285e42"><span class="id" title="notation">.*2</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#00fe0eaf5e6949f0a31725357afa4bba"><span class="id" title="notation"><</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Frobenius_index_dvd_ker1"><span class="id" title="lemma">Frobenius_index_dvd_ker1</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#bde82eab2fe4a0799bc2419e587505d4"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f953bf7095e0da1cb644443fd0e17d6d"><span class="id" title="notation">.-1</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Frobenius_coprime"><span class="id" title="lemma">Frobenius_coprime</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#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Frobenius_trivg_cent"><span class="id" title="lemma">Frobenius_trivg_cent</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">C_K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 1.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Frobenius_index_coprime"><span class="id" title="lemma">Frobenius_index_coprime</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#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">|</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Frobenius_ker_Hall"><span class="id" title="lemma">Frobenius_ker_Hall</span></a> : <a class="idref" href="mathcomp.solvable.pgroup.html#Hall"><span class="id" title="definition">Hall</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.K"><span class="id" title="variable">K</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Frobenius_compl_Hall"><span class="id" title="lemma">Frobenius_compl_Hall</span></a> : <a class="idref" href="mathcomp.solvable.pgroup.html#Hall"><span class="id" title="definition">Hall</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.H"><span class="id" title="variable">H</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties"><span class="id" title="section">FrobeniusProperties</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="normedTI_J"><span class="id" title="lemma">normedTI_J</span></a> <span class="id" title="var">x</span> <span class="id" title="var">A</span> <span class="id" title="var">G</span> <span class="id" title="var">L</span> : <a class="idref" href="mathcomp.solvable.frobenius.html#normedTI"><span class="id" title="definition">normedTI</span></a> (<a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#x"><span class="id" title="variable">x</span></a>) (<a class="idref" href="mathcomp.solvable.frobenius.html#L"><span class="id" title="variable">L</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#normedTI"><span class="id" title="definition">normedTI</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#L"><span class="id" title="variable">L</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="FrobeniusJcompl"><span class="id" title="lemma">FrobeniusJcompl</span></a> <span class="id" title="var">x</span> <span class="id" title="var">G</span> <span class="id" title="var">H</span> :<br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#73516a680e9150542d49d1098b491775"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#73516a680e9150542d49d1098b491775"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#73516a680e9150542d49d1098b491775"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#73516a680e9150542d49d1098b491775"><span class="id" title="notation">complement</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#73516a680e9150542d49d1098b491775"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#73516a680e9150542d49d1098b491775"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#73516a680e9150542d49d1098b491775"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#73516a680e9150542d49d1098b491775"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#73516a680e9150542d49d1098b491775"><span class="id" title="notation">complement</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#73516a680e9150542d49d1098b491775"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="FrobeniusJ"><span class="id" title="lemma">FrobeniusJ</span></a> <span class="id" title="var">x</span> <span class="id" title="var">G</span> <span class="id" title="var">K</span> <span class="id" title="var">H</span> :<br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">><|</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">><|</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="FrobeniusJker"><span class="id" title="lemma">FrobeniusJker</span></a> <span class="id" title="var">x</span> <span class="id" title="var">G</span> <span class="id" title="var">K</span> :<br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">kernel</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">kernel</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="FrobeniusJgroup"><span class="id" title="lemma">FrobeniusJgroup</span></a> <span class="id" title="var">x</span> <span class="id" title="var">G</span> : <a class="idref" href="mathcomp.solvable.frobenius.html#09bb2faa2af76eddba9b801e0b61cec9"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#09bb2faa2af76eddba9b801e0b61cec9"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#049e6d4210dc2b8af76facf30c9d4dd6"><span class="id" title="notation">:^</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#09bb2faa2af76eddba9b801e0b61cec9"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#09bb2faa2af76eddba9b801e0b61cec9"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#09bb2faa2af76eddba9b801e0b61cec9"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#09bb2faa2af76eddba9b801e0b61cec9"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Frobenius_ker_dvd_ker1"><span class="id" title="lemma">Frobenius_ker_dvd_ker1</span></a> <span class="id" title="var">G</span> <span class="id" title="var">K</span> :<br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">kernel</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#bde82eab2fe4a0799bc2419e587505d4"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f953bf7095e0da1cb644443fd0e17d6d"><span class="id" title="notation">.-1</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Frobenius_ker_coprime"><span class="id" title="lemma">Frobenius_ker_coprime</span></a> <span class="id" title="var">G</span> <span class="id" title="var">K</span> :<br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">kernel</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#0665f11b64f1431f9d664aba3c000866"><span class="id" title="notation">|</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Frobenius_semiregularP"><span class="id" title="lemma">Frobenius_semiregularP</span></a> <span class="id" title="var">G</span> <span class="id" title="var">K</span> <span class="id" title="var">H</span> :<br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#4c7b411f14f1faa861c7c0ade82faf76"><span class="id" title="notation">><|</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#be2f022a539ec6d4d51932b5ea998e57"><span class="id" title="notation">:!=:</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#be2f022a539ec6d4d51932b5ea998e57"><span class="id" title="notation">:!=:</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="mathcomp.solvable.frobenius.html#semiregular"><span class="id" title="definition">semiregular</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a>) <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">><|</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="prime_FrobeniusP"><span class="id" title="lemma">prime_FrobeniusP</span></a> <span class="id" title="var">G</span> <span class="id" title="var">K</span> <span class="id" title="var">H</span> :<br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#be2f022a539ec6d4d51932b5ea998e57"><span class="id" title="notation">:!=:</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.prime.html#prime"><span class="id" title="definition">prime</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#4c7b411f14f1faa861c7c0ade82faf76"><span class="id" title="notation">><|</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#ba2b0e492d2b4675a0acf3ea92aabadd"><span class="id" title="notation">∧</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">C_K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#04a5555c0db8685a27679a7e6af3f8c3"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 1) <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">><|</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Frobenius_subl"><span class="id" title="lemma">Frobenius_subl</span></a> <span class="id" title="var">G</span> <span class="id" title="var">K</span> <span class="id" title="var">K1</span> <span class="id" title="var">H</span> :<br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#K1"><span class="id" title="variable">K1</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#be2f022a539ec6d4d51932b5ea998e57"><span class="id" title="notation">:!=:</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K1"><span class="id" title="variable">K1</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#K1"><span class="id" title="variable">K1</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#1ff9e060a8cc6098d64e42214fa57c96"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">><|</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K1"><span class="id" title="variable">K1</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#0d7ccd69af81527d9facc6293603bbef"><span class="id" title="notation"><*></span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K1"><span class="id" title="variable">K1</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">><|</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Frobenius_subr"><span class="id" title="lemma">Frobenius_subr</span></a> <span class="id" title="var">G</span> <span class="id" title="var">K</span> <span class="id" title="var">H</span> <span class="id" title="var">H1</span> :<br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#H1"><span class="id" title="variable">H1</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#be2f022a539ec6d4d51932b5ea998e57"><span class="id" title="notation">:!=:</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H1"><span class="id" title="variable">H1</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">><|</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#0d7ccd69af81527d9facc6293603bbef"><span class="id" title="notation"><*></span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H1"><span class="id" title="variable">H1</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">><|</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H1"><span class="id" title="variable">H1</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Frobenius_kerP"><span class="id" title="lemma">Frobenius_kerP</span></a> <span class="id" title="var">G</span> <span class="id" title="var">K</span> :<br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#554fc3f3cf0a27fe0863b7741d119014"><span class="id" title="notation">[/\</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#be2f022a539ec6d4d51932b5ea998e57"><span class="id" title="notation">:!=:</span></a> 1<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#554fc3f3cf0a27fe0863b7741d119014"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f8a5284fd4c86e7670efa54241b49929"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f8a5284fd4c86e7670efa54241b49929"><span class="id" title="notation">proper</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#554fc3f3cf0a27fe0863b7741d119014"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7e8095b432e7aa5c3c22bb87584658b7"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#554fc3f3cf0a27fe0863b7741d119014"><span class="id" title="notation">&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ca7f9c8131cd704a6703ad86f415c132"><span class="id" title="notation">^#</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#554fc3f3cf0a27fe0863b7741d119014"><span class="id" title="notation">]</span></a><br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">kernel</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="set_Frobenius_compl"><span class="id" title="lemma">set_Frobenius_compl</span></a> <span class="id" title="var">G</span> <span class="id" title="var">K</span> <span class="id" title="var">H</span> :<br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#4c7b411f14f1faa861c7c0ade82faf76"><span class="id" title="notation">><|</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">kernel</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">><|</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Frobenius_kerS"><span class="id" title="lemma">Frobenius_kerS</span></a> <span class="id" title="var">G</span> <span class="id" title="var">K</span> <span class="id" title="var">G1</span> :<br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#G1"><span class="id" title="variable">G1</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f8a5284fd4c86e7670efa54241b49929"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f8a5284fd4c86e7670efa54241b49929"><span class="id" title="notation">proper</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G1"><span class="id" title="variable">G1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">kernel</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G1"><span class="id" title="variable">G1</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">kernel</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Frobenius_action_kernel_def"><span class="id" title="lemma">Frobenius_action_kernel_def</span></a> <span class="id" title="var">G</span> <span class="id" title="var">H</span> <span class="id" title="var">K</span> <span class="id" title="var">sT</span> <span class="id" title="var">S</span> <span class="id" title="var">to</span> :<br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#4c7b411f14f1faa861c7c0ade82faf76"><span class="id" title="notation">><|</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> @<a class="idref" href="mathcomp.solvable.frobenius.html#Frobenius_action"><span class="id" title="definition">Frobenius_action</span></a> <span class="id" title="var">_</span> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#sT"><span class="id" title="variable">sT</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#to"><span class="id" title="variable">to</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#f0bbce9238fab3dd03626439080979a9"><span class="id" title="notation">:=:</span></a> 1 <a class="idref" href="mathcomp.ssreflect.finset.html#3bfdad100117c55128c8f4e205b0209b"><span class="id" title="notation">:|:</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#91816551bcea1b6f359ecf76f3595e38"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#91816551bcea1b6f359ecf76f3595e38"><span class="id" title="notation">set</span></a> <span class="id" title="var">x</span> <a class="idref" href="mathcomp.ssreflect.finset.html#91816551bcea1b6f359ecf76f3595e38"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#91816551bcea1b6f359ecf76f3595e38"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.action.html#2bb94d3d01f9b00932888c009233b945"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#2bb94d3d01f9b00932888c009233b945"><span class="id" title="notation">Fix_</span></a><a class="idref" href="mathcomp.fingroup.action.html#2bb94d3d01f9b00932888c009233b945"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.action.html#2bb94d3d01f9b00932888c009233b945"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#2bb94d3d01f9b00932888c009233b945"><span class="id" title="notation">)[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.action.html#2bb94d3d01f9b00932888c009233b945"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#set0"><span class="id" title="definition">set0</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#91816551bcea1b6f359ecf76f3595e38"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics"><span class="id" title="section">FrobeniusBasics</span></a>.<br/> - -<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="Frobenius_coprime_quotient"><span class="id" title="lemma">Frobenius_coprime_quotient</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">G</span> <span class="id" title="var">K</span> <span class="id" title="var">H</span> <span class="id" title="var">N</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) :<br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#4c7b411f14f1faa861c7c0ade82faf76"><span class="id" title="notation">><|</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#N"><span class="id" title="variable">N</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7e8095b432e7aa5c3c22bb87584658b7"><span class="id" title="notation"><|</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#ba2b0e492d2b4675a0acf3ea92aabadd"><span class="id" title="notation">∧</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#be2f022a539ec6d4d51932b5ea998e57"><span class="id" title="notation">:!=:</span></a> 1%<span class="id" title="var">g</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#N"><span class="id" title="variable">N</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f8a5284fd4c86e7670efa54241b49929"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f8a5284fd4c86e7670efa54241b49929"><span class="id" title="notation">proper</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#ba2b0e492d2b4675a0acf3ea92aabadd"><span class="id" title="notation">∧</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ca7f9c8131cd704a6703ad86f415c132"><span class="id" title="notation">^#</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">C_K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#bb1f7e576b21e943bdeacc0f6a28b245"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#N"><span class="id" title="variable">N</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#8c08d4203604dbed63e7afa9b689d858"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#3e65ad3edf5f7fb3ea6bc63a878112a8"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#N"><span class="id" title="variable">N</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#3e65ad3edf5f7fb3ea6bc63a878112a8"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#N"><span class="id" title="variable">N</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">><|</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.fingroup.quotient.html#3e65ad3edf5f7fb3ea6bc63a878112a8"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#N"><span class="id" title="variable">N</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">)]</span></a>%<span class="id" title="var">g</span>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="InjmFrobenius"><span class="id" title="section">InjmFrobenius</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="InjmFrobenius.gT"><span class="id" title="variable">gT</span></a> <a name="InjmFrobenius.rT"><span class="id" title="variable">rT</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#FinGroup.Exports.finGroupType"><span class="id" title="abbreviation">finGroupType</span></a>) (<a name="InjmFrobenius.D"><span class="id" title="variable">D</span></a> <a name="InjmFrobenius.G"><span class="id" title="variable">G</span></a> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) (<a name="InjmFrobenius.f"><span class="id" title="variable">f</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">>-></span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#rT"><span class="id" title="variable">rT</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#efe2275bee4a5227161b40da886719a5"><span class="id" title="notation">}</span></a>).<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">H</span> <span class="id" title="var">K</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#InjmFrobenius.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">sGD</span> : <a class="idref" href="mathcomp.solvable.frobenius.html#InjmFrobenius.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#4102da6205bd8605932488256a8bd517"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#InjmFrobenius.D"><span class="id" title="variable">D</span></a>) (<span class="id" title="var">injf</span> : <a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#3a01b501aff42699ca141d6279e9102f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#InjmFrobenius.f"><span class="id" title="variable">f</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="injm_Frobenius_compl"><span class="id" title="lemma">injm_Frobenius_compl</span></a> <span class="id" title="var">H</span> <span class="id" title="var">sGD</span> <span class="id" title="var">injf</span> : <br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#73516a680e9150542d49d1098b491775"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#73516a680e9150542d49d1098b491775"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#InjmFrobenius.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#73516a680e9150542d49d1098b491775"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#73516a680e9150542d49d1098b491775"><span class="id" title="notation">complement</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#73516a680e9150542d49d1098b491775"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#73516a680e9150542d49d1098b491775"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#73516a680e9150542d49d1098b491775"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#InjmFrobenius.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#InjmFrobenius.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#73516a680e9150542d49d1098b491775"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#73516a680e9150542d49d1098b491775"><span class="id" title="notation">complement</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#InjmFrobenius.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#73516a680e9150542d49d1098b491775"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="injm_Frobenius"><span class="id" title="lemma">injm_Frobenius</span></a> <span class="id" title="var">H</span> <span class="id" title="var">K</span> <span class="id" title="var">sGD</span> <span class="id" title="var">injf</span> : <br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#InjmFrobenius.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">><|</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#InjmFrobenius.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#InjmFrobenius.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#InjmFrobenius.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">><|</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#InjmFrobenius.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#6a02d4f0bf764b40a5c4d5e7c25f76d3"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="injm_Frobenius_ker"><span class="id" title="lemma">injm_Frobenius_ker</span></a> <span class="id" title="var">K</span> <span class="id" title="var">sGD</span> <span class="id" title="var">injf</span> : <br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#InjmFrobenius.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">kernel</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#InjmFrobenius.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#InjmFrobenius.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">kernel</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#InjmFrobenius.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#74eaff00fb742dcd0d78d509b2b0e3f8"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="injm_Frobenius_group"><span class="id" title="lemma">injm_Frobenius_group</span></a> <span class="id" title="var">sGD</span> <span class="id" title="var">injf</span> : <a class="idref" href="mathcomp.solvable.frobenius.html#09bb2faa2af76eddba9b801e0b61cec9"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#09bb2faa2af76eddba9b801e0b61cec9"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#InjmFrobenius.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#09bb2faa2af76eddba9b801e0b61cec9"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#09bb2faa2af76eddba9b801e0b61cec9"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#09bb2faa2af76eddba9b801e0b61cec9"><span class="id" title="notation">Frobenius</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#InjmFrobenius.f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#70b0a61e30f130888503421fd44e1802"><span class="id" title="notation">@*</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#InjmFrobenius.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#09bb2faa2af76eddba9b801e0b61cec9"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.solvable.frobenius.html#InjmFrobenius"><span class="id" title="section">InjmFrobenius</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Theorem</span> <a name="Frobenius_Ldiv"><span class="id" title="lemma">Frobenius_Ldiv</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">G</span> : <a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#dd8cd2228f051940101d045bfdffe2d9"><span class="id" title="notation">}</span></a>) <span class="id" title="var">n</span> :<br/> - <a class="idref" href="mathcomp.solvable.frobenius.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#bde82eab2fe4a0799bc2419e587505d4"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#bde82eab2fe4a0799bc2419e587505d4"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.abelian.html#9bedce05b970c48e2984b10e94f8e153"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.abelian.html#9bedce05b970c48e2984b10e94f8e153"><span class="id" title="notation">Ldiv_n</span></a><a class="idref" href="mathcomp.solvable.abelian.html#9bedce05b970c48e2984b10e94f8e153"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.solvable.abelian.html#9bedce05b970c48e2984b10e94f8e153"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#234f50e13366f794cd6877cf832a5935"><span class="id" title="notation">|</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 |