diff options
Diffstat (limited to 'docs/htmldoc/mathcomp.field.separable.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.field.separable.html | 502 |
1 files changed, 0 insertions, 502 deletions
diff --git a/docs/htmldoc/mathcomp.field.separable.html b/docs/htmldoc/mathcomp.field.separable.html deleted file mode 100644 index 6ba91d2..0000000 --- a/docs/htmldoc/mathcomp.field.separable.html +++ /dev/null @@ -1,502 +0,0 @@ -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" -"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd"> -<html xmlns="http://www.w3.org/1999/xhtml"> -<head> -<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> -<link href="coqdoc.css" rel="stylesheet" type="text/css" /> -<title>mathcomp.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/> - -<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#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><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#c2ef4fdf7ae62c36654f85f0d2a6c874"><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#4edbe111d3afeccb0860281084ef5446"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#c385a484ee9d1b4e0615924561a9b75e"><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/V8.9.0/stdlib//Coq.Init.Logic.html#4bfb4f2d0721ba668e3a802ab1b745a1"><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#2d0cfb150261028f4ebd2ba355623dcc"><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#64fc6df2b95b79b2107dd5d7f2014b97"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#4bfb4f2d0721ba668e3a802ab1b745a1"><span class="id" title="notation">)</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#4bfb4f2d0721ba668e3a802ab1b745a1"><span class="id" title="notation">↔</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#4bfb4f2d0721ba668e3a802ab1b745a1"><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#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 1%<span class="id" title="var">N</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b3ebd0deddd84fd60e149cb5ef719351"><span class="id" title="notation">~~</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b3ebd0deddd84fd60e149cb5ef719351"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.separable.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#663140372ac3b275aae871b74b140513"><span class="id" title="notation">^+</span></a> 2 <a class="idref" href="mathcomp.algebra.polydiv.html#64fc6df2b95b79b2107dd5d7f2014b97"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b3ebd0deddd84fd60e149cb5ef719351"><span class="id" title="notation">)</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#4bfb4f2d0721ba668e3a802ab1b745a1"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#53e4c1e546d9b20e029d981f761726c2"><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#2d0cfb150261028f4ebd2ba355623dcc"><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#64fc6df2b95b79b2107dd5d7f2014b97"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#53e4c1e546d9b20e029d981f761726c2"><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#64fc6df2b95b79b2107dd5d7f2014b97"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> 1 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#00fe0eaf5e6949f0a31725357afa4bba"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#4edbe111d3afeccb0860281084ef5446"><span class="id" title="notation">^`</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#53e4c1e546d9b20e029d981f761726c2"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#2d0cfb150261028f4ebd2ba355623dcc"><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#64fc6df2b95b79b2107dd5d7f2014b97"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> 1 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#00fe0eaf5e6949f0a31725357afa4bba"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 1%<span class="id" title="var">N</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.separable.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#663140372ac3b275aae871b74b140513"><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#64fc6df2b95b79b2107dd5d7f2014b97"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#64fc6df2b95b79b2107dd5d7f2014b97"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> 1 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#00fe0eaf5e6949f0a31725357afa4bba"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#4edbe111d3afeccb0860281084ef5446"><span class="id" title="notation">^`</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.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#64fc6df2b95b79b2107dd5d7f2014b97"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#2d0cfb150261028f4ebd2ba355623dcc"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5a7d806905be2a0d04047156433535f1"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5a7d806905be2a0d04047156433535f1"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5a7d806905be2a0d04047156433535f1"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#5a7d806905be2a0d04047156433535f1"><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#952776a2e27e0a80427a97e8cd81c9aa"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.poly.html#dc2ed3a32abac1baa27cfc93ddc4e844"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#dc2ed3a32abac1baa27cfc93ddc4e844"><span class="id" title="notation">X</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#51dc792c356ca1a71a3094b50d6bb2fb"><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#8b14e41ab5fcce2460b8672da1456d67"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.poly.html#8b14e41ab5fcce2460b8672da1456d67"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">)</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.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/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><span class="id" title="notation">&&</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b3ebd0deddd84fd60e149cb5ef719351"><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#20f16c1d55d1e4ca9bb0e0513dd4b06a"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#20f16c1d55d1e4ca9bb0e0513dd4b06a"><span class="id" title="notation">prod_</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#20f16c1d55d1e4ca9bb0e0513dd4b06a"><span class="id" title="notation">(</span></a><span class="id" title="var">x</span> <a class="idref" href="mathcomp.algebra.ssralg.html#20f16c1d55d1e4ca9bb0e0513dd4b06a"><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#20f16c1d55d1e4ca9bb0e0513dd4b06a"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#20f16c1d55d1e4ca9bb0e0513dd4b06a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.poly.html#dc2ed3a32abac1baa27cfc93ddc4e844"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#dc2ed3a32abac1baa27cfc93ddc4e844"><span class="id" title="notation">X</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#51dc792c356ca1a71a3094b50d6bb2fb"><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#8b14e41ab5fcce2460b8672da1456d67"><span class="id" title="notation">%:</span></a><a class="idref" href="mathcomp.algebra.poly.html#8b14e41ab5fcce2460b8672da1456d67"><span class="id" title="notation">P</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#20f16c1d55d1e4ca9bb0e0513dd4b06a"><span class="id" title="notation">)</span></a>) <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.ssreflect.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#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.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#72a0c853cc9a32bb5fdc8a920a96e7c6"><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#4edbe111d3afeccb0860281084ef5446"><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#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">p</span> : <a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><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#c2ef4fdf7ae62c36654f85f0d2a6c874"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#d531732ed602c7af62b88c7cfce824e5"><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#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><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#c2ef4fdf7ae62c36654f85f0d2a6c874"><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#c385a484ee9d1b4e0615924561a9b75e"><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#38cc4a0ecff51aef123b4feb1fb0b274"><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/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <span class="id" title="var">q</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><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#38cc4a0ecff51aef123b4feb1fb0b274"><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#e4361ce58e4de0a4b9786d0011b61316"><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#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.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#38cc4a0ecff51aef123b4feb1fb0b274"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">r</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.field.separable.html#r"><span class="id" title="variable">r</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0<br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">&</span></a> <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#2d0cfb150261028f4ebd2ba355623dcc"><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#51dc792c356ca1a71a3094b50d6bb2fb"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b3ebd0deddd84fd60e149cb5ef719351"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#ba2b0e492d2b4675a0acf3ea92aabadd"><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#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><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#c2ef4fdf7ae62c36654f85f0d2a6c874"><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#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.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#38cc4a0ecff51aef123b4feb1fb0b274"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><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#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#1e6a438ff685c38fcd9034a94f271777"><span class="id" title="notation">=</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#1e6a438ff685c38fcd9034a94f271777"><span class="id" title="notation">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#pred0"><span class="id" title="definition">pred0</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <span class="id" title="var">n</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><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#e9001f602764f7896bb1eb34bf606a23"><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#51dc792c356ca1a71a3094b50d6bb2fb"><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/V8.9.0/stdlib//Coq.Init.Logic.html#ba2b0e492d2b4675a0acf3ea92aabadd"><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#95065d7eff417cb87497b35ad25bda41"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.vector.html#95065d7eff417cb87497b35ad25bda41"><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#95065d7eff417cb87497b35ad25bda41"><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#810f00798e9fd6a59691271bacabea40"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.field.fieldext.html#810f00798e9fd6a59691271bacabea40"><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#810f00798e9fd6a59691271bacabea40"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">D</span> : <a class="idref" href="mathcomp.algebra.vector.html#53a3ec8a4009300ec80babde5a7883ab"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.vector.html#53a3ec8a4009300ec80babde5a7883ab"><span class="id" title="notation">End</span></a><a class="idref" href="mathcomp.algebra.vector.html#53a3ec8a4009300ec80babde5a7883ab"><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#53a3ec8a4009300ec80babde5a7883ab"><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#95065d7eff417cb87497b35ad25bda41"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.vector.html#95065d7eff417cb87497b35ad25bda41"><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#95065d7eff417cb87497b35ad25bda41"><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#53a3ec8a4009300ec80babde5a7883ab"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.vector.html#53a3ec8a4009300ec80babde5a7883ab"><span class="id" title="notation">End</span></a><a class="idref" href="mathcomp.algebra.vector.html#53a3ec8a4009300ec80babde5a7883ab"><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#53a3ec8a4009300ec80babde5a7883ab"><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/V8.9.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#2d0cfb150261028f4ebd2ba355623dcc"><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#df45e8c2e8370fd4f0f7c4fdaf208180"><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#2d0cfb150261028f4ebd2ba355623dcc"><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#c7f78cf1f6a5e4f664654f7d671ca752"><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#2d0cfb150261028f4ebd2ba355623dcc"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><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#2d0cfb150261028f4ebd2ba355623dcc"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#2d0cfb150261028f4ebd2ba355623dcc"><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#c7f78cf1f6a5e4f664654f7d671ca752"><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#2d0cfb150261028f4ebd2ba355623dcc"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><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#2d0cfb150261028f4ebd2ba355623dcc"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#2d0cfb150261028f4ebd2ba355623dcc"><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#c7f78cf1f6a5e4f664654f7d671ca752"><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#2d0cfb150261028f4ebd2ba355623dcc"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b4f176550f5b849a7fbba2ee164934d3"><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#65f0b8f4dcd5cfd6280e7c777466601a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#810f00798e9fd6a59691271bacabea40"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.field.fieldext.html#810f00798e9fd6a59691271bacabea40"><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#810f00798e9fd6a59691271bacabea40"><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#53a3ec8a4009300ec80babde5a7883ab"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.vector.html#53a3ec8a4009300ec80babde5a7883ab"><span class="id" title="notation">End</span></a><a class="idref" href="mathcomp.algebra.vector.html#53a3ec8a4009300ec80babde5a7883ab"><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#53a3ec8a4009300ec80babde5a7883ab"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> 1%<span class="id" title="var">VS</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.DerivationAlgebra.E"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.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#663140372ac3b275aae871b74b140513"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#663140372ac3b275aae871b74b140513"><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#f953bf7095e0da1cb644443fd0e17d6d"><span class="id" title="notation">.-1</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#e9001f602764f7896bb1eb34bf606a23"><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#2d0cfb150261028f4ebd2ba355623dcc"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">is</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.DerivationAlgebra.E"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="mathcomp.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#e4361ce58e4de0a4b9786d0011b61316"><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#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><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#e4361ce58e4de0a4b9786d0011b61316"><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#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#c7f78cf1f6a5e4f664654f7d671ca752"><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#4edbe111d3afeccb0860281084ef5446"><span class="id" title="notation">^`</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><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#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><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#810f00798e9fd6a59691271bacabea40"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.field.fieldext.html#810f00798e9fd6a59691271bacabea40"><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#810f00798e9fd6a59691271bacabea40"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <span class="id" title="var">f</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">[/\</span></a> <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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">is</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.K"><span class="id" title="variable">K</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.poly.html#4edbe111d3afeccb0860281084ef5446"><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#4edbe111d3afeccb0860281084ef5446"><span class="id" title="notation">)^`</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>.<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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">p</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.field.separable.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><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#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">&</span></a> <br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">g</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.field.separable.html#g"><span class="id" title="variable">g</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">is</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><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/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#011952147f33cb889a964c228c4ebadd"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.poly.html#011952147f33cb889a964c228c4ebadd"><span class="id" title="notation">Po</span></a> <a class="idref" href="mathcomp.algebra.poly.html#e809881bcf0cc80f806c17b9ef433187"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.poly.html#e809881bcf0cc80f806c17b9ef433187"><span class="id" title="notation">X</span></a><a class="idref" href="mathcomp.algebra.poly.html#e809881bcf0cc80f806c17b9ef433187"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b3ebd0deddd84fd60e149cb5ef719351"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#a60537c464e134477471443dd91ae651"><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#4edbe111d3afeccb0860281084ef5446"><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#4edbe111d3afeccb0860281084ef5446"><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#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#8d0566c961139ec21811f52ef0c317db"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><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#e4361ce58e4de0a4b9786d0011b61316"><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#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#69c431a9c94f6f30a655bd7ddb59037b"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.poly.html#4edbe111d3afeccb0860281084ef5446"><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#4edbe111d3afeccb0860281084ef5446"><span class="id" title="notation">)^`</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><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#e4361ce58e4de0a4b9786d0011b61316"><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#53a3ec8a4009300ec80babde5a7883ab"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.vector.html#53a3ec8a4009300ec80babde5a7883ab"><span class="id" title="notation">End</span></a><a class="idref" href="mathcomp.algebra.vector.html#53a3ec8a4009300ec80babde5a7883ab"><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#53a3ec8a4009300ec80babde5a7883ab"><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#8d0566c961139ec21811f52ef0c317db"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><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#e4361ce58e4de0a4b9786d0011b61316"><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#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#69c431a9c94f6f30a655bd7ddb59037b"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.poly.html#4edbe111d3afeccb0860281084ef5446"><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#4edbe111d3afeccb0860281084ef5446"><span class="id" title="notation">)^`</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><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#e4361ce58e4de0a4b9786d0011b61316"><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#e4361ce58e4de0a4b9786d0011b61316"><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#e4361ce58e4de0a4b9786d0011b61316"><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#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#c7f78cf1f6a5e4f664654f7d671ca752"><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#4edbe111d3afeccb0860281084ef5446"><span class="id" title="notation">^`</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><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#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><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#53a3ec8a4009300ec80babde5a7883ab"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.vector.html#53a3ec8a4009300ec80babde5a7883ab"><span class="id" title="notation">End</span></a><a class="idref" href="mathcomp.algebra.vector.html#53a3ec8a4009300ec80babde5a7883ab"><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#53a3ec8a4009300ec80babde5a7883ab"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.separable.html#Separable.SeparableElement.K"><span class="id" title="variable">K</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><span class="id" title="notation">is</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#f6c65697fefaf4504de1d4d641cd4409"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#e4361ce58e4de0a4b9786d0011b61316"><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#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><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#e4361ce58e4de0a4b9786d0011b61316"><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#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#c7f78cf1f6a5e4f664654f7d671ca752"><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#4edbe111d3afeccb0860281084ef5446"><span class="id" title="notation">^`</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><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#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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/V8.9.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#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#65f0b8f4dcd5cfd6280e7c777466601a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.field.falgebra.html#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><span class="id" title="notation">>></span></a> <a class="idref" href="mathcomp.algebra.vector.html#65f0b8f4dcd5cfd6280e7c777466601a"><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#65f0b8f4dcd5cfd6280e7c777466601a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.falgebra.html#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><span class="id" title="notation">>></span></a>%<span class="id" title="var">VS</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <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/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <span class="id" title="var">n</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><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#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#31aa0776b2fdb88da5b5ba70544862a1"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#31aa0776b2fdb88da5b5ba70544862a1"><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/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><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#663140372ac3b275aae871b74b140513"><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#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><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#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#1e6a438ff685c38fcd9034a94f271777"><span class="id" title="notation">=</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#1e6a438ff685c38fcd9034a94f271777"><span class="id" title="notation">i</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#pred0"><span class="id" title="definition">pred0</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><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#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">]</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.falgebra.html#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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#663140372ac3b275aae871b74b140513"><span class="id" title="notation">^+</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#663140372ac3b275aae871b74b140513"><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#81fd94e251a61ee523cdd7855774ae7c"><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#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#663140372ac3b275aae871b74b140513"><span class="id" title="notation">)</span></a><a class="idref" href="mathcomp.field.falgebra.html#faad1af6363310d507c72eed3dbfbc17"><span class="id" title="notation">>></span></a>%<span class="id" title="var">VS</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>.<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#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><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#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#31aa0776b2fdb88da5b5ba70544862a1"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#31aa0776b2fdb88da5b5ba70544862a1"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> 1 <a class="idref" href="mathcomp.ssreflect.ssrnat.html#00fe0eaf5e6949f0a31725357afa4bba"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.falgebra.html#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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#663140372ac3b275aae871b74b140513"><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#faad1af6363310d507c72eed3dbfbc17"><span class="id" title="notation">>></span></a>%<span class="id" title="var">VS</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a>.<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#663140372ac3b275aae871b74b140513"><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#3e666855bd966e1fc13cba166232bd7a"><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#3e666855bd966e1fc13cba166232bd7a"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#reflect"><span class="id" title="abbreviation">reflect</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">n</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0928aaf0450c3a4c5521d7d3da15b6d8"><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#0928aaf0450c3a4c5521d7d3da15b6d8"><span class="id" title="notation">]</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#31aa0776b2fdb88da5b5ba70544862a1"><span class="id" title="notation">.-</span></a><a class="idref" href="mathcomp.ssreflect.prime.html#31aa0776b2fdb88da5b5ba70544862a1"><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/V8.9.0/stdlib//Coq.Init.Logic.html#3df228c109f14f0423b4fccc967ee1ac"><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#663140372ac3b275aae871b74b140513"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.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/V8.9.0/stdlib//Coq.Init.Datatypes.html#9ddeac0ab66152bd1d64bedb507a795e"><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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.field.separable.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.separable.html#K"><span class="id" title="variable">K</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.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#65f0b8f4dcd5cfd6280e7c777466601a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#810f00798e9fd6a59691271bacabea40"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.field.fieldext.html#810f00798e9fd6a59691271bacabea40"><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#810f00798e9fd6a59691271bacabea40"><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/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <span class="id" title="var">s</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">[/\</span></a> <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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">{</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#ca592708f529c7c7ee5f3dbd6cf93463"><span class="id" title="notation">}</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><span class="id" title="notation">&</span></a> <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#00fe0eaf5e6949f0a31725357afa4bba"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#d7e433f5d2fe56f5b712860a9ff2a681"><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#c385a484ee9d1b4e0615924561a9b75e"><span class="id" title="notation">!=</span></a> 0 <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.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/V8.9.0/stdlib//Coq.Init.Logic.html#f031fe1957c4a4a8e217aa46af2b4e25"><span class="id" title="notation">∨</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <span class="id" title="var">a</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><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#663140372ac3b275aae871b74b140513"><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#bda89d73ec4a8f23ae92b565ffb5aaa6"><span class="id" title="notation">.+1</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> 1.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="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/V8.9.0/stdlib//Coq.Init.Logic.html#f031fe1957c4a4a8e217aa46af2b4e25"><span class="id" title="notation">∨</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <span class="id" title="var">z</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> (<a class="idref" href="mathcomp.field.falgebra.html#faad1af6363310d507c72eed3dbfbc17"><span class="id" title="notation"><<</span></a> <a class="idref" href="mathcomp.field.falgebra.html#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><span class="id" title="notation">>></span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.field.falgebra.html#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">∃</span></a> <span class="id" title="var">z</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#a883bdd010993579f99d60b3775bcf54"><span class="id" title="notation">,</span></a> (<a class="idref" href="mathcomp.field.falgebra.html#faad1af6363310d507c72eed3dbfbc17"><span class="id" title="notation"><<</span></a> <a class="idref" href="mathcomp.field.falgebra.html#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><span class="id" title="notation">>></span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.field.falgebra.html#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#59ba2b47d2814e66f8210a649ae6e6bc"><span class="id" title="notation">exists2</span></a> <span class="id" title="var">z</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#59ba2b47d2814e66f8210a649ae6e6bc"><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/V8.9.0/stdlib//Coq.Init.Logic.html#59ba2b47d2814e66f8210a649ae6e6bc"><span class="id" title="notation">,</span></a> (<a class="idref" href="mathcomp.field.falgebra.html#faad1af6363310d507c72eed3dbfbc17"><span class="id" title="notation"><<</span></a> <a class="idref" href="mathcomp.field.falgebra.html#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><span class="id" title="notation">>></span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.field.falgebra.html#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><span class="id" title="notation">>></span></a>)%<span class="id" title="var">VS</span><br/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#59ba2b47d2814e66f8210a649ae6e6bc"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.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/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#c7f78cf1f6a5e4f664654f7d671ca752"><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/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#0e493beb85c9c1b3ab2241ceeaa98b08"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0e493beb85c9c1b3ab2241ceeaa98b08"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0e493beb85c9c1b3ab2241ceeaa98b08"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.algebra.ssralg.html#0e493beb85c9c1b3ab2241ceeaa98b08"><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#0e493beb85c9c1b3ab2241ceeaa98b08"><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#0e493beb85c9c1b3ab2241ceeaa98b08"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#c7f78cf1f6a5e4f664654f7d671ca752"><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/V8.9.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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#0e493beb85c9c1b3ab2241ceeaa98b08"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0e493beb85c9c1b3ab2241ceeaa98b08"><span class="id" title="notation">sum_</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#0e493beb85c9c1b3ab2241ceeaa98b08"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.algebra.ssralg.html#0e493beb85c9c1b3ab2241ceeaa98b08"><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#0e493beb85c9c1b3ab2241ceeaa98b08"><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#0e493beb85c9c1b3ab2241ceeaa98b08"><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/V8.9.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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.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/V8.9.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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.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/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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/V8.9.0/stdlib//Coq.Init.Specif.html#c0bbd202248f4def7aaf0c316cf2c29e"><span class="id" title="notation">{</span></a><span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#c0bbd202248f4def7aaf0c316cf2c29e"><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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.field.separable.html#E"><span class="id" title="variable">E</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#ba2b0e492d2b4675a0acf3ea92aabadd"><span class="id" title="notation">∧</span></a> <a class="idref" href="mathcomp.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/V8.9.0/stdlib//Coq.Init.Specif.html#c0bbd202248f4def7aaf0c316cf2c29e"><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#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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/V8.9.0/stdlib//Coq.Init.Specif.html#c0bbd202248f4def7aaf0c316cf2c29e"><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/V8.9.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/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">\</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrbool.html#b09457274bcb94927e289b8a9e9cd3f7"><span class="id" title="notation">in</span></a> <a class="idref" href="mathcomp.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#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#65f0b8f4dcd5cfd6280e7c777466601a"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.field.falgebra.html#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#65f0b8f4dcd5cfd6280e7c777466601a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.field.falgebra.html#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><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#faad1af6363310d507c72eed3dbfbc17"><span class="id" title="notation">>></span></a>%<span class="id" title="var">VS</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#b8b2ebc8e1a8b9aa935c0702efb5dccf"><span class="id" title="notation">:></span></a> <a class="idref" href="mathcomp.algebra.vector.html#95065d7eff417cb87497b35ad25bda41"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.vector.html#95065d7eff417cb87497b35ad25bda41"><span class="id" title="notation">vspace</span></a> <span class="id" title="var">_</span><a class="idref" href="mathcomp.algebra.vector.html#95065d7eff417cb87497b35ad25bda41"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#65f0b8f4dcd5cfd6280e7c777466601a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#65f0b8f4dcd5cfd6280e7c777466601a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#65f0b8f4dcd5cfd6280e7c777466601a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#65f0b8f4dcd5cfd6280e7c777466601a"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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#371fc5178e74e35fccdd110881a97487"><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#371fc5178e74e35fccdd110881a97487"><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#371fc5178e74e35fccdd110881a97487"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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/V8.9.0/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><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 |