diff options
Diffstat (limited to 'docs/htmldoc/mathcomp.solvable.frobenius.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.solvable.frobenius.html | 438 |
1 files changed, 438 insertions, 0 deletions
diff --git a/docs/htmldoc/mathcomp.solvable.frobenius.html b/docs/htmldoc/mathcomp.solvable.frobenius.html new file mode 100644 index 0000000..d1eb384 --- /dev/null +++ b/docs/htmldoc/mathcomp.solvable.frobenius.html @@ -0,0 +1,438 @@ +<!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/> +<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#"><span class="id" title="library">mathcomp.ssreflect.ssreflect</span></a>.<br/> + +<br/> +</div> + +<div class="doc"> + 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#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#Definitions.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a>.<br/> + +<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/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#adb8044960c962a921cca1bd48aae97d"><span class="id" title="notation">^#</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">C_K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><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#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 1<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +</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/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#adb8044960c962a921cca1bd48aae97d"><span class="id" title="notation">^#</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">C_K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><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#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">C_K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><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#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</span></a>.<br/> + +<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/8.8.0/stdlib//Coq.ssr.ssrbool.html#2e9317c5f71a1305fb695cdc49716482"><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#b1eeadc2feabc7422252baa895418c7b"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#2e9317c5f71a1305fb695cdc49716482"><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#6c121d1bcff5b1c0972474f398d18325"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#2e9317c5f71a1305fb695cdc49716482"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7193b23d12b4f3c2146b0e77ee974b2b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#7193b23d12b4f3c2146b0e77ee974b2b"><span class="id" title="notation">N_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#7193b23d12b4f3c2146b0e77ee974b2b"><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#7193b23d12b4f3c2146b0e77ee974b2b"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#2e9317c5f71a1305fb695cdc49716482"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="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/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><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#b1eeadc2feabc7422252baa895418c7b"><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/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">&&</span></a> <a class="idref" href="mathcomp.solvable.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#adb8044960c962a921cca1bd48aae97d"><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#a843dcbb9dc2e69b147054d3e1465e78"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#a843dcbb9dc2e69b147054d3e1465e78"><span class="id" title="notation">∃</span></a> <span class="id" title="var">H</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#a843dcbb9dc2e69b147054d3e1465e78"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#Definitions.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#46e5a4123d46e6b126f7788a77176785"><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#a843dcbb9dc2e69b147054d3e1465e78"><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/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><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#ff5a974c523b8d4c8927273818a26a02"><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#17d28d004d0863cb022d4ce832ddaaae"><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/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">&&</span></a> <a class="idref" href="mathcomp.solvable.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#a843dcbb9dc2e69b147054d3e1465e78"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#a843dcbb9dc2e69b147054d3e1465e78"><span class="id" title="notation">∃</span></a> <span class="id" title="var">H</span> <a class="idref" href="mathcomp.ssreflect.fintype.html#a843dcbb9dc2e69b147054d3e1465e78"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#Definitions.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#46e5a4123d46e6b126f7788a77176785"><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#a843dcbb9dc2e69b147054d3e1465e78"><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#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#Definitions.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a>.<br/> +<span class="id" title="keyword">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#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a>) (<a name="Definitions.FrobeniusAction.to"><span class="id" title="variable">to</span></a> : <a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">action</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#Definitions.gT"><span class="id" title="variable">gT</span></a> <a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">&-></span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#sT"><span class="id" title="variable">sT</span></a><a class="idref" href="mathcomp.fingroup.action.html#5c606fa2629c1fac8f3ee3f6e9ad2934"><span class="id" title="notation">}</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="Frobenius_action"><span class="id" title="definition">Frobenius_action</span></a> :=<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#c7fe7fb0f694e91a7e258ff78a0390ef"><span class="id" title="notation">[/\</span></a> <a class="idref" href="mathcomp.fingroup.action.html#6e1bf5287bfc6397badc2a71c227e8d0"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#6e1bf5287bfc6397badc2a71c227e8d0"><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#6e1bf5287bfc6397badc2a71c227e8d0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#6e1bf5287bfc6397badc2a71c227e8d0"><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#6e1bf5287bfc6397badc2a71c227e8d0"><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#6e1bf5287bfc6397badc2a71c227e8d0"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#c7fe7fb0f694e91a7e258ff78a0390ef"><span class="id" title="notation">,</span></a><br/> + <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">transitive</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#Definitions.FrobeniusAction.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">on</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#Definitions.FrobeniusAction.S"><span class="id" title="variable">S</span></a> <a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#Definitions.FrobeniusAction.to"><span class="id" title="variable">to</span></a><a class="idref" href="mathcomp.fingroup.action.html#ad5f1da050fedbae022d48bb21530fba"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#c7fe7fb0f694e91a7e258ff78a0390ef"><span class="id" title="notation">,</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#Definitions.FrobeniusAction.G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#adb8044960c962a921cca1bd48aae97d"><span class="id" title="notation">^#</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.fingroup.action.html#d332864708f1d0e9a3a13805c0663964"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#d332864708f1d0e9a3a13805c0663964"><span class="id" title="notation">Fix_</span></a><a class="idref" href="mathcomp.fingroup.action.html#d332864708f1d0e9a3a13805c0663964"><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#d332864708f1d0e9a3a13805c0663964"><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#d332864708f1d0e9a3a13805c0663964"><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#d332864708f1d0e9a3a13805c0663964"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#9b077c369e19739ef880736ba34623ff"><span class="id" title="notation">≤</span></a> 1<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#c7fe7fb0f694e91a7e258ff78a0390ef"><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#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 1<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#c7fe7fb0f694e91a7e258ff78a0390ef"><span class="id" title="notation">&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">u</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#Definitions.FrobeniusAction.S"><span class="id" title="variable">S</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.action.html#d6d8c6555a0082b6cbf651a274d2a4d6"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#d6d8c6555a0082b6cbf651a274d2a4d6"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.action.html#d6d8c6555a0082b6cbf651a274d2a4d6"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.fingroup.action.html#d6d8c6555a0082b6cbf651a274d2a4d6"><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#d6d8c6555a0082b6cbf651a274d2a4d6"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#c7fe7fb0f694e91a7e258ff78a0390ef"><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">CoInductive</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="9829227212a3e6faf0fd92ec80565912"><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="d4e6bc74ab587888a04843e00b93ce8e"><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="e8e2fd4a723a04f0e53299cb08000cfe"><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="4d6d07a024def374c6574865fc5ac3d7"><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#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">set</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#0fec877de6d09ef39abb9b599a84eb0e"><span class="id" title="notation">}</span></a>) (<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#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>).<br/> + +<br/> +<span class="id" title="keyword">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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K2"><span class="id" title="variable">K2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A1"><span class="id" title="variable">A1</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A2"><span class="id" title="variable">A2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">C_K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><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#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.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#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K2"><span class="id" title="variable">K2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A1"><span class="id" title="variable">A1</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A2"><span class="id" title="variable">A2</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#36625695d37b6869c156bfcdf13834f7"><span class="id" title="notation">:!=:</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">C_K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><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#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">C_K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><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#507fd39a15bb9cb7e52e1aaa9e2285b5"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">C_H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><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#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">C_H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><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#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#36625695d37b6869c156bfcdf13834f7"><span class="id" title="notation">:!=:</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">C_K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><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#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 1.<br/> + +<br/> +<span class="id" title="keyword">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#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#aa34fd1c61c5cf0a3356b624a5d2afed"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><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#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a>.<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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#1deb3845cf16de446ae6619879e9d6db"><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#1deb3845cf16de446ae6619879e9d6db"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#1deb3845cf16de446ae6619879e9d6db"><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#1deb3845cf16de446ae6619879e9d6db"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><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#b1eeadc2feabc7422252baa895418c7b"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><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#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#7193b23d12b4f3c2146b0e77ee974b2b"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#7193b23d12b4f3c2146b0e77ee974b2b"><span class="id" title="notation">N_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#7193b23d12b4f3c2146b0e77ee974b2b"><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#7193b23d12b4f3c2146b0e77ee974b2b"><span class="id" title="notation">)</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">g</span>, <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">~~</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#fca367ac88276c4c83db3cc7c637993a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#fca367ac88276c4c83db3cc7c637993a"><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#fca367ac88276c4c83db3cc7c637993a"><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#1deb3845cf16de446ae6619879e9d6db"><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#fca367ac88276c4c83db3cc7c637993a"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#g"><span class="id" title="variable">g</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#L"><span class="id" title="variable">L</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><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#b1eeadc2feabc7422252baa895418c7b"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><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#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#208bc995000a6307bdbc043c43919d97"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#208bc995000a6307bdbc043c43919d97"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#208bc995000a6307bdbc043c43919d97"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#208bc995000a6307bdbc043c43919d97"><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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><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#808c6b8e35e792f23899f360a21e4638"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#L"><span class="id" title="variable">L</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#208bc995000a6307bdbc043c43919d97"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><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#b1eeadc2feabc7422252baa895418c7b"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#6c121d1bcff5b1c0972474f398d18325"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#6c121d1bcff5b1c0972474f398d18325"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#6c121d1bcff5b1c0972474f398d18325"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.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#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> (<a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><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#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#697e4695610f677ae98a52af81f779d2"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#L"><span class="id" title="variable">L</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><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#b1eeadc2feabc7422252baa895418c7b"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#B"><span class="id" title="variable">B</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#A"><span class="id" title="variable">A</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><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#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><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#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#L"><span class="id" title="variable">L</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">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/8.8.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#9829227212a3e6faf0fd92ec80565912"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#9829227212a3e6faf0fd92ec80565912"><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#9829227212a3e6faf0fd92ec80565912"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#9829227212a3e6faf0fd92ec80565912"><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#9829227212a3e6faf0fd92ec80565912"><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#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>.<br/> +<span class="id" title="keyword">Hypothesis</span> <a name="FrobeniusBasics.FrobeniusProperties.frobG"><span class="id" title="variable">frobG</span></a> : <a class="idref" href="mathcomp.solvable.frobenius.html#4d6d07a024def374c6574865fc5ac3d7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#4d6d07a024def374c6574865fc5ac3d7"><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#4d6d07a024def374c6574865fc5ac3d7"><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#4d6d07a024def374c6574865fc5ac3d7"><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#4d6d07a024def374c6574865fc5ac3d7"><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#d4e6bc74ab587888a04843e00b93ce8e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#d4e6bc74ab587888a04843e00b93ce8e"><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#d4e6bc74ab587888a04843e00b93ce8e"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#d4e6bc74ab587888a04843e00b93ce8e"><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#d4e6bc74ab587888a04843e00b93ce8e"><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#9829227212a3e6faf0fd92ec80565912"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#9829227212a3e6faf0fd92ec80565912"><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#9829227212a3e6faf0fd92ec80565912"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#9829227212a3e6faf0fd92ec80565912"><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#9829227212a3e6faf0fd92ec80565912"><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#e8e2fd4a723a04f0e53299cb08000cfe"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#e8e2fd4a723a04f0e53299cb08000cfe"><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#e8e2fd4a723a04f0e53299cb08000cfe"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#c7fe7fb0f694e91a7e258ff78a0390ef"><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#ff5a974c523b8d4c8927273818a26a02"><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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#c7fe7fb0f694e91a7e258ff78a0390ef"><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#36625695d37b6869c156bfcdf13834f7"><span class="id" title="notation">:!=:</span></a> 1<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#c7fe7fb0f694e91a7e258ff78a0390ef"><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#36625695d37b6869c156bfcdf13834f7"><span class="id" title="notation">:!=:</span></a> 1<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#c7fe7fb0f694e91a7e258ff78a0390ef"><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#219b95257a323aaee1742e9bec4975d7"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#219b95257a323aaee1742e9bec4975d7"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#c7fe7fb0f694e91a7e258ff78a0390ef"><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#219b95257a323aaee1742e9bec4975d7"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#219b95257a323aaee1742e9bec4975d7"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#c7fe7fb0f694e91a7e258ff78a0390ef"><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#8d51214861729e594d3598f0d320a13d"><span class="id" title="notation">|:</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#8d51214861729e594d3598f0d320a13d"><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#adb8044960c962a921cca1bd48aae97d"><span class="id" title="notation">^#</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#6c121d1bcff5b1c0972474f398d18325"><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#8d51214861729e594d3598f0d320a13d"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#adb8044960c962a921cca1bd48aae97d"><span class="id" title="notation">^#</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><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#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.K"><span class="id" title="variable">K</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">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#f01714bb99e6c7abc6cfb2e43eff7f6e"><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#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#aa34fd1c61c5cf0a3356b624a5d2afed"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><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#f01714bb99e6c7abc6cfb2e43eff7f6e"><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#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><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#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f460b977ac49dd1a229be682bc38c411"><span class="id" title="notation">.*2</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation"><</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><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#f65ecb5148d1ef5a9c551827b20e9bfa"><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#f65ecb5148d1ef5a9c551827b20e9bfa"><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#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#aa34fd1c61c5cf0a3356b624a5d2afed"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><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#f01714bb99e6c7abc6cfb2e43eff7f6e"><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#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a>.<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#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">C_K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><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#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 1.<br/> + +<br/> +<span class="id" title="keyword">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#f01714bb99e6c7abc6cfb2e43eff7f6e"><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#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#FrobeniusBasics.FrobeniusProperties.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">|</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="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#1deb3845cf16de446ae6619879e9d6db"><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#1deb3845cf16de446ae6619879e9d6db"><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#1deb3845cf16de446ae6619879e9d6db"><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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><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#9829227212a3e6faf0fd92ec80565912"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#9829227212a3e6faf0fd92ec80565912"><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#1deb3845cf16de446ae6619879e9d6db"><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#9829227212a3e6faf0fd92ec80565912"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#9829227212a3e6faf0fd92ec80565912"><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#1deb3845cf16de446ae6619879e9d6db"><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#9829227212a3e6faf0fd92ec80565912"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#9829227212a3e6faf0fd92ec80565912"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#9829227212a3e6faf0fd92ec80565912"><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#9829227212a3e6faf0fd92ec80565912"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#9829227212a3e6faf0fd92ec80565912"><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#9829227212a3e6faf0fd92ec80565912"><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#4d6d07a024def374c6574865fc5ac3d7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#4d6d07a024def374c6574865fc5ac3d7"><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#1deb3845cf16de446ae6619879e9d6db"><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#4d6d07a024def374c6574865fc5ac3d7"><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#1deb3845cf16de446ae6619879e9d6db"><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#4d6d07a024def374c6574865fc5ac3d7"><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#1deb3845cf16de446ae6619879e9d6db"><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#4d6d07a024def374c6574865fc5ac3d7"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#4d6d07a024def374c6574865fc5ac3d7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#4d6d07a024def374c6574865fc5ac3d7"><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#4d6d07a024def374c6574865fc5ac3d7"><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#4d6d07a024def374c6574865fc5ac3d7"><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#4d6d07a024def374c6574865fc5ac3d7"><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#d4e6bc74ab587888a04843e00b93ce8e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#d4e6bc74ab587888a04843e00b93ce8e"><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#1deb3845cf16de446ae6619879e9d6db"><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#d4e6bc74ab587888a04843e00b93ce8e"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#d4e6bc74ab587888a04843e00b93ce8e"><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#1deb3845cf16de446ae6619879e9d6db"><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#d4e6bc74ab587888a04843e00b93ce8e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#d4e6bc74ab587888a04843e00b93ce8e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#d4e6bc74ab587888a04843e00b93ce8e"><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#d4e6bc74ab587888a04843e00b93ce8e"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#d4e6bc74ab587888a04843e00b93ce8e"><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#d4e6bc74ab587888a04843e00b93ce8e"><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#e8e2fd4a723a04f0e53299cb08000cfe"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#e8e2fd4a723a04f0e53299cb08000cfe"><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#1deb3845cf16de446ae6619879e9d6db"><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#e8e2fd4a723a04f0e53299cb08000cfe"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#e8e2fd4a723a04f0e53299cb08000cfe"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#e8e2fd4a723a04f0e53299cb08000cfe"><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#e8e2fd4a723a04f0e53299cb08000cfe"><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#d4e6bc74ab587888a04843e00b93ce8e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#d4e6bc74ab587888a04843e00b93ce8e"><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#d4e6bc74ab587888a04843e00b93ce8e"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#d4e6bc74ab587888a04843e00b93ce8e"><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#d4e6bc74ab587888a04843e00b93ce8e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><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#f65ecb5148d1ef5a9c551827b20e9bfa"><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#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#aa34fd1c61c5cf0a3356b624a5d2afed"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><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#d4e6bc74ab587888a04843e00b93ce8e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#d4e6bc74ab587888a04843e00b93ce8e"><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#d4e6bc74ab587888a04843e00b93ce8e"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#d4e6bc74ab587888a04843e00b93ce8e"><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#d4e6bc74ab587888a04843e00b93ce8e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#f65ecb5148d1ef5a9c551827b20e9bfa"><span class="id" title="notation">|</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="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#ff5a974c523b8d4c8927273818a26a02"><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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#36625695d37b6869c156bfcdf13834f7"><span class="id" title="notation">:!=:</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#36625695d37b6869c156bfcdf13834f7"><span class="id" title="notation">:!=:</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#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#4d6d07a024def374c6574865fc5ac3d7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#4d6d07a024def374c6574865fc5ac3d7"><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#4d6d07a024def374c6574865fc5ac3d7"><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#4d6d07a024def374c6574865fc5ac3d7"><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#4d6d07a024def374c6574865fc5ac3d7"><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#36625695d37b6869c156bfcdf13834f7"><span class="id" title="notation">:!=:</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#f01714bb99e6c7abc6cfb2e43eff7f6e"><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#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#ff5a974c523b8d4c8927273818a26a02"><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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><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/8.8.0/stdlib//Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">C_K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#507fd39a15bb9cb7e52e1aaa9e2285b5"><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#507fd39a15bb9cb7e52e1aaa9e2285b5"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 1) <a class="idref" href="mathcomp.solvable.frobenius.html#4d6d07a024def374c6574865fc5ac3d7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#4d6d07a024def374c6574865fc5ac3d7"><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#4d6d07a024def374c6574865fc5ac3d7"><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#4d6d07a024def374c6574865fc5ac3d7"><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#4d6d07a024def374c6574865fc5ac3d7"><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#36625695d37b6869c156bfcdf13834f7"><span class="id" title="notation">:!=:</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">N</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#K1"><span class="id" title="variable">K1</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#3cae19671031307d430e5b14ccbd1058"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#4d6d07a024def374c6574865fc5ac3d7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#4d6d07a024def374c6574865fc5ac3d7"><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#4d6d07a024def374c6574865fc5ac3d7"><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#4d6d07a024def374c6574865fc5ac3d7"><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#4d6d07a024def374c6574865fc5ac3d7"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.solvable.frobenius.html#4d6d07a024def374c6574865fc5ac3d7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#4d6d07a024def374c6574865fc5ac3d7"><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#80208730563aa86aa7861f6fe1b846da"><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#4d6d07a024def374c6574865fc5ac3d7"><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#4d6d07a024def374c6574865fc5ac3d7"><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#4d6d07a024def374c6574865fc5ac3d7"><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#36625695d37b6869c156bfcdf13834f7"><span class="id" title="notation">:!=:</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#4d6d07a024def374c6574865fc5ac3d7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#4d6d07a024def374c6574865fc5ac3d7"><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#4d6d07a024def374c6574865fc5ac3d7"><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#4d6d07a024def374c6574865fc5ac3d7"><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#4d6d07a024def374c6574865fc5ac3d7"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.solvable.frobenius.html#4d6d07a024def374c6574865fc5ac3d7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#4d6d07a024def374c6574865fc5ac3d7"><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#80208730563aa86aa7861f6fe1b846da"><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#4d6d07a024def374c6574865fc5ac3d7"><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#4d6d07a024def374c6574865fc5ac3d7"><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#4d6d07a024def374c6574865fc5ac3d7"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ca13a32469ebe56c9f4cc99d00e8eeba"><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#36625695d37b6869c156bfcdf13834f7"><span class="id" title="notation">:!=:</span></a> 1<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ca13a32469ebe56c9f4cc99d00e8eeba"><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#219b95257a323aaee1742e9bec4975d7"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#219b95257a323aaee1742e9bec4975d7"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#ca13a32469ebe56c9f4cc99d00e8eeba"><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#c27c638e534bbb5b7de2d4b4aa0a3e82"><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/8.8.0/stdlib//Coq.ssr.ssrbool.html#ca13a32469ebe56c9f4cc99d00e8eeba"><span class="id" title="notation">&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#adb8044960c962a921cca1bd48aae97d"><span class="id" title="notation">^#</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">C_G</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><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#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ca13a32469ebe56c9f4cc99d00e8eeba"><span class="id" title="notation">]</span></a><br/> + <a class="idref" href="mathcomp.solvable.frobenius.html#d4e6bc74ab587888a04843e00b93ce8e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#d4e6bc74ab587888a04843e00b93ce8e"><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#d4e6bc74ab587888a04843e00b93ce8e"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#d4e6bc74ab587888a04843e00b93ce8e"><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#d4e6bc74ab587888a04843e00b93ce8e"><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#ff5a974c523b8d4c8927273818a26a02"><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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#d4e6bc74ab587888a04843e00b93ce8e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#d4e6bc74ab587888a04843e00b93ce8e"><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#d4e6bc74ab587888a04843e00b93ce8e"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#d4e6bc74ab587888a04843e00b93ce8e"><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#d4e6bc74ab587888a04843e00b93ce8e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#4d6d07a024def374c6574865fc5ac3d7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#4d6d07a024def374c6574865fc5ac3d7"><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#4d6d07a024def374c6574865fc5ac3d7"><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#4d6d07a024def374c6574865fc5ac3d7"><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#4d6d07a024def374c6574865fc5ac3d7"><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#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#219b95257a323aaee1742e9bec4975d7"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#219b95257a323aaee1742e9bec4975d7"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.solvable.frobenius.html#d4e6bc74ab587888a04843e00b93ce8e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#d4e6bc74ab587888a04843e00b93ce8e"><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#d4e6bc74ab587888a04843e00b93ce8e"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#d4e6bc74ab587888a04843e00b93ce8e"><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#d4e6bc74ab587888a04843e00b93ce8e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#d4e6bc74ab587888a04843e00b93ce8e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#d4e6bc74ab587888a04843e00b93ce8e"><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#d4e6bc74ab587888a04843e00b93ce8e"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#d4e6bc74ab587888a04843e00b93ce8e"><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#d4e6bc74ab587888a04843e00b93ce8e"><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#ff5a974c523b8d4c8927273818a26a02"><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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#67291ec55239f54fa5aa0b0bb974446c"><span class="id" title="notation">:=:</span></a> 1 <a class="idref" href="mathcomp.ssreflect.finset.html#52f608a788da136ac97df132d7055463"><span class="id" title="notation">:|:</span></a> <a class="idref" href="mathcomp.ssreflect.finset.html#11a9aebd9632a5968df4f5811663355a"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.ssreflect.finset.html#11a9aebd9632a5968df4f5811663355a"><span class="id" title="notation">set</span></a> <span class="id" title="var">x</span> <a class="idref" href="mathcomp.ssreflect.finset.html#11a9aebd9632a5968df4f5811663355a"><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#11a9aebd9632a5968df4f5811663355a"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.fingroup.action.html#d332864708f1d0e9a3a13805c0663964"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.action.html#d332864708f1d0e9a3a13805c0663964"><span class="id" title="notation">Fix_</span></a><a class="idref" href="mathcomp.fingroup.action.html#d332864708f1d0e9a3a13805c0663964"><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#d332864708f1d0e9a3a13805c0663964"><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#d332864708f1d0e9a3a13805c0663964"><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#d332864708f1d0e9a3a13805c0663964"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><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#11a9aebd9632a5968df4f5811663355a"><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#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) :<br/> + <a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.fingroup.gproduct.html#ff5a974c523b8d4c8927273818a26a02"><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/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><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#c27c638e534bbb5b7de2d4b4aa0a3e82"><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/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#coprime"><span class="id" title="definition">coprime</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><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#36625695d37b6869c156bfcdf13834f7"><span class="id" title="notation">:!=:</span></a> 1%<span class="id" title="var">g</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.solvable.frobenius.html#N"><span class="id" title="variable">N</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#219b95257a323aaee1742e9bec4975d7"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#219b95257a323aaee1742e9bec4975d7"><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/8.8.0/stdlib//Coq.Init.Logic.html#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#H"><span class="id" title="variable">H</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#adb8044960c962a921cca1bd48aae97d"><span class="id" title="notation">^#</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">C_K</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#addacbae2e0ffbfd03aaa03c308b39d7"><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#addacbae2e0ffbfd03aaa03c308b39d7"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#N"><span class="id" title="variable">N</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#5c59b35a0b51db520cf1fba473ecf127"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.solvable.frobenius.html#4d6d07a024def374c6574865fc5ac3d7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#4d6d07a024def374c6574865fc5ac3d7"><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#c7768147d2d560601601fbf95706ddcc"><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#4d6d07a024def374c6574865fc5ac3d7"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#4d6d07a024def374c6574865fc5ac3d7"><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#c7768147d2d560601601fbf95706ddcc"><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#4d6d07a024def374c6574865fc5ac3d7"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#4d6d07a024def374c6574865fc5ac3d7"><span class="id" title="notation">><|</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#4d6d07a024def374c6574865fc5ac3d7"><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#c7768147d2d560601601fbf95706ddcc"><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#4d6d07a024def374c6574865fc5ac3d7"><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#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<a name="InjmFrobenius.f"><span class="id" title="variable">f</span></a> : <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><span class="id" title="notation">morphism</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.fingroup.morphism.html#c5b2825fcd994c4c5cc69df8802f5376"><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#c5b2825fcd994c4c5cc69df8802f5376"><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#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#InjmFrobenius.gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">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#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#826eae8d7598a787ea56f4249e6e210e"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.solvable.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#14bfb149f00fa839cfb11397f4fe629f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.fingroup.morphism.html#14bfb149f00fa839cfb11397f4fe629f"><span class="id" title="notation">injm</span></a> <a class="idref" href="mathcomp.solvable.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#9829227212a3e6faf0fd92ec80565912"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#9829227212a3e6faf0fd92ec80565912"><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#9829227212a3e6faf0fd92ec80565912"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#9829227212a3e6faf0fd92ec80565912"><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#9829227212a3e6faf0fd92ec80565912"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#9829227212a3e6faf0fd92ec80565912"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#9829227212a3e6faf0fd92ec80565912"><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#48cff845c81518398138031392d44c93"><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#9829227212a3e6faf0fd92ec80565912"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#9829227212a3e6faf0fd92ec80565912"><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#48cff845c81518398138031392d44c93"><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#9829227212a3e6faf0fd92ec80565912"><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#4d6d07a024def374c6574865fc5ac3d7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#4d6d07a024def374c6574865fc5ac3d7"><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#4d6d07a024def374c6574865fc5ac3d7"><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#4d6d07a024def374c6574865fc5ac3d7"><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#4d6d07a024def374c6574865fc5ac3d7"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#4d6d07a024def374c6574865fc5ac3d7"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#4d6d07a024def374c6574865fc5ac3d7"><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#48cff845c81518398138031392d44c93"><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#4d6d07a024def374c6574865fc5ac3d7"><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#48cff845c81518398138031392d44c93"><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#4d6d07a024def374c6574865fc5ac3d7"><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#48cff845c81518398138031392d44c93"><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#4d6d07a024def374c6574865fc5ac3d7"><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#d4e6bc74ab587888a04843e00b93ce8e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#d4e6bc74ab587888a04843e00b93ce8e"><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#d4e6bc74ab587888a04843e00b93ce8e"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#d4e6bc74ab587888a04843e00b93ce8e"><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#d4e6bc74ab587888a04843e00b93ce8e"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#d4e6bc74ab587888a04843e00b93ce8e"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#d4e6bc74ab587888a04843e00b93ce8e"><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#48cff845c81518398138031392d44c93"><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#d4e6bc74ab587888a04843e00b93ce8e"><span class="id" title="notation">with</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#d4e6bc74ab587888a04843e00b93ce8e"><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#48cff845c81518398138031392d44c93"><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#d4e6bc74ab587888a04843e00b93ce8e"><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#e8e2fd4a723a04f0e53299cb08000cfe"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#e8e2fd4a723a04f0e53299cb08000cfe"><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#e8e2fd4a723a04f0e53299cb08000cfe"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#e8e2fd4a723a04f0e53299cb08000cfe"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#e8e2fd4a723a04f0e53299cb08000cfe"><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#48cff845c81518398138031392d44c93"><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#e8e2fd4a723a04f0e53299cb08000cfe"><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#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">group</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#gT"><span class="id" title="variable">gT</span></a><a class="idref" href="mathcomp.fingroup.fingroup.html#ab072eb546972c7e5cdaf33b8a35ce6b"><span class="id" title="notation">}</span></a>) <span class="id" title="var">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#aa34fd1c61c5cf0a3356b624a5d2afed"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.frobenius.html#G"><span class="id" title="variable">G</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">|</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.solvable.frobenius.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.ssreflect.div.html#aa34fd1c61c5cf0a3356b624a5d2afed"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><span class="id" title="notation">#|</span></a><a class="idref" href="mathcomp.solvable.abelian.html#b06f56cd886fcbad526a037600cca851"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.solvable.abelian.html#b06f56cd886fcbad526a037600cca851"><span class="id" title="notation">Ldiv_n</span></a><a class="idref" href="mathcomp.solvable.abelian.html#b06f56cd886fcbad526a037600cca851"><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#b06f56cd886fcbad526a037600cca851"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.ssreflect.fintype.html#f01714bb99e6c7abc6cfb2e43eff7f6e"><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 |