diff options
| author | Enrico Tassi | 2018-04-20 10:54:22 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-04-20 10:54:22 +0200 |
| commit | ed05182cece6bb3706e09b2ce14af4a41a2e8141 (patch) | |
| tree | e850d7314b6372d0476cf2ffaf7d3830721db7b1 /docs/htmldoc/mathcomp.field.separable.html | |
| parent | 3d196f44681fb3b23ff8a79fbd44e12308680531 (diff) | |
generate the documentation for 1.7
Diffstat (limited to 'docs/htmldoc/mathcomp.field.separable.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.field.separable.html | 503 |
1 files changed, 503 insertions, 0 deletions
diff --git a/docs/htmldoc/mathcomp.field.separable.html b/docs/htmldoc/mathcomp.field.separable.html new file mode 100644 index 0000000..e436592 --- /dev/null +++ b/docs/htmldoc/mathcomp.field.separable.html @@ -0,0 +1,503 @@ +<!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.field.separable</title> +</head> + +<body> + +<div id="page"> + +<div id="header"> +</div> + +<div id="main"> + +<h1 class="libtitle">Library mathcomp.field.separable</h1> + +<div class="code"> +<span class="comment">(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. <br/> + Distributed under the terms of CeCILL-B. *)</span><br/> +<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="mathcomp.ssreflect.ssreflect.html#"><span class="id" title="library">mathcomp.ssreflect.ssreflect</span></a>.<br/> + +<br/> +</div> + +<div class="doc"> + This file provides a theory of separable and inseparable field extensions. + +<div class="paragraph"> </div> + + separable_poly p <=> p has no multiple roots in any field extension. + separable_element K x <=> the minimal polynomial of x over K is separable. + separable K E <=> every member of E is separable over K. + separable_generator K E == some x \in E that generates the largest + subfield K[x] that is separable over K. + purely_inseparable_element K x <=> there is a [char L].-nat n such that + x ^+ n \in K. + purely_inseparable K E <=> every member of E is purely inseparable over K. + +<div class="paragraph"> </div> + + Derivations are introduced to prove the adjoin_separableP Lemma: + Derivation K D <=> the linear operator D satifies the Leibniz + product rule inside K. + extendDerivation x D K == given a derivation D on K and a separable + element x over K, this function returns the + unique extension of D to K(x). +</div> +<div class="code"> + +<br/> +<span class="id" title="keyword">Set Implicit Arguments</span>.<br/> + +<br/> +<span class="id" title="keyword">Local Open</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">ring_scope</span>.<br/> +<span class="id" title="keyword">Import</span> <span class="id" title="var">GRing.Theory</span>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="SeparablePoly"><span class="id" title="section">SeparablePoly</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variable</span> <a name="SeparablePoly.R"><span class="id" title="variable">R</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.IntegralDomain.Exports.idomainType"><span class="id" title="abbreviation">idomainType</span></a>.<br/> +<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> <span class="id" title="var">p</span> <span class="id" title="var">q</span> <span class="id" title="var">d</span> <span class="id" title="var">u</span> <span class="id" title="var">v</span> : <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.field.separable.html#SeparablePoly.R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="separable_poly"><span class="id" title="definition">separable_poly</span></a> <span class="id" title="var">p</span> := <a class="idref" href="mathcomp.algebra.polydiv.html#Pdiv.Field.coprimep"><span class="id" title="definition">coprimep</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#03bdc25c1ca3719165e27fca9d5b98af"><span class="id" title="notation">^`</span></a>.<br/> + +<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="separable_poly_neq0"><span class="id" title="lemma">separable_poly_neq0</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.field.separable.html#separable"><span class="id" title="abbreviation">separable</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="poly_square_freeP"><span class="id" title="lemma">poly_square_freeP</span></a> <span class="id" title="var">p</span> :<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#df1ced36fc33ce188051218bca314374"><span class="id" title="notation">(</span></a><span class="id" title="keyword">∀</span> <span class="id" title="var">u</span> <span class="id" title="var">v</span>, <a class="idref" href="mathcomp.field.separable.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.field.separable.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="mathcomp.algebra.polydiv.html#8d02531a91f8648b92789372c052c0ad"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polydiv.html#Pdiv.Field.coprimep"><span class="id" title="definition">coprimep</span></a> <a class="idref" href="mathcomp.field.separable.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.field.separable.html#v"><span class="id" title="variable">v</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#df1ced36fc33ce188051218bca314374"><span class="id" title="notation">)</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#df1ced36fc33ce188051218bca314374"><span class="id" title="notation">↔</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#df1ced36fc33ce188051218bca314374"><span class="id" title="notation">(</span></a><span class="id" title="keyword">∀</span> <span class="id" title="var">u</span>, <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.field.separable.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 1%<span class="id" title="var">N</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> <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="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.field.separable.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#fb22424322c3d7eb9b837dfca65ce21e"><span class="id" title="notation">^+</span></a> 2 <a class="idref" href="mathcomp.algebra.polydiv.html#8d02531a91f8648b92789372c052c0ad"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#df1ced36fc33ce188051218bca314374"><span class="id" title="notation">)</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="separable_polyP"><span class="id" title="lemma">separable_polyP</span></a> {<span class="id" title="var">p</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#4d70beb460e783df2b7b2ad387c00194"><span class="id" title="notation">[/\</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">u</span> <span class="id" title="var">v</span>, <a class="idref" href="mathcomp.field.separable.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.field.separable.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="mathcomp.algebra.polydiv.html#8d02531a91f8648b92789372c052c0ad"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polydiv.html#Pdiv.Field.coprimep"><span class="id" title="definition">coprimep</span></a> <a class="idref" href="mathcomp.field.separable.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.field.separable.html#v"><span class="id" title="variable">v</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4d70beb460e783df2b7b2ad387c00194"><span class="id" title="notation">&</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">u</span>, <a class="idref" href="mathcomp.field.separable.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.polydiv.html#8d02531a91f8648b92789372c052c0ad"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> 1 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation"><</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.field.separable.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.separable.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.algebra.poly.html#03bdc25c1ca3719165e27fca9d5b98af"><span class="id" title="notation">^`</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4d70beb460e783df2b7b2ad387c00194"><span class="id" title="notation">]</span></a><br/> + (<a class="idref" href="mathcomp.field.separable.html#separable"><span class="id" title="abbreviation">separable</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="separable_coprime"><span class="id" title="lemma">separable_coprime</span></a> <span class="id" title="var">p</span> <span class="id" title="var">u</span> <span class="id" title="var">v</span> : <a class="idref" href="mathcomp.field.separable.html#separable"><span class="id" title="abbreviation">separable</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.separable.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.field.separable.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="mathcomp.algebra.polydiv.html#8d02531a91f8648b92789372c052c0ad"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polydiv.html#Pdiv.Field.coprimep"><span class="id" title="definition">coprimep</span></a> <a class="idref" href="mathcomp.field.separable.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.field.separable.html#v"><span class="id" title="variable">v</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="separable_nosquare"><span class="id" title="lemma">separable_nosquare</span></a> <span class="id" title="var">p</span> <span class="id" title="var">u</span> <span class="id" title="var">k</span> :<br/> + <a class="idref" href="mathcomp.field.separable.html#separable"><span class="id" title="abbreviation">separable</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> 1 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation"><</span></a> <a class="idref" href="mathcomp.field.separable.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.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.field.separable.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 1%<span class="id" title="var">N</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> <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.field.separable.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#fb22424322c3d7eb9b837dfca65ce21e"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.field.separable.html#k"><span class="id" title="variable">k</span></a> <a class="idref" href="mathcomp.algebra.polydiv.html#8d02531a91f8648b92789372c052c0ad"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="separable_deriv_eq0"><span class="id" title="lemma">separable_deriv_eq0</span></a> <span class="id" title="var">p</span> <span class="id" title="var">u</span> :<br/> + <a class="idref" href="mathcomp.field.separable.html#separable"><span class="id" title="abbreviation">separable</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.separable.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.polydiv.html#8d02531a91f8648b92789372c052c0ad"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> 1 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation"><</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.field.separable.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.separable.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.algebra.poly.html#03bdc25c1ca3719165e27fca9d5b98af"><span class="id" title="notation">^`</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="dvdp_separable"><span class="id" title="lemma">dvdp_separable</span></a> <span class="id" title="var">p</span> <span class="id" title="var">q</span> : <a class="idref" href="mathcomp.field.separable.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.algebra.polydiv.html#8d02531a91f8648b92789372c052c0ad"><span class="id" title="notation">%|</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.separable.html#separable"><span class="id" title="abbreviation">separable</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.separable.html#separable"><span class="id" title="abbreviation">separable</span></a> <a class="idref" href="mathcomp.field.separable.html#q"><span class="id" title="variable">q</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="separable_mul"><span class="id" title="lemma">separable_mul</span></a> <span class="id" title="var">p</span> <span class="id" title="var">q</span> :<br/> + <a class="idref" href="mathcomp.field.separable.html#separable"><span class="id" title="abbreviation">separable</span></a> (<a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.field.separable.html#q"><span class="id" title="variable">q</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#2e9317c5f71a1305fb695cdc49716482"><span class="id" title="notation">[&&</span></a> <a class="idref" href="mathcomp.field.separable.html#separable"><span class="id" title="abbreviation">separable</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</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.field.separable.html#separable"><span class="id" title="abbreviation">separable</span></a> <a class="idref" href="mathcomp.field.separable.html#q"><span class="id" title="variable">q</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.algebra.polydiv.html#Pdiv.Field.coprimep"><span class="id" title="definition">coprimep</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.field.separable.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2e9317c5f71a1305fb695cdc49716482"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="eqp_separable"><span class="id" title="lemma">eqp_separable</span></a> <span class="id" title="var">p</span> <span class="id" title="var">q</span> : <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polydiv.html#9c1ccd33b816bf809c7479082caaf63e"><span class="id" title="notation">%=</span></a> <a class="idref" href="mathcomp.field.separable.html#q"><span class="id" title="variable">q</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.field.separable.html#separable"><span class="id" title="abbreviation">separable</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.field.separable.html#separable"><span class="id" title="abbreviation">separable</span></a> <a class="idref" href="mathcomp.field.separable.html#q"><span class="id" title="variable">q</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="separable_root"><span class="id" title="lemma">separable_root</span></a> <span class="id" title="var">p</span> <span class="id" title="var">x</span> :<br/> + <a class="idref" href="mathcomp.field.separable.html#separable"><span class="id" title="abbreviation">separable</span></a> (<a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.poly.html#ffd3fc7e3c529f4febe87040923e7332"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#ffd3fc7e3c529f4febe87040923e7332"><span class="id" title="notation">X</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#d70623330b2787db6b196e37db7d8f45"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#5d46c3ff21505243f65fdae89313c246"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.poly.html#5d46c3ff21505243f65fdae89313c246"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><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.field.separable.html#separable"><span class="id" title="abbreviation">separable</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">&&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">~~</span></a> <a class="idref" href="mathcomp.algebra.poly.html#root"><span class="id" title="definition">root</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="separable_prod_XsubC"><span class="id" title="lemma">separable_prod_XsubC</span></a> (<span class="id" title="var">r</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#seq"><span class="id" title="abbreviation">seq</span></a> <a class="idref" href="mathcomp.field.separable.html#SeparablePoly.R"><span class="id" title="variable">R</span></a>) :<br/> + <a class="idref" href="mathcomp.field.separable.html#separable"><span class="id" title="abbreviation">separable</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#add995903469f3735748795c8f1b81bd"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#add995903469f3735748795c8f1b81bd"><span class="id" title="notation">prod_</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#add995903469f3735748795c8f1b81bd"><span class="id" title="notation">(</span></a><span class="id" title="var">x</span> <a class="idref" href="mathcomp.algebra.ssralg.html#add995903469f3735748795c8f1b81bd"><span class="id" title="notation"><-</span></a> <a class="idref" href="mathcomp.field.separable.html#r"><span class="id" title="variable">r</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#add995903469f3735748795c8f1b81bd"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#add995903469f3735748795c8f1b81bd"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.poly.html#ffd3fc7e3c529f4febe87040923e7332"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#ffd3fc7e3c529f4febe87040923e7332"><span class="id" title="notation">X</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#d70623330b2787db6b196e37db7d8f45"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#5d46c3ff21505243f65fdae89313c246"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.poly.html#5d46c3ff21505243f65fdae89313c246"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#add995903469f3735748795c8f1b81bd"><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.seq.html#uniq"><span class="id" title="definition">uniq</span></a> <a class="idref" href="mathcomp.field.separable.html#r"><span class="id" title="variable">r</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="make_separable"><span class="id" title="lemma">make_separable</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0 <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.field.separable.html#separable"><span class="id" title="abbreviation">separable</span></a> (<a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polydiv.html#6a276cc55c6f28b3ec69a3618ce07a9c"><span class="id" title="notation">%/</span></a> <a class="idref" href="mathcomp.algebra.polydiv.html#Pdiv.Field.gcdp"><span class="id" title="definition">gcdp</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#03bdc25c1ca3719165e27fca9d5b98af"><span class="id" title="notation">^`</span></a>).<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.separable.html#SeparablePoly"><span class="id" title="section">SeparablePoly</span></a>.<br/> + +<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="separable_map"><span class="id" title="lemma">separable_map</span></a> (<span class="id" title="var">F</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Field.Exports.fieldType"><span class="id" title="abbreviation">fieldType</span></a>) (<span class="id" title="var">R</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.IntegralDomain.Exports.idomainType"><span class="id" title="abbreviation">idomainType</span></a>)<br/> + (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">rmorphism</span></a> <a class="idref" href="mathcomp.field.separable.html#F"><span class="id" title="variable">F</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.field.separable.html#R"><span class="id" title="variable">R</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.field.separable.html#F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">}</span></a>) :<br/> + <a class="idref" href="mathcomp.field.separable.html#separable_poly"><span class="id" title="definition">separable_poly</span></a> (<a class="idref" href="mathcomp.algebra.poly.html#map_poly"><span class="id" title="definition">map_poly</span></a> <a class="idref" href="mathcomp.field.separable.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.field.separable.html#separable_poly"><span class="id" title="definition">separable_poly</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="InfinitePrimitiveElementTheorem"><span class="id" title="section">InfinitePrimitiveElementTheorem</span></a>.<br/> + +<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="InfinitePrimitiveElementTheorem.F"><span class="id" title="variable">F</span></a> <a name="InfinitePrimitiveElementTheorem.L"><span class="id" title="variable">L</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Field.Exports.fieldType"><span class="id" title="abbreviation">fieldType</span></a>) (<a name="InfinitePrimitiveElementTheorem.iota"><span class="id" title="variable">iota</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">rmorphism</span></a> <a class="idref" href="mathcomp.field.separable.html#F"><span class="id" title="variable">F</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.field.separable.html#L"><span class="id" title="variable">L</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0c709ebe43ddbd7719f75250a7b916d9"><span class="id" title="notation">}</span></a>).<br/> +<span class="id" title="keyword">Variables</span> (<a name="InfinitePrimitiveElementTheorem.x"><span class="id" title="variable">x</span></a> <a name="InfinitePrimitiveElementTheorem.y"><span class="id" title="variable">y</span></a> : <a class="idref" href="mathcomp.field.separable.html#InfinitePrimitiveElementTheorem.L"><span class="id" title="variable">L</span></a>) (<a name="InfinitePrimitiveElementTheorem.p"><span class="id" title="variable">p</span></a> : <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.field.separable.html#InfinitePrimitiveElementTheorem.F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">}</span></a>).<br/> +<span class="id" title="keyword">Hypotheses</span> (<a name="InfinitePrimitiveElementTheorem.nz_p"><span class="id" title="variable">nz_p</span></a> : <a class="idref" href="mathcomp.field.separable.html#InfinitePrimitiveElementTheorem.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0) (<a name="InfinitePrimitiveElementTheorem.px_0"><span class="id" title="variable">px_0</span></a> : <a class="idref" href="mathcomp.algebra.poly.html#root"><span class="id" title="definition">root</span></a> (<a class="idref" href="mathcomp.field.separable.html#InfinitePrimitiveElementTheorem.p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.field.separable.html#59212b1a12dae621b413316be212d437"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.field.separable.html#InfinitePrimitiveElementTheorem.iota"><span class="id" title="variable">iota</span></a>) <a class="idref" href="mathcomp.field.separable.html#InfinitePrimitiveElementTheorem.x"><span class="id" title="variable">x</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Let</span> <a name="InfinitePrimitiveElementTheorem.inFz"><span class="id" title="variable">inFz</span></a> <span class="id" title="var">z</span> <span class="id" title="var">w</span> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">q</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.separable.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.field.separable.html#59212b1a12dae621b413316be212d437"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.field.separable.html#InfinitePrimitiveElementTheorem.iota"><span class="id" title="variable">iota</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.field.separable.html#z"><span class="id" title="variable">z</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><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.field.separable.html#w"><span class="id" title="variable">w</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="large_field_PET"><span class="id" title="lemma">large_field_PET</span></a> <span class="id" title="var">q</span> :<br/> + <a class="idref" href="mathcomp.algebra.poly.html#root"><span class="id" title="definition">root</span></a> (<a class="idref" href="mathcomp.field.separable.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.field.separable.html#59212b1a12dae621b413316be212d437"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.field.separable.html#InfinitePrimitiveElementTheorem.iota"><span class="id" title="variable">iota</span></a>) <a class="idref" href="mathcomp.field.separable.html#InfinitePrimitiveElementTheorem.y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.separable.html#separable_poly"><span class="id" title="definition">separable_poly</span></a> <a class="idref" href="mathcomp.field.separable.html#q"><span class="id" title="variable">q</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.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">r</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.field.separable.html#r"><span class="id" title="variable">r</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0<br/> + <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> <span class="id" title="keyword">∀</span> <span class="id" title="var">t</span> (<span class="id" title="var">z</span> := <a class="idref" href="mathcomp.field.separable.html#InfinitePrimitiveElementTheorem.iota"><span class="id" title="variable">iota</span></a> <a class="idref" href="mathcomp.field.separable.html#t"><span class="id" title="variable">t</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.field.separable.html#InfinitePrimitiveElementTheorem.y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#d70623330b2787db6b196e37db7d8f45"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.field.separable.html#InfinitePrimitiveElementTheorem.x"><span class="id" title="variable">x</span></a>), <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#4b80c70cdb231351c5e129ba61f7f956"><span class="id" title="notation">~~</span></a> <a class="idref" href="mathcomp.algebra.poly.html#root"><span class="id" title="definition">root</span></a> <a class="idref" href="mathcomp.field.separable.html#r"><span class="id" title="variable">r</span></a> (<a class="idref" href="mathcomp.field.separable.html#InfinitePrimitiveElementTheorem.iota"><span class="id" title="variable">iota</span></a> <a class="idref" href="mathcomp.field.separable.html#t"><span class="id" title="variable">t</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.separable.html#InfinitePrimitiveElementTheorem.inFz"><span class="id" title="variable">inFz</span></a> <a class="idref" href="mathcomp.field.separable.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.field.separable.html#InfinitePrimitiveElementTheorem.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#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="mathcomp.field.separable.html#InfinitePrimitiveElementTheorem.inFz"><span class="id" title="variable">inFz</span></a> <a class="idref" href="mathcomp.field.separable.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.field.separable.html#InfinitePrimitiveElementTheorem.y"><span class="id" title="variable">y</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="char0_PET"><span class="id" title="lemma">char0_PET</span></a> (<span class="id" title="var">q</span> : <a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">poly</span></a> <a class="idref" href="mathcomp.field.separable.html#InfinitePrimitiveElementTheorem.F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.algebra.poly.html#699040ddc0986f520cece215f531d947"><span class="id" title="notation">}</span></a>) :<br/> + <a class="idref" href="mathcomp.field.separable.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0 <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.algebra.poly.html#root"><span class="id" title="definition">root</span></a> (<a class="idref" href="mathcomp.field.separable.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.field.separable.html#59212b1a12dae621b413316be212d437"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.field.separable.html#InfinitePrimitiveElementTheorem.iota"><span class="id" title="variable">iota</span></a>) <a class="idref" href="mathcomp.field.separable.html#InfinitePrimitiveElementTheorem.y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.field.separable.html#InfinitePrimitiveElementTheorem.F"><span class="id" title="variable">F</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#20bf07099d6d8cf369383b22fd37862e"><span class="id" title="notation">=</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#20bf07099d6d8cf369383b22fd37862e"><span class="id" title="notation">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred0"><span class="id" title="definition">pred0</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.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">n</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a> <span class="id" title="keyword">let</span> <span class="id" title="var">z</span> := <a class="idref" href="mathcomp.field.separable.html#InfinitePrimitiveElementTheorem.y"><span class="id" title="variable">y</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#891e51846c7d1d63a9cb5458374cf308"><span class="id" title="notation">*+</span></a> <a class="idref" href="mathcomp.field.separable.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#d70623330b2787db6b196e37db7d8f45"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.field.separable.html#InfinitePrimitiveElementTheorem.x"><span class="id" title="variable">x</span></a> <span class="id" title="tactic">in</span> <a class="idref" href="mathcomp.field.separable.html#InfinitePrimitiveElementTheorem.inFz"><span class="id" title="variable">inFz</span></a> <a class="idref" href="mathcomp.field.separable.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.field.separable.html#InfinitePrimitiveElementTheorem.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#d82a7d96d3659d805ffe732283716822"><span class="id" title="notation">∧</span></a> <a class="idref" href="mathcomp.field.separable.html#InfinitePrimitiveElementTheorem.inFz"><span class="id" title="variable">inFz</span></a> <a class="idref" href="mathcomp.field.separable.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.field.separable.html#InfinitePrimitiveElementTheorem.y"><span class="id" title="variable">y</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.separable.html#InfinitePrimitiveElementTheorem"><span class="id" title="section">InfinitePrimitiveElementTheorem</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="Separable"><span class="id" title="section">Separable</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="Separable.F"><span class="id" title="variable">F</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Field.Exports.fieldType"><span class="id" title="abbreviation">fieldType</span></a>) (<a name="Separable.L"><span class="id" title="variable">L</span></a> : <a class="idref" href="mathcomp.field.fieldext.html#FieldExt.Exports.fieldExtType"><span class="id" title="abbreviation">fieldExtType</span></a> <a class="idref" href="mathcomp.field.separable.html#F"><span class="id" title="variable">F</span></a>).<br/> +<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">U</span> <span class="id" title="var">V</span> <span class="id" title="var">W</span> : <a class="idref" href="mathcomp.algebra.vector.html#ca0a177f6d6581a7f5199987cd7ee21c"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.vector.html#ca0a177f6d6581a7f5199987cd7ee21c"><span class="id" title="notation">vspace</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.L"><span class="id" title="variable">L</span></a><a class="idref" href="mathcomp.algebra.vector.html#ca0a177f6d6581a7f5199987cd7ee21c"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">E</span> <span class="id" title="var">K</span> <span class="id" title="var">M</span> : <a class="idref" href="mathcomp.field.fieldext.html#da0a594fae595c8172b1a3e2dd69d19d"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.field.fieldext.html#da0a594fae595c8172b1a3e2dd69d19d"><span class="id" title="notation">subfield</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.L"><span class="id" title="variable">L</span></a><a class="idref" href="mathcomp.field.fieldext.html#da0a594fae595c8172b1a3e2dd69d19d"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">D</span> : <a class="idref" href="mathcomp.algebra.vector.html#f2977b5d91be916157fc34deec16772c"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.vector.html#f2977b5d91be916157fc34deec16772c"><span class="id" title="notation">End</span></a><a class="idref" href="mathcomp.algebra.vector.html#f2977b5d91be916157fc34deec16772c"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.separable.html#Separable.L"><span class="id" title="variable">L</span></a><a class="idref" href="mathcomp.algebra.vector.html#f2977b5d91be916157fc34deec16772c"><span class="id" title="notation">)</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="Separable.Derivation"><span class="id" title="section">Derivation</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="Separable.Derivation.K"><span class="id" title="variable">K</span></a> : <a class="idref" href="mathcomp.algebra.vector.html#ca0a177f6d6581a7f5199987cd7ee21c"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.vector.html#ca0a177f6d6581a7f5199987cd7ee21c"><span class="id" title="notation">vspace</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.L"><span class="id" title="variable">L</span></a><a class="idref" href="mathcomp.algebra.vector.html#ca0a177f6d6581a7f5199987cd7ee21c"><span class="id" title="notation">}</span></a>) (<a name="Separable.Derivation.D"><span class="id" title="variable">D</span></a> : <a class="idref" href="mathcomp.algebra.vector.html#f2977b5d91be916157fc34deec16772c"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.vector.html#f2977b5d91be916157fc34deec16772c"><span class="id" title="notation">End</span></a><a class="idref" href="mathcomp.algebra.vector.html#f2977b5d91be916157fc34deec16772c"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.separable.html#Separable.L"><span class="id" title="variable">L</span></a><a class="idref" href="mathcomp.algebra.vector.html#f2977b5d91be916157fc34deec16772c"><span class="id" title="notation">)</span></a>).<br/> + +<br/> +</div> + +<div class="doc"> + A deriviation only needs to be additive and satify Lebniz's law, but all + the deriviations used here are going to be linear, so we only define + the Derivation predicate for linear endomorphisms. +</div> +<div class="code"> +<span class="id" title="keyword">Definition</span> <a name="Derivation"><span class="id" title="definition">Derivation</span></a> (<span class="id" title="var">s</span> := <a class="idref" href="mathcomp.algebra.vector.html#vbasis"><span class="id" title="definition">vbasis</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.Derivation.K"><span class="id" title="variable">K</span></a>) : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a> :=<br/> + <a class="idref" href="mathcomp.ssreflect.seq.html#all"><span class="id" title="definition">all</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">u</span> ⇒ <a class="idref" href="mathcomp.ssreflect.seq.html#all"><span class="id" title="definition">all</span></a> (<span class="id" title="keyword">fun</span> <span class="id" title="var">v</span> ⇒ <a class="idref" href="mathcomp.field.separable.html#Separable.Derivation.D"><span class="id" title="variable">D</span></a> (<a class="idref" href="mathcomp.field.separable.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.field.separable.html#v"><span class="id" title="variable">v</span></a>) <a class="idref" href="mathcomp.ssreflect.eqtype.html#17d28d004d0863cb022d4ce832ddaaae"><span class="id" title="notation">==</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.Derivation.D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.field.separable.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.field.separable.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#ae4d81913e6239182a9ac7467ffde8cd"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.field.separable.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.Derivation.D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.field.separable.html#v"><span class="id" title="variable">v</span></a>) <a class="idref" href="mathcomp.field.separable.html#s"><span class="id" title="variable">s</span></a>) <a class="idref" href="mathcomp.field.separable.html#s"><span class="id" title="variable">s</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Hypothesis</span> <a name="Separable.Derivation.derD"><span class="id" title="variable">derD</span></a> : <a class="idref" href="mathcomp.field.separable.html#Derivation"><span class="id" title="definition">Derivation</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Derivation_mul"><span class="id" title="lemma">Derivation_mul</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.Derivation.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#2bba53854f326a714d377124cccec593"><span class="id" title="notation">&,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">u</span> <span class="id" title="var">v</span>, <a class="idref" href="mathcomp.field.separable.html#Separable.Derivation.D"><span class="id" title="variable">D</span></a> (<a class="idref" href="mathcomp.field.separable.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.field.separable.html#v"><span class="id" title="variable">v</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.Derivation.D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.field.separable.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.field.separable.html#v"><span class="id" title="variable">v</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#ae4d81913e6239182a9ac7467ffde8cd"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.field.separable.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.Derivation.D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.field.separable.html#v"><span class="id" title="variable">v</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Derivation_mul_poly"><span class="id" title="lemma">Derivation_mul_poly</span></a> (<span class="id" title="var">Dp</span> := <a class="idref" href="mathcomp.algebra.poly.html#map_poly"><span class="id" title="definition">map_poly</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.Derivation.D"><span class="id" title="variable">D</span></a>) :<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.poly.html#polyOver"><span class="id" title="definition">polyOver</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.Derivation.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#2bba53854f326a714d377124cccec593"><span class="id" title="notation">&,</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">p</span> <span class="id" title="var">q</span>, <a class="idref" href="mathcomp.field.separable.html#Dp"><span class="id" title="variable">Dp</span></a> (<a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.field.separable.html#q"><span class="id" title="variable">q</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.field.separable.html#Dp"><span class="id" title="variable">Dp</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.field.separable.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#ae4d81913e6239182a9ac7467ffde8cd"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.field.separable.html#Dp"><span class="id" title="variable">Dp</span></a> <a class="idref" href="mathcomp.field.separable.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#2bba53854f326a714d377124cccec593"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.separable.html#Separable.Derivation"><span class="id" title="section">Derivation</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="DerivationS"><span class="id" title="lemma">DerivationS</span></a> <span class="id" title="var">E</span> <span class="id" title="var">K</span> <span class="id" title="var">D</span> : (<a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.algebra.vector.html#755d11a7d5629bce3486e7cbadc915e7"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</span></a>)%<span class="id" title="var">VS</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> <a class="idref" href="mathcomp.field.separable.html#Derivation"><span class="id" title="definition">Derivation</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</span></a> <a class="idref" href="mathcomp.field.separable.html#D"><span class="id" title="variable">D</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.field.separable.html#Derivation"><span class="id" title="definition">Derivation</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#D"><span class="id" title="variable">D</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="Separable.DerivationAlgebra"><span class="id" title="section">DerivationAlgebra</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="Separable.DerivationAlgebra.E"><span class="id" title="variable">E</span></a> : <a class="idref" href="mathcomp.field.fieldext.html#da0a594fae595c8172b1a3e2dd69d19d"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.field.fieldext.html#da0a594fae595c8172b1a3e2dd69d19d"><span class="id" title="notation">subfield</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.L"><span class="id" title="variable">L</span></a><a class="idref" href="mathcomp.field.fieldext.html#da0a594fae595c8172b1a3e2dd69d19d"><span class="id" title="notation">}</span></a>) (<a name="Separable.DerivationAlgebra.D"><span class="id" title="variable">D</span></a> : <a class="idref" href="mathcomp.algebra.vector.html#f2977b5d91be916157fc34deec16772c"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.vector.html#f2977b5d91be916157fc34deec16772c"><span class="id" title="notation">End</span></a><a class="idref" href="mathcomp.algebra.vector.html#f2977b5d91be916157fc34deec16772c"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.separable.html#Separable.L"><span class="id" title="variable">L</span></a><a class="idref" href="mathcomp.algebra.vector.html#f2977b5d91be916157fc34deec16772c"><span class="id" title="notation">)</span></a>).<br/> +<span class="id" title="keyword">Hypothesis</span> <a name="Separable.DerivationAlgebra.derD"><span class="id" title="variable">derD</span></a> : <a class="idref" href="mathcomp.field.separable.html#Derivation"><span class="id" title="definition">Derivation</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.DerivationAlgebra.E"><span class="id" title="variable">E</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.DerivationAlgebra.D"><span class="id" title="variable">D</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Derivation1"><span class="id" title="lemma">Derivation1</span></a> : <a class="idref" href="mathcomp.field.separable.html#Separable.DerivationAlgebra.D"><span class="id" title="variable">D</span></a> 1 <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 0.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Derivation_scalar"><span class="id" title="lemma">Derivation_scalar</span></a> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> 1%<span class="id" title="var">VS</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> <a class="idref" href="mathcomp.field.separable.html#Separable.DerivationAlgebra.D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> 0.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Derivation_exp"><span class="id" title="lemma">Derivation_exp</span></a> <span class="id" title="var">x</span> <span class="id" title="var">m</span> : <a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.DerivationAlgebra.E"><span class="id" title="variable">E</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.field.separable.html#Separable.DerivationAlgebra.D"><span class="id" title="variable">D</span></a> (<a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#fb22424322c3d7eb9b837dfca65ce21e"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.field.separable.html#m"><span class="id" title="variable">m</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#fb22424322c3d7eb9b837dfca65ce21e"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.field.separable.html#m"><span class="id" title="variable">m</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#1d63841e595f2805afd872744cbb1cce"><span class="id" title="notation">.-1</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#891e51846c7d1d63a9cb5458374cf308"><span class="id" title="notation">*+</span></a> <a class="idref" href="mathcomp.field.separable.html#m"><span class="id" title="variable">m</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.DerivationAlgebra.D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Derivation_horner"><span class="id" title="lemma">Derivation_horner</span></a> <span class="id" title="var">p</span> <span class="id" title="var">x</span> :<br/> + <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#1e40fee506a85b20590ef299005b003d"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#1e40fee506a85b20590ef299005b003d"><span class="id" title="notation">is</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#1e40fee506a85b20590ef299005b003d"><span class="id" title="notation">a</span></a> <a class="idref" href="mathcomp.algebra.poly.html#polyOver"><span class="id" title="definition">polyOver</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.DerivationAlgebra.E"><span class="id" title="variable">E</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.field.separable.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.DerivationAlgebra.E"><span class="id" title="variable">E</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.field.separable.html#Separable.DerivationAlgebra.D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><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.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.poly.html#map_poly"><span class="id" title="definition">map_poly</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.DerivationAlgebra.D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#ae4d81913e6239182a9ac7467ffde8cd"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#03bdc25c1ca3719165e27fca9d5b98af"><span class="id" title="notation">^`</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.DerivationAlgebra.D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.separable.html#Separable.DerivationAlgebra"><span class="id" title="section">DerivationAlgebra</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="separable_element"><span class="id" title="definition">separable_element</span></a> <span class="id" title="var">U</span> <span class="id" title="var">x</span> := <a class="idref" href="mathcomp.field.separable.html#separable_poly"><span class="id" title="definition">separable_poly</span></a> (<a class="idref" href="mathcomp.field.fieldext.html#minPoly"><span class="id" title="definition">minPoly</span></a> <a class="idref" href="mathcomp.field.separable.html#U"><span class="id" title="variable">U</span></a> <a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="Separable.SeparableElement"><span class="id" title="section">SeparableElement</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="Separable.SeparableElement.K"><span class="id" title="variable">K</span></a> : <a class="idref" href="mathcomp.field.fieldext.html#da0a594fae595c8172b1a3e2dd69d19d"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.field.fieldext.html#da0a594fae595c8172b1a3e2dd69d19d"><span class="id" title="notation">subfield</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.L"><span class="id" title="variable">L</span></a><a class="idref" href="mathcomp.field.fieldext.html#da0a594fae595c8172b1a3e2dd69d19d"><span class="id" title="notation">}</span></a>) (<a name="Separable.SeparableElement.x"><span class="id" title="variable">x</span></a> : <a class="idref" href="mathcomp.field.separable.html#Separable.L"><span class="id" title="variable">L</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="separable_elementP"><span class="id" title="lemma">separable_elementP</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="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">f</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><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> <a class="idref" href="mathcomp.field.separable.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#1e40fee506a85b20590ef299005b003d"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#1e40fee506a85b20590ef299005b003d"><span class="id" title="notation">is</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#1e40fee506a85b20590ef299005b003d"><span class="id" title="notation">a</span></a> <a class="idref" href="mathcomp.algebra.poly.html#polyOver"><span class="id" title="definition">polyOver</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.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#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.poly.html#root"><span class="id" title="definition">root</span></a> <a class="idref" href="mathcomp.field.separable.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.field.separable.html#separable_poly"><span class="id" title="definition">separable_poly</span></a> <a class="idref" href="mathcomp.field.separable.html#f"><span class="id" title="variable">f</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.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.x"><span class="id" title="variable">x</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="base_separable"><span class="id" title="lemma">base_separable</span></a> : <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.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.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="separable_nz_der"><span class="id" title="lemma">separable_nz_der</span></a> : <a class="idref" href="mathcomp.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.poly.html#03bdc25c1ca3719165e27fca9d5b98af"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.fieldext.html#minPoly"><span class="id" title="definition">minPoly</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#03bdc25c1ca3719165e27fca9d5b98af"><span class="id" title="notation">)^`</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="separablePn"><span class="id" title="lemma">separablePn</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="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">p</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.field.separable.html#p"><span class="id" title="variable">p</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.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.L"><span class="id" title="variable">L</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><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">&</span></a> <br/> + <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">g</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.field.separable.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#1e40fee506a85b20590ef299005b003d"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#1e40fee506a85b20590ef299005b003d"><span class="id" title="notation">is</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#1e40fee506a85b20590ef299005b003d"><span class="id" title="notation">a</span></a> <a class="idref" href="mathcomp.algebra.poly.html#polyOver"><span class="id" title="definition">polyOver</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.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#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.field.fieldext.html#minPoly"><span class="id" title="definition">minPoly</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.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.field.separable.html#g"><span class="id" title="variable">g</span></a> <a class="idref" href="mathcomp.algebra.poly.html#cad3d28b9cdd7490720002e244568365"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.poly.html#cad3d28b9cdd7490720002e244568365"><span class="id" title="notation">Po</span></a> <a class="idref" href="mathcomp.algebra.poly.html#9f0d1035fe3072a93b6e6065c1932def"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#9f0d1035fe3072a93b6e6065c1932def"><span class="id" title="notation">X</span></a><a class="idref" href="mathcomp.algebra.poly.html#9f0d1035fe3072a93b6e6065c1932def"><span class="id" title="notation">^</span></a><a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a>)<br/> + (<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.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.x"><span class="id" title="variable">x</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="separable_root_der"><span class="id" title="lemma">separable_root_der</span></a> : <a class="idref" href="mathcomp.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#ef177bde7d01ae97c98f9cba81f6c95b"><span class="id" title="notation">(+)</span></a> <a class="idref" href="mathcomp.algebra.poly.html#root"><span class="id" title="definition">root</span></a> <a class="idref" href="mathcomp.algebra.poly.html#03bdc25c1ca3719165e27fca9d5b98af"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.fieldext.html#minPoly"><span class="id" title="definition">minPoly</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#03bdc25c1ca3719165e27fca9d5b98af"><span class="id" title="notation">)^`</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Derivation_separable"><span class="id" title="lemma">Derivation_separable</span></a> <span class="id" title="var">D</span> :<br/> + <a class="idref" href="mathcomp.field.separable.html#Derivation"><span class="id" title="definition">Derivation</span></a> <a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation"><<</span></a><a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">;</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">>></span></a> <a class="idref" href="mathcomp.field.separable.html#D"><span class="id" title="variable">D</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.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.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#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.field.separable.html#D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.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.algebra.ssralg.html#941c6d086004545bd62614d0213e75e5"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.poly.html#map_poly"><span class="id" title="definition">map_poly</span></a> <a class="idref" href="mathcomp.field.separable.html#D"><span class="id" title="variable">D</span></a> (<a class="idref" href="mathcomp.field.fieldext.html#minPoly"><span class="id" title="definition">minPoly</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.x"><span class="id" title="variable">x</span></a>)<a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#4fa85b0aa898c2a7e18c3b076438c2e7"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.poly.html#03bdc25c1ca3719165e27fca9d5b98af"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.fieldext.html#minPoly"><span class="id" title="definition">minPoly</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#03bdc25c1ca3719165e27fca9d5b98af"><span class="id" title="notation">)^`</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="Separable.SeparableElement.ExtendDerivation"><span class="id" title="section">ExtendDerivation</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variable</span> <a name="Separable.SeparableElement.ExtendDerivation.D"><span class="id" title="variable">D</span></a> : <a class="idref" href="mathcomp.algebra.vector.html#f2977b5d91be916157fc34deec16772c"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.vector.html#f2977b5d91be916157fc34deec16772c"><span class="id" title="notation">End</span></a><a class="idref" href="mathcomp.algebra.vector.html#f2977b5d91be916157fc34deec16772c"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.separable.html#Separable.L"><span class="id" title="variable">L</span></a><a class="idref" href="mathcomp.algebra.vector.html#f2977b5d91be916157fc34deec16772c"><span class="id" title="notation">)</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Let</span> <a name="Separable.SeparableElement.ExtendDerivation.Dx"><span class="id" title="variable">Dx</span></a> <span class="id" title="var">E</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#941c6d086004545bd62614d0213e75e5"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.poly.html#map_poly"><span class="id" title="definition">map_poly</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.ExtendDerivation.D"><span class="id" title="variable">D</span></a> (<a class="idref" href="mathcomp.field.fieldext.html#minPoly"><span class="id" title="definition">minPoly</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.x"><span class="id" title="variable">x</span></a>)<a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#4fa85b0aa898c2a7e18c3b076438c2e7"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.poly.html#03bdc25c1ca3719165e27fca9d5b98af"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.fieldext.html#minPoly"><span class="id" title="definition">minPoly</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#03bdc25c1ca3719165e27fca9d5b98af"><span class="id" title="notation">)^`</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Fact</span> <a name="extendDerivation_subproof"><span class="id" title="lemma">extendDerivation_subproof</span></a> <span class="id" title="var">E</span> (<span class="id" title="var">adjEx</span> := <a class="idref" href="mathcomp.field.fieldext.html#Fadjoin_poly"><span class="id" title="definition">Fadjoin_poly</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.x"><span class="id" title="variable">x</span></a>) :<br/> + <span class="id" title="keyword">let</span> <span class="id" title="var">body</span> <span class="id" title="var">y</span> (<span class="id" title="var">p</span> := <a class="idref" href="mathcomp.field.separable.html#adjEx"><span class="id" title="variable">adjEx</span></a> <a class="idref" href="mathcomp.field.separable.html#y"><span class="id" title="variable">y</span></a>) := <a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.poly.html#map_poly"><span class="id" title="definition">map_poly</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.ExtendDerivation.D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#ae4d81913e6239182a9ac7467ffde8cd"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#03bdc25c1ca3719165e27fca9d5b98af"><span class="id" title="notation">^`</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.ExtendDerivation.Dx"><span class="id" title="variable">Dx</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</span></a> <span class="id" title="tactic">in</span><br/> + <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Linear.Exports.linear"><span class="id" title="abbreviation">linear</span></a> <a class="idref" href="mathcomp.field.separable.html#body"><span class="id" title="variable">body</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="extendDerivation"><span class="id" title="definition">extendDerivation</span></a> <span class="id" title="var">E</span> : <a class="idref" href="mathcomp.algebra.vector.html#f2977b5d91be916157fc34deec16772c"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.vector.html#f2977b5d91be916157fc34deec16772c"><span class="id" title="notation">End</span></a><a class="idref" href="mathcomp.algebra.vector.html#f2977b5d91be916157fc34deec16772c"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.separable.html#Separable.L"><span class="id" title="variable">L</span></a><a class="idref" href="mathcomp.algebra.vector.html#f2977b5d91be916157fc34deec16772c"><span class="id" title="notation">)</span></a> :=<br/> + <a class="idref" href="mathcomp.algebra.vector.html#linfun"><span class="id" title="definition">linfun</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Linear.Exports.Linear"><span class="id" title="abbreviation">Linear</span></a> (<a class="idref" href="mathcomp.field.separable.html#extendDerivation_subproof"><span class="id" title="lemma">extendDerivation_subproof</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</span></a>)).<br/> + +<br/> +<span class="id" title="keyword">Hypothesis</span> <a name="Separable.SeparableElement.ExtendDerivation.derD"><span class="id" title="variable">derD</span></a> : <a class="idref" href="mathcomp.field.separable.html#Derivation"><span class="id" title="definition">Derivation</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.ExtendDerivation.D"><span class="id" title="variable">D</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="extendDerivation_id"><span class="id" title="lemma">extendDerivation_id</span></a> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.field.separable.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.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.field.separable.html#extendDerivation"><span class="id" title="definition">extendDerivation</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.ExtendDerivation.D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.field.separable.html#y"><span class="id" title="variable">y</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="extendDerivation_horner"><span class="id" title="lemma">extendDerivation_horner</span></a> <span class="id" title="var">p</span> :<br/> + <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#1e40fee506a85b20590ef299005b003d"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#1e40fee506a85b20590ef299005b003d"><span class="id" title="notation">is</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#1e40fee506a85b20590ef299005b003d"><span class="id" title="notation">a</span></a> <a class="idref" href="mathcomp.algebra.poly.html#polyOver"><span class="id" title="definition">polyOver</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.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.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.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#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.field.separable.html#extendDerivation"><span class="id" title="definition">extendDerivation</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><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.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.poly.html#map_poly"><span class="id" title="definition">map_poly</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.ExtendDerivation.D"><span class="id" title="variable">D</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#ae4d81913e6239182a9ac7467ffde8cd"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#03bdc25c1ca3719165e27fca9d5b98af"><span class="id" title="notation">^`</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.poly.html#9956cd3926e9966aa6979e465e39d037"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#22058a36a53dac65c94ca403bc62650a"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.ExtendDerivation.Dx"><span class="id" title="variable">Dx</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.K"><span class="id" title="variable">K</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="extendDerivationP"><span class="id" title="lemma">extendDerivationP</span></a> :<br/> + <a class="idref" href="mathcomp.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.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#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.separable.html#Derivation"><span class="id" title="definition">Derivation</span></a> <a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation"><<</span></a><a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">;</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">>></span></a> (<a class="idref" href="mathcomp.field.separable.html#extendDerivation"><span class="id" title="definition">extendDerivation</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.K"><span class="id" title="variable">K</span></a>).<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.ExtendDerivation"><span class="id" title="section">ExtendDerivation</span></a>.<br/> + +<br/> +</div> + +<div class="doc"> + Reference: +http://www.math.uconn.edu/~kconrad/blurbs/galoistheory/separable2.pdf +</div> +<div class="code"> +<span class="id" title="keyword">Lemma</span> <a name="Derivation_separableP"><span class="id" title="lemma">Derivation_separableP</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><br/> + (<span class="id" title="keyword">∀</span> <span class="id" title="var">D</span>, <a class="idref" href="mathcomp.field.separable.html#Derivation"><span class="id" title="definition">Derivation</span></a> <a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation"><<</span></a><a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">;</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">>></span></a> <a class="idref" href="mathcomp.field.separable.html#D"><span class="id" title="variable">D</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.field.separable.html#Separable.SeparableElement.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.algebra.vector.html#755d11a7d5629bce3486e7cbadc915e7"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.vector.html#lker"><span class="id" title="definition">lker</span></a> <a class="idref" href="mathcomp.field.separable.html#D"><span class="id" title="variable">D</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.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation"><<</span></a><a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">;</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">>></span></a> <a class="idref" href="mathcomp.algebra.vector.html#755d11a7d5629bce3486e7cbadc915e7"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.vector.html#lker"><span class="id" title="definition">lker</span></a> <a class="idref" href="mathcomp.field.separable.html#D"><span class="id" title="variable">D</span></a>)%<span class="id" title="var">VS</span><br/> + (<a class="idref" href="mathcomp.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.x"><span class="id" title="variable">x</span></a>).<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement"><span class="id" title="section">SeparableElement</span></a>.<br/> + +<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="separable_elementS"><span class="id" title="lemma">separable_elementS</span></a> <span class="id" title="var">K</span> <span class="id" title="var">E</span> <span class="id" title="var">x</span> :<br/> + (<a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.algebra.vector.html#755d11a7d5629bce3486e7cbadc915e7"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</span></a>)%<span class="id" title="var">VS</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> <a class="idref" href="mathcomp.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.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#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</span></a> <a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="adjoin_separableP"><span class="id" title="lemma">adjoin_separableP</span></a> {<span class="id" title="var">K</span> <span class="id" title="var">x</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> (<span class="id" title="keyword">∀</span> <span class="id" title="var">y</span>, <a class="idref" href="mathcomp.field.separable.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation"><<</span></a><a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">;</span></a> <a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">>></span></a>%<span class="id" title="var">VS</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> <a class="idref" href="mathcomp.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#y"><span class="id" title="variable">y</span></a>)<br/> + (<a class="idref" href="mathcomp.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="separable_exponent"><span class="id" title="lemma">separable_exponent</span></a> <span class="id" title="var">K</span> <span class="id" title="var">x</span> :<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">n</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.L"><span class="id" title="variable">L</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#8663a77d1d910826e10ba42d1e8d2a02"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#8663a77d1d910826e10ba42d1e8d2a02"><span class="id" title="notation">nat</span></a> <a class="idref" href="mathcomp.field.separable.html#n"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">&&</span></a> <a class="idref" href="mathcomp.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> (<a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#fb22424322c3d7eb9b837dfca65ce21e"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.field.separable.html#n"><span class="id" title="variable">n</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="charf0_separable"><span class="id" title="lemma">charf0_separable</span></a> <span class="id" title="var">K</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.L"><span class="id" title="variable">L</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#20bf07099d6d8cf369383b22fd37862e"><span class="id" title="notation">=</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#20bf07099d6d8cf369383b22fd37862e"><span class="id" title="notation">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred0"><span class="id" title="definition">pred0</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> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span>, <a class="idref" href="mathcomp.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="charf_p_separable"><span class="id" title="lemma">charf_p_separable</span></a> <span class="id" title="var">K</span> <span class="id" title="var">x</span> <span class="id" title="var">e</span> <span class="id" title="var">p</span> :<br/> + <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</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.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.L"><span class="id" title="variable">L</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><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.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation"><<</span></a><a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">;</span></a> <a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#fb22424322c3d7eb9b837dfca65ce21e"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#fb22424322c3d7eb9b837dfca65ce21e"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#4c362bcf0e947e2792a2e6989b44aeb0"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.field.separable.html#e"><span class="id" title="variable">e</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#fb22424322c3d7eb9b837dfca65ce21e"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">>></span></a>%<span class="id" title="var">VS</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>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="charf_n_separable"><span class="id" title="lemma">charf_n_separable</span></a> <span class="id" title="var">K</span> <span class="id" title="var">x</span> <span class="id" title="var">n</span> :<br/> + <a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.L"><span class="id" title="variable">L</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#8663a77d1d910826e10ba42d1e8d2a02"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#8663a77d1d910826e10ba42d1e8d2a02"><span class="id" title="notation">nat</span></a> <a class="idref" href="mathcomp.field.separable.html#n"><span class="id" title="variable">n</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> 1 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation"><</span></a> <a class="idref" href="mathcomp.field.separable.html#n"><span class="id" title="variable">n</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.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation"><<</span></a><a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">;</span></a> <a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#fb22424322c3d7eb9b837dfca65ce21e"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.field.separable.html#n"><span class="id" title="variable">n</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">>></span></a>%<span class="id" title="var">VS</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>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="purely_inseparable_element"><span class="id" title="definition">purely_inseparable_element</span></a> <span class="id" title="var">U</span> <span class="id" title="var">x</span> :=<br/> + <a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#fb22424322c3d7eb9b837dfca65ce21e"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#ex_minn"><span class="id" title="definition">ex_minn</span></a> (<a class="idref" href="mathcomp.field.separable.html#separable_exponent"><span class="id" title="lemma">separable_exponent</span></a> <a class="idref" href="mathcomp.field.falgebra.html#a5d136b64fbd8856d9b682844c957cd8"><span class="id" title="notation"><<</span></a><a class="idref" href="mathcomp.field.separable.html#U"><span class="id" title="variable">U</span></a><a class="idref" href="mathcomp.field.falgebra.html#a5d136b64fbd8856d9b682844c957cd8"><span class="id" title="notation">>></span></a> <a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.separable.html#U"><span class="id" title="variable">U</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="purely_inseparable_elementP"><span class="id" title="lemma">purely_inseparable_elementP</span></a> {<span class="id" title="var">K</span> <span class="id" title="var">x</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.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">n</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#28b18e493f7cb0bd8447607bdc385ff8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">char</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.L"><span class="id" title="variable">L</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b8d1051ec5bf038cb2a33edc541359f8"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#8663a77d1d910826e10ba42d1e8d2a02"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#8663a77d1d910826e10ba42d1e8d2a02"><span class="id" title="notation">nat</span></a> <a class="idref" href="mathcomp.field.separable.html#n"><span class="id" title="variable">n</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.field.separable.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#fb22424322c3d7eb9b837dfca65ce21e"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.field.separable.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#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.field.separable.html#K"><span class="id" title="variable">K</span></a>)<br/> + (<a class="idref" href="mathcomp.field.separable.html#purely_inseparable_element"><span class="id" title="definition">purely_inseparable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="separable_inseparable_element"><span class="id" title="lemma">separable_inseparable_element</span></a> <span class="id" title="var">K</span> <span class="id" title="var">x</span> :<br/> + <a class="idref" href="mathcomp.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.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.Datatypes.html#49ac24efa716d8b0ee8943bc1d1769a9"><span class="id" title="notation">&&</span></a> <a class="idref" href="mathcomp.field.separable.html#purely_inseparable_element"><span class="id" title="definition">purely_inseparable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.separable.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#1c39bf18749e5cc609e83c0a0ba5a372"><span class="id" title="notation">)</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="base_inseparable"><span class="id" title="lemma">base_inseparable</span></a> <span class="id" title="var">K</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.separable.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.field.separable.html#purely_inseparable_element"><span class="id" title="definition">purely_inseparable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="sub_inseparable"><span class="id" title="lemma">sub_inseparable</span></a> <span class="id" title="var">K</span> <span class="id" title="var">E</span> <span class="id" title="var">x</span> :<br/> + (<a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.algebra.vector.html#755d11a7d5629bce3486e7cbadc915e7"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</span></a>)%<span class="id" title="var">VS</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> <a class="idref" href="mathcomp.field.separable.html#purely_inseparable_element"><span class="id" title="definition">purely_inseparable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.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#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.field.separable.html#purely_inseparable_element"><span class="id" title="definition">purely_inseparable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</span></a> <a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="Separable.PrimitiveElementTheorem"><span class="id" title="section">PrimitiveElementTheorem</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variables</span> (<a name="Separable.PrimitiveElementTheorem.K"><span class="id" title="variable">K</span></a> : <a class="idref" href="mathcomp.field.fieldext.html#da0a594fae595c8172b1a3e2dd69d19d"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.field.fieldext.html#da0a594fae595c8172b1a3e2dd69d19d"><span class="id" title="notation">subfield</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.L"><span class="id" title="variable">L</span></a><a class="idref" href="mathcomp.field.fieldext.html#da0a594fae595c8172b1a3e2dd69d19d"><span class="id" title="notation">}</span></a>) (<a name="Separable.PrimitiveElementTheorem.x"><span class="id" title="variable">x</span></a> <a name="Separable.PrimitiveElementTheorem.y"><span class="id" title="variable">y</span></a> : <a class="idref" href="mathcomp.field.separable.html#Separable.L"><span class="id" title="variable">L</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Section</span> <a name="Separable.PrimitiveElementTheorem.FiniteCase"><span class="id" title="section">FiniteCase</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Variable</span> <a name="Separable.PrimitiveElementTheorem.FiniteCase.N"><span class="id" title="variable">N</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Let</span> <a name="Separable.PrimitiveElementTheorem.FiniteCase.K_is_large"><span class="id" title="variable">K_is_large</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">s</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><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> <a class="idref" href="mathcomp.ssreflect.seq.html#uniq"><span class="id" title="definition">uniq</span></a> <a class="idref" href="mathcomp.field.separable.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#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#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">subset</span></a> <a class="idref" href="mathcomp.field.separable.html#s"><span class="id" title="variable">s</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.PrimitiveElementTheorem.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#53295d8f18390300c5a24f66e0bcda98"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.PrimitiveElementTheorem.FiniteCase.N"><span class="id" title="variable">N</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#989c98e7ddd65d5bf37c334ff2076de8"><span class="id" title="notation"><</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.field.separable.html#s"><span class="id" title="variable">s</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#962a3cb7af009aedac7986e261646bd1"><span class="id" title="notation">]</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Let</span> <a name="Separable.PrimitiveElementTheorem.FiniteCase.cyclic_or_large"><span class="id" title="variable">cyclic_or_large</span></a> (<span class="id" title="var">z</span> : <a class="idref" href="mathcomp.field.separable.html#Separable.L"><span class="id" title="variable">L</span></a>) : <a class="idref" href="mathcomp.field.separable.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#b1eeadc2feabc7422252baa895418c7b"><span class="id" title="notation">!=</span></a> 0 <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.field.separable.html#Separable.PrimitiveElementTheorem.FiniteCase.K_is_large"><span class="id" title="variable">K_is_large</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#7a45dffb109c3069e5c675be68643e60"><span class="id" title="notation">∨</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">a</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.field.separable.html#z"><span class="id" title="variable">z</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#fb22424322c3d7eb9b837dfca65ce21e"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.field.separable.html#a"><span class="id" title="variable">a</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#361454269931ea8643f7b402f2ab7222"><span class="id" title="notation">.+1</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="finite_PET"><span class="id" title="lemma">finite_PET</span></a> : <a class="idref" href="mathcomp.field.separable.html#Separable.PrimitiveElementTheorem.FiniteCase.K_is_large"><span class="id" title="variable">K_is_large</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#7a45dffb109c3069e5c675be68643e60"><span class="id" title="notation">∨</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">z</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a> (<a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation"><<</span></a> <a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation"><<</span></a><a class="idref" href="mathcomp.field.separable.html#Separable.PrimitiveElementTheorem.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">;</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.PrimitiveElementTheorem.y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">>>;</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.PrimitiveElementTheorem.x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><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.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation"><<</span></a><a class="idref" href="mathcomp.field.separable.html#Separable.PrimitiveElementTheorem.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">;</span></a> <a class="idref" href="mathcomp.field.separable.html#z"><span class="id" title="variable">z</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">>></span></a>)%<span class="id" title="var">VS</span>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.separable.html#Separable.PrimitiveElementTheorem.FiniteCase"><span class="id" title="section">FiniteCase</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Hypothesis</span> <a name="Separable.PrimitiveElementTheorem.sepKy"><span class="id" title="variable">sepKy</span></a> : <a class="idref" href="mathcomp.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.PrimitiveElementTheorem.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.PrimitiveElementTheorem.y"><span class="id" title="variable">y</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="Primitive_Element_Theorem"><span class="id" title="lemma">Primitive_Element_Theorem</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">∃</span></a> <span class="id" title="var">z</span><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#84eb6d2849dbf3581b1c0c05add5f2d8"><span class="id" title="notation">,</span></a> (<a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation"><<</span></a> <a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation"><<</span></a><a class="idref" href="mathcomp.field.separable.html#Separable.PrimitiveElementTheorem.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">;</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.PrimitiveElementTheorem.y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">>>;</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.PrimitiveElementTheorem.x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><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.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation"><<</span></a><a class="idref" href="mathcomp.field.separable.html#Separable.PrimitiveElementTheorem.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">;</span></a> <a class="idref" href="mathcomp.field.separable.html#z"><span class="id" title="variable">z</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">>></span></a>)%<span class="id" title="var">VS</span>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="adjoin_separable"><span class="id" title="lemma">adjoin_separable</span></a> : <a class="idref" href="mathcomp.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation"><<</span></a><a class="idref" href="mathcomp.field.separable.html#Separable.PrimitiveElementTheorem.K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">;</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.PrimitiveElementTheorem.y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">>></span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.PrimitiveElementTheorem.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#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.PrimitiveElementTheorem.K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.PrimitiveElementTheorem.x"><span class="id" title="variable">x</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.separable.html#Separable.PrimitiveElementTheorem"><span class="id" title="section">PrimitiveElementTheorem</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="strong_Primitive_Element_Theorem"><span class="id" title="lemma">strong_Primitive_Element_Theorem</span></a> <span class="id" title="var">K</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> :<br/> + <a class="idref" href="mathcomp.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation"><<</span></a><a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">;</span></a> <a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">>></span></a> <a class="idref" href="mathcomp.field.separable.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#fe60c20831f772c0c3c288abf68cc42a"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">z</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#fe60c20831f772c0c3c288abf68cc42a"><span class="id" title="notation">:</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.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#fe60c20831f772c0c3c288abf68cc42a"><span class="id" title="notation">,</span></a> (<a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation"><<</span></a> <a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation"><<</span></a><a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">;</span></a> <a class="idref" href="mathcomp.field.separable.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">>>;</span></a> <a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><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.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation"><<</span></a><a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">;</span></a> <a class="idref" href="mathcomp.field.separable.html#z"><span class="id" title="variable">z</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">>></span></a>)%<span class="id" title="var">VS</span><br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#fe60c20831f772c0c3c288abf68cc42a"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.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#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#y"><span class="id" title="variable">y</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="separable"><span class="id" title="definition">separable</span></a> <span class="id" title="var">U</span> <span class="id" title="var">W</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a> :=<br/> + <a class="idref" href="mathcomp.ssreflect.seq.html#all"><span class="id" title="definition">all</span></a> (<a class="idref" href="mathcomp.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#U"><span class="id" title="variable">U</span></a>) (<a class="idref" href="mathcomp.algebra.vector.html#vbasis"><span class="id" title="definition">vbasis</span></a> <a class="idref" href="mathcomp.field.separable.html#W"><span class="id" title="variable">W</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="purely_inseparable"><span class="id" title="definition">purely_inseparable</span></a> <span class="id" title="var">U</span> <span class="id" title="var">W</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a> :=<br/> + <a class="idref" href="mathcomp.ssreflect.seq.html#all"><span class="id" title="definition">all</span></a> (<a class="idref" href="mathcomp.field.separable.html#purely_inseparable_element"><span class="id" title="definition">purely_inseparable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#U"><span class="id" title="variable">U</span></a>) (<a class="idref" href="mathcomp.algebra.vector.html#vbasis"><span class="id" title="definition">vbasis</span></a> <a class="idref" href="mathcomp.field.separable.html#W"><span class="id" title="variable">W</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="separable_add"><span class="id" title="lemma">separable_add</span></a> <span class="id" title="var">K</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> :<br/> + <a class="idref" href="mathcomp.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.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#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> (<a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#ae4d81913e6239182a9ac7467ffde8cd"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.field.separable.html#y"><span class="id" title="variable">y</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="separable_sum"><span class="id" title="lemma">separable_sum</span></a> <span class="id" title="var">I</span> <span class="id" title="var">r</span> (<span class="id" title="var">P</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.field.separable.html#I"><span class="id" title="variable">I</span></a>) (<span class="id" title="var">v_</span> : <a class="idref" href="mathcomp.field.separable.html#I"><span class="id" title="variable">I</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.field.separable.html#Separable.L"><span class="id" title="variable">L</span></a>) <span class="id" title="var">K</span> :<br/> + <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><span class="id" title="keyword">∀</span> <span class="id" title="var">i</span>, <a class="idref" href="mathcomp.field.separable.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.field.separable.html#i"><span class="id" title="variable">i</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.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> (<a class="idref" href="mathcomp.field.separable.html#v_"><span class="id" title="variable">v_</span></a> <a class="idref" href="mathcomp.field.separable.html#i"><span class="id" title="variable">i</span></a>)<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#cbc2f2ab11c1c376b5c4511d28b14d74"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#cbc2f2ab11c1c376b5c4511d28b14d74"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#cbc2f2ab11c1c376b5c4511d28b14d74"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.algebra.ssralg.html#cbc2f2ab11c1c376b5c4511d28b14d74"><span class="id" title="notation"><-</span></a> <a class="idref" href="mathcomp.field.separable.html#r"><span class="id" title="variable">r</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#cbc2f2ab11c1c376b5c4511d28b14d74"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.field.separable.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.field.separable.html#i"><span class="id" title="variable">i</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#cbc2f2ab11c1c376b5c4511d28b14d74"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.field.separable.html#v_"><span class="id" title="variable">v_</span></a> <a class="idref" href="mathcomp.field.separable.html#i"><span class="id" title="variable">i</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="inseparable_add"><span class="id" title="lemma">inseparable_add</span></a> <span class="id" title="var">K</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> :<br/> + <a class="idref" href="mathcomp.field.separable.html#purely_inseparable_element"><span class="id" title="definition">purely_inseparable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.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#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.separable.html#purely_inseparable_element"><span class="id" title="definition">purely_inseparable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.field.separable.html#purely_inseparable_element"><span class="id" title="definition">purely_inseparable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> (<a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#ae4d81913e6239182a9ac7467ffde8cd"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.field.separable.html#y"><span class="id" title="variable">y</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="inseparable_sum"><span class="id" title="lemma">inseparable_sum</span></a> <span class="id" title="var">I</span> <span class="id" title="var">r</span> (<span class="id" title="var">P</span> : <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#pred"><span class="id" title="definition">pred</span></a> <a class="idref" href="mathcomp.field.separable.html#I"><span class="id" title="variable">I</span></a>) (<span class="id" title="var">v_</span> : <a class="idref" href="mathcomp.field.separable.html#I"><span class="id" title="variable">I</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.field.separable.html#Separable.L"><span class="id" title="variable">L</span></a>) <span class="id" title="var">K</span> :<br/> + <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><span class="id" title="keyword">∀</span> <span class="id" title="var">i</span>, <a class="idref" href="mathcomp.field.separable.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.field.separable.html#i"><span class="id" title="variable">i</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.field.separable.html#purely_inseparable_element"><span class="id" title="definition">purely_inseparable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> (<a class="idref" href="mathcomp.field.separable.html#v_"><span class="id" title="variable">v_</span></a> <a class="idref" href="mathcomp.field.separable.html#i"><span class="id" title="variable">i</span></a>)<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a><br/> + <a class="idref" href="mathcomp.field.separable.html#purely_inseparable_element"><span class="id" title="definition">purely_inseparable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> (<a class="idref" href="mathcomp.algebra.ssralg.html#cbc2f2ab11c1c376b5c4511d28b14d74"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#cbc2f2ab11c1c376b5c4511d28b14d74"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#cbc2f2ab11c1c376b5c4511d28b14d74"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.algebra.ssralg.html#cbc2f2ab11c1c376b5c4511d28b14d74"><span class="id" title="notation"><-</span></a> <a class="idref" href="mathcomp.field.separable.html#r"><span class="id" title="variable">r</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#cbc2f2ab11c1c376b5c4511d28b14d74"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.field.separable.html#P"><span class="id" title="variable">P</span></a> <a class="idref" href="mathcomp.field.separable.html#i"><span class="id" title="variable">i</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#cbc2f2ab11c1c376b5c4511d28b14d74"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.field.separable.html#v_"><span class="id" title="variable">v_</span></a> <a class="idref" href="mathcomp.field.separable.html#i"><span class="id" title="variable">i</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="separableP"><span class="id" title="lemma">separableP</span></a> {<span class="id" title="var">K</span> <span class="id" title="var">E</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> (<span class="id" title="keyword">∀</span> <span class="id" title="var">y</span>, <a class="idref" href="mathcomp.field.separable.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</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.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#y"><span class="id" title="variable">y</span></a>) (<a class="idref" href="mathcomp.field.separable.html#separable"><span class="id" title="definition">separable</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="purely_inseparableP"><span class="id" title="lemma">purely_inseparableP</span></a> {<span class="id" title="var">K</span> <span class="id" title="var">E</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> (<span class="id" title="keyword">∀</span> <span class="id" title="var">y</span>, <a class="idref" href="mathcomp.field.separable.html#y"><span class="id" title="variable">y</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</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.field.separable.html#purely_inseparable_element"><span class="id" title="definition">purely_inseparable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#y"><span class="id" title="variable">y</span></a>)<br/> + (<a class="idref" href="mathcomp.field.separable.html#purely_inseparable"><span class="id" title="definition">purely_inseparable</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="adjoin_separable_eq"><span class="id" title="lemma">adjoin_separable_eq</span></a> <span class="id" title="var">K</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.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.field.separable.html#separable"><span class="id" title="definition">separable</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation"><<</span></a><a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">;</span></a> <a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">>></span></a>%<span class="id" title="var">VS</span>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="separable_inseparable_decomposition"><span class="id" title="lemma">separable_inseparable_decomposition</span></a> <span class="id" title="var">E</span> <span class="id" title="var">K</span> :<br/> + <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#f5350ad671d3ce0e1e463e298917cf6e"><span class="id" title="notation">{</span></a><span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#f5350ad671d3ce0e1e463e298917cf6e"><span class="id" title="notation">|</span></a> <a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssrbool.html#46c9e8232fa09401e24f1934bb65029f"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</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.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.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.Specif.html#f5350ad671d3ce0e1e463e298917cf6e"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.field.separable.html#purely_inseparable"><span class="id" title="definition">purely_inseparable</span></a> <a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation"><<</span></a><a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">;</span></a> <a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">>></span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</span></a><a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Specif.html#f5350ad671d3ce0e1e463e298917cf6e"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Definition</span> <a name="separable_generator"><span class="id" title="definition">separable_generator</span></a> <span class="id" title="var">K</span> <span class="id" title="var">E</span> : <a class="idref" href="mathcomp.field.separable.html#Separable.L"><span class="id" title="variable">L</span></a> :=<br/> + <a class="idref" href="mathcomp.ssreflect.eqtype.html#s2val"><span class="id" title="definition">s2val</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.ssr.ssreflect.html#locked"><span class="id" title="definition">locked</span></a> (<a class="idref" href="mathcomp.field.separable.html#separable_inseparable_decomposition"><span class="id" title="lemma">separable_inseparable_decomposition</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a>)).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="separable_generator_mem"><span class="id" title="lemma">separable_generator_mem</span></a> <span class="id" title="var">E</span> <span class="id" title="var">K</span> : <a class="idref" href="mathcomp.field.separable.html#separable_generator"><span class="id" title="definition">separable_generator</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</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.field.separable.html#E"><span class="id" title="variable">E</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="separable_generatorP"><span class="id" title="lemma">separable_generatorP</span></a> <span class="id" title="var">E</span> <span class="id" title="var">K</span> : <a class="idref" href="mathcomp.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> (<a class="idref" href="mathcomp.field.separable.html#separable_generator"><span class="id" title="definition">separable_generator</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</span></a>).<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="separable_generator_maximal"><span class="id" title="lemma">separable_generator_maximal</span></a> <span class="id" title="var">E</span> <span class="id" title="var">K</span> :<br/> + <a class="idref" href="mathcomp.field.separable.html#purely_inseparable"><span class="id" title="definition">purely_inseparable</span></a> <a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation"><<</span></a><a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">;</span></a> <a class="idref" href="mathcomp.field.separable.html#separable_generator"><span class="id" title="definition">separable_generator</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">>></span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="sub_adjoin_separable_generator"><span class="id" title="lemma">sub_adjoin_separable_generator</span></a> <span class="id" title="var">E</span> <span class="id" title="var">K</span> :<br/> + <a class="idref" href="mathcomp.field.separable.html#separable"><span class="id" title="definition">separable</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</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.field.separable.html#E"><span class="id" title="variable">E</span></a> <a class="idref" href="mathcomp.algebra.vector.html#755d11a7d5629bce3486e7cbadc915e7"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation"><<</span></a><a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">;</span></a> <a class="idref" href="mathcomp.field.separable.html#separable_generator"><span class="id" title="definition">separable_generator</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">>></span></a>)%<span class="id" title="var">VS</span>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="eq_adjoin_separable_generator"><span class="id" title="lemma">eq_adjoin_separable_generator</span></a> <span class="id" title="var">E</span> <span class="id" title="var">K</span> :<br/> + <a class="idref" href="mathcomp.field.separable.html#separable"><span class="id" title="definition">separable</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</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.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.algebra.vector.html#755d11a7d5629bce3486e7cbadc915e7"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</span></a>)%<span class="id" title="var">VS</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.field.separable.html#E"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation"><<</span></a><a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">;</span></a> <a class="idref" href="mathcomp.field.separable.html#separable_generator"><span class="id" title="definition">separable_generator</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</span></a><a class="idref" href="mathcomp.field.falgebra.html#8327f1e5c19a7e79cb67878854f30e5f"><span class="id" title="notation">>></span></a>%<span class="id" title="var">VS</span> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#8f9364556521ebb498093f28eea2240f"><span class="id" title="notation">:></span></a> <a class="idref" href="mathcomp.algebra.vector.html#ca0a177f6d6581a7f5199987cd7ee21c"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.vector.html#ca0a177f6d6581a7f5199987cd7ee21c"><span class="id" title="notation">vspace</span></a> <span class="id" title="var">_</span><a class="idref" href="mathcomp.algebra.vector.html#ca0a177f6d6581a7f5199987cd7ee21c"><span class="id" title="notation">}</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="separable_refl"><span class="id" title="lemma">separable_refl</span></a> <span class="id" title="var">K</span> : <a class="idref" href="mathcomp.field.separable.html#separable"><span class="id" title="definition">separable</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="separable_trans"><span class="id" title="lemma">separable_trans</span></a> <span class="id" title="var">M</span> <span class="id" title="var">K</span> <span class="id" title="var">E</span> : <a class="idref" href="mathcomp.field.separable.html#separable"><span class="id" title="definition">separable</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.separable.html#separable"><span class="id" title="definition">separable</span></a> <a class="idref" href="mathcomp.field.separable.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</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.field.separable.html#separable"><span class="id" title="definition">separable</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="separableS"><span class="id" title="lemma">separableS</span></a> <span class="id" title="var">K1</span> <span class="id" title="var">K2</span> <span class="id" title="var">E2</span> <span class="id" title="var">E1</span> : <br/> + (<a class="idref" href="mathcomp.field.separable.html#K1"><span class="id" title="variable">K1</span></a> <a class="idref" href="mathcomp.algebra.vector.html#755d11a7d5629bce3486e7cbadc915e7"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.field.separable.html#K2"><span class="id" title="variable">K2</span></a>)%<span class="id" title="var">VS</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> (<a class="idref" href="mathcomp.field.separable.html#E2"><span class="id" title="variable">E2</span></a> <a class="idref" href="mathcomp.algebra.vector.html#755d11a7d5629bce3486e7cbadc915e7"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.field.separable.html#E1"><span class="id" title="variable">E1</span></a>)%<span class="id" title="var">VS</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> <a class="idref" href="mathcomp.field.separable.html#separable"><span class="id" title="definition">separable</span></a> <a class="idref" href="mathcomp.field.separable.html#K1"><span class="id" title="variable">K1</span></a> <a class="idref" href="mathcomp.field.separable.html#E1"><span class="id" title="variable">E1</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.field.separable.html#separable"><span class="id" title="definition">separable</span></a> <a class="idref" href="mathcomp.field.separable.html#K2"><span class="id" title="variable">K2</span></a> <a class="idref" href="mathcomp.field.separable.html#E2"><span class="id" title="variable">E2</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="separableSl"><span class="id" title="lemma">separableSl</span></a> <span class="id" title="var">K</span> <span class="id" title="var">M</span> <span class="id" title="var">E</span> : (<a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.algebra.vector.html#755d11a7d5629bce3486e7cbadc915e7"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.field.separable.html#M"><span class="id" title="variable">M</span></a>)%<span class="id" title="var">VS</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> <a class="idref" href="mathcomp.field.separable.html#separable"><span class="id" title="definition">separable</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</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.field.separable.html#separable"><span class="id" title="definition">separable</span></a> <a class="idref" href="mathcomp.field.separable.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="separableSr"><span class="id" title="lemma">separableSr</span></a> <span class="id" title="var">K</span> <span class="id" title="var">M</span> <span class="id" title="var">E</span> : (<a class="idref" href="mathcomp.field.separable.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.algebra.vector.html#755d11a7d5629bce3486e7cbadc915e7"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</span></a>)%<span class="id" title="var">VS</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> <a class="idref" href="mathcomp.field.separable.html#separable"><span class="id" title="definition">separable</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</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.field.separable.html#separable"><span class="id" title="definition">separable</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#M"><span class="id" title="variable">M</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="separable_Fadjoin_seq"><span class="id" title="lemma">separable_Fadjoin_seq</span></a> <span class="id" title="var">K</span> <span class="id" title="var">rs</span> :<br/> + <a class="idref" href="mathcomp.ssreflect.seq.html#all"><span class="id" title="definition">all</span></a> (<a class="idref" href="mathcomp.field.separable.html#separable_element"><span class="id" title="definition">separable_element</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a>) <a class="idref" href="mathcomp.field.separable.html#rs"><span class="id" title="variable">rs</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.field.separable.html#separable"><span class="id" title="definition">separable</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.falgebra.html#e4ccb61d3c0d4e7e716fb926f4a43f39"><span class="id" title="notation"><<</span></a><a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.falgebra.html#e4ccb61d3c0d4e7e716fb926f4a43f39"><span class="id" title="notation">&</span></a> <a class="idref" href="mathcomp.field.separable.html#rs"><span class="id" title="variable">rs</span></a><a class="idref" href="mathcomp.field.falgebra.html#e4ccb61d3c0d4e7e716fb926f4a43f39"><span class="id" title="notation">>></span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="purely_inseparable_refl"><span class="id" title="lemma">purely_inseparable_refl</span></a> <span class="id" title="var">K</span> : <a class="idref" href="mathcomp.field.separable.html#purely_inseparable"><span class="id" title="definition">purely_inseparable</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a>.<br/> + +<br/> +<span class="id" title="keyword">Lemma</span> <a name="purely_inseparable_trans"><span class="id" title="lemma">purely_inseparable_trans</span></a> <span class="id" title="var">M</span> <span class="id" title="var">K</span> <span class="id" title="var">E</span> :<br/> + <a class="idref" href="mathcomp.field.separable.html#purely_inseparable"><span class="id" title="definition">purely_inseparable</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="http://coq.inria.fr/distrib/8.8.0/stdlib//Coq.Init.Logic.html#d43e996736952df71ebeeae74d10a287"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.separable.html#purely_inseparable"><span class="id" title="definition">purely_inseparable</span></a> <a class="idref" href="mathcomp.field.separable.html#M"><span class="id" title="variable">M</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</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.field.separable.html#purely_inseparable"><span class="id" title="definition">purely_inseparable</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</span></a>.<br/> + +<br/> +<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.field.separable.html#Separable"><span class="id" title="section">Separable</span></a>.<br/> + +<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 |