diff options
Diffstat (limited to 'docs/htmldoc/mathcomp.algebra.polyXY.html')
| -rw-r--r-- | docs/htmldoc/mathcomp.algebra.polyXY.html | 296 |
1 files changed, 0 insertions, 296 deletions
diff --git a/docs/htmldoc/mathcomp.algebra.polyXY.html b/docs/htmldoc/mathcomp.algebra.polyXY.html deleted file mode 100644 index 53a0eb8..0000000 --- a/docs/htmldoc/mathcomp.algebra.polyXY.html +++ /dev/null @@ -1,296 +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.algebra.polyXY</title> -</head> - -<body> - -<div id="page"> - -<div id="header"> -</div> - -<div id="main"> - -<h1 class="libtitle">Library mathcomp.algebra.polyXY</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 additional primitives and theory for bivariate - polynomials (polynomials of two variables), represented as polynomials - with (univariate) polynomial coefficients : - 'Y == the (generic) second variable (:= 'X%:P). - p^:P == the bivariate polynomial p['X], for p univariate. - := map_poly polyC p (this notation is defined in poly.v). - u. [x, y] == the bivariate polynomial u evaluated at 'X = x, 'Y = y. - := u. [x%:P]. [y]. - sizeY u == the size of u in 'Y (1 + the 'Y-degree of u, if u != 0). - := \max</i>(i < size u) size u`<i>i. - swapXY u == the bivariate polynomial u['Y, 'X], for u bivariate. - poly_XaY p == the bivariate polynomial p['X + 'Y], for p univariate. - := p^:P \Po ('X + 'Y). - poly_XmY p == the bivariate polynomial p['X * 'Y], for p univariate. - := P^:P \Po ('X * 'Y). - sub_annihilant p q == for univariate p, q != 0, a nonzero polynomial whose - roots include all the differences of roots of p and q, in - all field extensions (:= resultant (poly_XaY p) q^:P). - div_annihilant p q == for polynomials p != 0, q with q. [0] != 0, a nonzero - polynomial whose roots include all the quotients of roots - of p by roots of q, in all field extensions - (:= resultant (poly_XmY p) q^:P). - The latter two "annhilants" provide uniform witnesses for an alternative - proof of the closure of the algebraicOver predicate (see mxpoly.v). The - fact that the annhilant does not depend on the particular choice of roots - of p and q is crucial for the proof of the Primitive Element Theorem (file - separable.v). -</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/> - -<br/> -<span class="id" title="keyword">Notation</span> <a name="8458d60dcb98967fb458fa915fbb9d8f"><span class="id" title="notation">"</span></a>'Y" := <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.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> : <span class="id" title="var">ring_scope</span>.<br/> -<span class="id" title="keyword">Notation</span> <a name="3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">"</span></a>p ^:P" := (<span class="id" title="var">p</span> <a class="idref" href="mathcomp.algebra.polyXY.html#11a706273cccd094dd42b3c7d6457ef8"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.poly.html#polyC"><span class="id" title="definition">polyC</span></a>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="var">format</span> "p ^:P") : <span class="id" title="var">ring_scope</span>.<br/> -<span class="id" title="keyword">Notation</span> <a name="75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">"</span></a>p .[ x , y ]" := (<span class="id" title="var">p</span><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">.[</span></a><span class="id" title="var">x</span><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.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">].[</span></a><span class="id" title="var">y</span><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a>)<br/> - (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 2, <span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>, <span class="id" title="var">format</span> "p .[ x , y ]") : <span class="id" title="var">ring_scope</span>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="PolyXY_Ring"><span class="id" title="section">PolyXY_Ring</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="PolyXY_Ring.R"><span class="id" title="variable">R</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Ring.Exports.ringType"><span class="id" title="abbreviation">ringType</span></a>.<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">u</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.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.algebra.polyXY.html#PolyXY_Ring.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>) (<span class="id" title="var">p</span> <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.algebra.polyXY.html#PolyXY_Ring.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>) (<span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Ring.R"><span class="id" title="variable">R</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Fact</span> <a name="swapXY_key"><span class="id" title="lemma">swapXY_key</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a>. <br/> -<span class="id" title="keyword">Definition</span> <a name="swapXY_def"><span class="id" title="definition">swapXY_def</span></a> <span class="id" title="var">u</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.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.algebra.polyXY.html#PolyXY_Ring.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> := <a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#11a706273cccd094dd42b3c7d6457ef8"><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.algebra.poly.html#polyC"><span class="id" title="definition">polyC</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#8458d60dcb98967fb458fa915fbb9d8f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#8458d60dcb98967fb458fa915fbb9d8f"><span class="id" title="notation">Y</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="swapXY"><span class="id" title="definition">swapXY</span></a> := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#locked_with"><span class="id" title="definition">locked_with</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY_key"><span class="id" title="lemma">swapXY_key</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY_def"><span class="id" title="definition">swapXY_def</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">swapXY_unlockable</span> := <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#84464b412faf5a30a7c5c6423d9b3956"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#84464b412faf5a30a7c5c6423d9b3956"><span class="id" title="notation">unlockable</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#84464b412faf5a30a7c5c6423d9b3956"><span class="id" title="notation">fun</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssreflect.html#84464b412faf5a30a7c5c6423d9b3956"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Definition</span> <a name="sizeY"><span class="id" title="definition">sizeY</span></a> <span class="id" title="var">u</span> : <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> := <a class="idref" href="mathcomp.ssreflect.bigop.html#3a447b0afd9ad8298064c27788129338"><span class="id" title="notation">\</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#3a447b0afd9ad8298064c27788129338"><span class="id" title="notation">max_</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#3a447b0afd9ad8298064c27788129338"><span class="id" title="notation">(</span></a><span class="id" title="var">i</span> <a class="idref" href="mathcomp.ssreflect.bigop.html#3a447b0afd9ad8298064c27788129338"><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.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#3a447b0afd9ad8298064c27788129338"><span class="id" title="notation">)</span></a> <a class="idref" href="mathcomp.ssreflect.bigop.html#3a447b0afd9ad8298064c27788129338"><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.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#82d810f9f90b79e8fe98d90a63070c32"><span class="id" title="notation">`</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#82d810f9f90b79e8fe98d90a63070c32"><span class="id" title="notation">_i</span></a><a class="idref" href="mathcomp.ssreflect.bigop.html#3a447b0afd9ad8298064c27788129338"><span class="id" title="notation">)</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="poly_XaY"><span class="id" title="definition">poly_XaY</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.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.algebra.polyXY.html#PolyXY_Ring.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> := <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">^:</span></a><a class="idref" href="mathcomp.algebra.poly.html#3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">P</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#011952147f33cb889a964c228c4ebadd"><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#c7f78cf1f6a5e4f664654f7d671ca752"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#8458d60dcb98967fb458fa915fbb9d8f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#8458d60dcb98967fb458fa915fbb9d8f"><span class="id" title="notation">Y</span></a><a class="idref" href="mathcomp.algebra.poly.html#011952147f33cb889a964c228c4ebadd"><span class="id" title="notation">)</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="poly_XmY"><span class="id" title="definition">poly_XmY</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.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.algebra.polyXY.html#PolyXY_Ring.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> := <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">^:</span></a><a class="idref" href="mathcomp.algebra.poly.html#3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">P</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#011952147f33cb889a964c228c4ebadd"><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#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#8458d60dcb98967fb458fa915fbb9d8f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#8458d60dcb98967fb458fa915fbb9d8f"><span class="id" title="notation">Y</span></a><a class="idref" href="mathcomp.algebra.poly.html#011952147f33cb889a964c228c4ebadd"><span class="id" title="notation">)</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="sub_annihilant"><span class="id" title="definition">sub_annihilant</span></a> <span class="id" title="var">p</span> <span class="id" title="var">q</span> := <a class="idref" href="mathcomp.algebra.mxpoly.html#resultant"><span class="id" title="definition">resultant</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#poly_XaY"><span class="id" title="definition">poly_XaY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.poly.html#3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">^:</span></a><a class="idref" href="mathcomp.algebra.poly.html#3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">P</span></a>.<br/> -<span class="id" title="keyword">Definition</span> <a name="div_annihilant"><span class="id" title="definition">div_annihilant</span></a> <span class="id" title="var">p</span> <span class="id" title="var">q</span> := <a class="idref" href="mathcomp.algebra.mxpoly.html#resultant"><span class="id" title="definition">resultant</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#poly_XmY"><span class="id" title="definition">poly_XmY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.poly.html#3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">^:</span></a><a class="idref" href="mathcomp.algebra.poly.html#3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">P</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="swapXY_polyC"><span class="id" title="lemma">swapXY_polyC</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</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="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.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">^:</span></a><a class="idref" href="mathcomp.algebra.poly.html#3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">P</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="swapXY_X"><span class="id" title="lemma">swapXY_X</span></a> : <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</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="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.polyXY.html#8458d60dcb98967fb458fa915fbb9d8f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#8458d60dcb98967fb458fa915fbb9d8f"><span class="id" title="notation">Y</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="swapXY_Y"><span class="id" title="lemma">swapXY_Y</span></a> : <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#8458d60dcb98967fb458fa915fbb9d8f"><span class="id" title="notation">'</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#8458d60dcb98967fb458fa915fbb9d8f"><span class="id" title="notation">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.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>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="swapXY_is_additive"><span class="id" title="lemma">swapXY_is_additive</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Additive.Exports.additive"><span class="id" title="abbreviation">additive</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a>.<br/> - <span class="id" title="keyword">Canonical</span> <span class="id" title="var">swapXY_addf</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Additive.Exports.Additive"><span class="id" title="abbreviation">Additive</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY_is_additive"><span class="id" title="lemma">swapXY_is_additive</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="coef_swapXY"><span class="id" title="lemma">coef_swapXY</span></a> <span class="id" title="var">u</span> <span class="id" title="var">i</span> <span class="id" title="var">j</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#82d810f9f90b79e8fe98d90a63070c32"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#82d810f9f90b79e8fe98d90a63070c32"><span class="id" title="notation">)`</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#82d810f9f90b79e8fe98d90a63070c32"><span class="id" title="notation">_i</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#82d810f9f90b79e8fe98d90a63070c32"><span class="id" title="notation">`</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#82d810f9f90b79e8fe98d90a63070c32"><span class="id" title="notation">_j</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.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#82d810f9f90b79e8fe98d90a63070c32"><span class="id" title="notation">`</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#82d810f9f90b79e8fe98d90a63070c32"><span class="id" title="notation">_j</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#82d810f9f90b79e8fe98d90a63070c32"><span class="id" title="notation">`</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#82d810f9f90b79e8fe98d90a63070c32"><span class="id" title="notation">_i</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="swapXYK"><span class="id" title="lemma">swapXYK</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#involutive"><span class="id" title="definition">involutive</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="swapXY_map_polyC"><span class="id" title="lemma">swapXY_map_polyC</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">^:</span></a><a class="idref" href="mathcomp.algebra.poly.html#3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">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.algebra.polyXY.html#p"><span class="id" title="variable">p</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>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="swapXY_eq0"><span class="id" title="lemma">swapXY_eq0</span></a> <span class="id" title="var">u</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</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.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</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>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="swapXY_is_multiplicative"><span class="id" title="lemma">swapXY_is_multiplicative</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.RMorphism.Exports.multiplicative"><span class="id" title="abbreviation">multiplicative</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">swapXY_rmorphism</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.RMorphism.Exports.AddRMorphism"><span class="id" title="abbreviation">AddRMorphism</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY_is_multiplicative"><span class="id" title="lemma">swapXY_is_multiplicative</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="swapXY_is_scalable"><span class="id" title="lemma">swapXY_is_scalable</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Linear.Exports.scalable_for"><span class="id" title="abbreviation">scalable_for</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.algebra.poly.html#polyC"><span class="id" title="definition">polyC</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#11ebad41b70994075d9152ef8d0a15b3"><span class="id" title="notation">\;</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#3609d85e23333c9e68741ad96b416eec"><span class="id" title="notation">*%</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#3609d85e23333c9e68741ad96b416eec"><span class="id" title="notation">R</span></a>) <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a>.<br/> - <span class="id" title="keyword">Canonical</span> <span class="id" title="var">swapXY_linear</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Linear.Exports.AddLinear"><span class="id" title="abbreviation">AddLinear</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY_is_scalable"><span class="id" title="lemma">swapXY_is_scalable</span></a>.<br/> -<span class="id" title="keyword">Canonical</span> <span class="id" title="var">swapXY_lrmorphism</span> := <a class="idref" href="mathcomp.algebra.ssralg.html#d17433407f88fd9a1e0740e2eddd6566"><span class="id" title="notation">[</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d17433407f88fd9a1e0740e2eddd6566"><span class="id" title="notation">lrmorphism</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#d17433407f88fd9a1e0740e2eddd6566"><span class="id" title="notation">of</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d17433407f88fd9a1e0740e2eddd6566"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="swapXY_comp_poly"><span class="id" title="lemma">swapXY_comp_poly</span></a> <span class="id" title="var">p</span> <span class="id" title="var">u</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">^:</span></a><a class="idref" href="mathcomp.algebra.poly.html#3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">P</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.polyXY.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#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a><a class="idref" href="mathcomp.algebra.poly.html#3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">^:</span></a><a class="idref" href="mathcomp.algebra.poly.html#3ccfd12ca6a7abb145c90e1788b68707"><span class="id" title="notation">P</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.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="max_size_coefXY"><span class="id" title="lemma">max_size_coefXY</span></a> <span class="id" title="var">u</span> <span class="id" title="var">i</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#82d810f9f90b79e8fe98d90a63070c32"><span class="id" title="notation">`</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#82d810f9f90b79e8fe98d90a63070c32"><span class="id" title="notation">_i</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#cb53cf0ee22c036a03b4a9281c68b5a3"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#sizeY"><span class="id" title="definition">sizeY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="max_size_lead_coefXY"><span class="id" title="lemma">max_size_lead_coefXY</span></a> <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.algebra.poly.html#lead_coef"><span class="id" title="definition">lead_coef</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a>) <a class="idref" href="mathcomp.ssreflect.ssrnat.html#cb53cf0ee22c036a03b4a9281c68b5a3"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#sizeY"><span class="id" title="definition">sizeY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="max_size_evalX"><span class="id" title="lemma">max_size_evalX</span></a> <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.algebra.polyXY.html#u"><span class="id" title="variable">u</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#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.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#cb53cf0ee22c036a03b4a9281c68b5a3"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#sizeY"><span class="id" title="definition">sizeY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#f953bf7095e0da1cb644443fd0e17d6d"><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.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.ssreflect.ssrnat.html#f953bf7095e0da1cb644443fd0e17d6d"><span class="id" title="notation">).-1</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="max_size_evalC"><span class="id" title="lemma">max_size_evalC</span></a> <span class="id" title="var">u</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.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.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#cb53cf0ee22c036a03b4a9281c68b5a3"><span class="id" title="notation">≤</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#sizeY"><span class="id" title="definition">sizeY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="sizeYE"><span class="id" title="lemma">sizeYE</span></a> <span class="id" title="var">u</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#sizeY"><span class="id" title="definition">sizeY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.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#6cd0f7b28b6092304087c7049437bb1a"><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.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="sizeY_eq0"><span class="id" title="lemma">sizeY_eq0</span></a> <span class="id" title="var">u</span> : <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#sizeY"><span class="id" title="definition">sizeY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.ssreflect.eqtype.html#df45e8c2e8370fd4f0f7c4fdaf208180"><span class="id" title="notation">==</span></a> 0%<span class="id" title="var">N</span><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">)</span></a> <a class="idref" href="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.polyXY.html#u"><span class="id" title="variable">u</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>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="sizeY_mulX"><span class="id" title="lemma">sizeY_mulX</span></a> <span class="id" title="var">u</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#sizeY"><span class="id" title="definition">sizeY</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.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.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="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.polyXY.html#sizeY"><span class="id" title="definition">sizeY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="swapXY_poly_XaY"><span class="id" title="lemma">swapXY_poly_XaY</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#poly_XaY"><span class="id" title="definition">poly_XaY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.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.algebra.polyXY.html#poly_XaY"><span class="id" title="definition">poly_XaY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="swapXY_poly_XmY"><span class="id" title="lemma">swapXY_poly_XmY</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#poly_XmY"><span class="id" title="definition">poly_XmY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.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.algebra.polyXY.html#poly_XmY"><span class="id" title="definition">poly_XmY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="poly_XaY0"><span class="id" title="lemma">poly_XaY0</span></a> : <a class="idref" href="mathcomp.algebra.polyXY.html#poly_XaY"><span class="id" title="definition">poly_XaY</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> 0.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="poly_XmY0"><span class="id" title="lemma">poly_XmY0</span></a> : <a class="idref" href="mathcomp.algebra.polyXY.html#poly_XmY"><span class="id" title="definition">poly_XmY</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> 0.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Ring"><span class="id" title="section">PolyXY_Ring</span></a>.<br/> - -<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="swapXY_map"><span class="id" title="lemma">swapXY_map</span></a> (<span class="id" title="var">R</span> <span class="id" title="var">S</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Ring.Exports.ringType"><span class="id" title="abbreviation">ringType</span></a>) (<span class="id" title="var">f</span> : <a class="idref" href="mathcomp.algebra.ssralg.html#b15d1bebaaff5b5ed693647b6d36f348"><span class="id" title="notation">{</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b15d1bebaaff5b5ed693647b6d36f348"><span class="id" title="notation">additive</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#R"><span class="id" title="variable">R</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.polyXY.html#S"><span class="id" title="variable">S</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#b15d1bebaaff5b5ed693647b6d36f348"><span class="id" title="notation">}</span></a>) <span class="id" title="var">u</span> :<br/> - <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#11a706273cccd094dd42b3c7d6457ef8"><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.algebra.polyXY.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#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#11a706273cccd094dd42b3c7d6457ef8"><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.algebra.polyXY.html#f"><span class="id" title="variable">f</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="PolyXY_ComRing"><span class="id" title="section">PolyXY_ComRing</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="PolyXY_ComRing.R"><span class="id" title="variable">R</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.ComRing.Exports.comRingType"><span class="id" title="abbreviation">comRingType</span></a>.<br/> -<span class="id" title="keyword">Implicit</span> <span class="id" title="keyword">Types</span> (<span class="id" title="var">u</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.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.algebra.polyXY.html#PolyXY_ComRing.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>) (<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.algebra.polyXY.html#PolyXY_ComRing.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>) (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_ComRing.R"><span class="id" title="variable">R</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="horner_swapXY"><span class="id" title="lemma">horner_swapXY</span></a> <span class="id" title="var">u</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.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.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.polyXY.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#11a706273cccd094dd42b3c7d6457ef8"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#eval"><span class="id" title="abbreviation">eval</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="horner_polyC"><span class="id" title="lemma">horner_polyC</span></a> <span class="id" title="var">u</span> <span class="id" title="var">x</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.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.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.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#11a706273cccd094dd42b3c7d6457ef8"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#eval"><span class="id" title="abbreviation">eval</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="horner2_swapXY"><span class="id" title="lemma">horner2_swapXY</span></a> <span class="id" title="var">u</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#swapXY"><span class="id" title="definition">swapXY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><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.polyXY.html#u"><span class="id" title="variable">u</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">]</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="horner_poly_XaY"><span class="id" title="lemma">horner_poly_XaY</span></a> <span class="id" title="var">p</span> <span class="id" title="var">v</span> : <a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#poly_XaY"><span class="id" title="definition">poly_XaY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.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.algebra.polyXY.html#v"><span class="id" title="variable">v</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.polyXY.html#p"><span class="id" title="variable">p</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#011952147f33cb889a964c228c4ebadd"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.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.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.poly.html#011952147f33cb889a964c228c4ebadd"><span class="id" title="notation">)</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="horner_poly_XmY"><span class="id" title="lemma">horner_poly_XmY</span></a> <span class="id" title="var">p</span> <span class="id" title="var">v</span> : <a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#poly_XmY"><span class="id" title="definition">poly_XmY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.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.algebra.polyXY.html#v"><span class="id" title="variable">v</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.polyXY.html#p"><span class="id" title="variable">p</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#011952147f33cb889a964c228c4ebadd"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#v"><span class="id" title="variable">v</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.poly.html#011952147f33cb889a964c228c4ebadd"><span class="id" title="notation">)</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_ComRing"><span class="id" title="section">PolyXY_ComRing</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="PolyXY_Idomain"><span class="id" title="section">PolyXY_Idomain</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variable</span> <a name="PolyXY_Idomain.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> : <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.algebra.polyXY.html#PolyXY_Idomain.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>) (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Idomain.R"><span class="id" title="variable">R</span></a>).<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="size_poly_XaY"><span class="id" title="lemma">size_poly_XaY</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#poly_XaY"><span class="id" title="definition">poly_XaY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.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.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="poly_XaY_eq0"><span class="id" title="lemma">poly_XaY_eq0</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#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#poly_XaY"><span class="id" title="definition">poly_XaY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</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.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</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>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="size_poly_XmY"><span class="id" title="lemma">size_poly_XmY</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#poly_XmY"><span class="id" title="definition">poly_XmY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.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.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="poly_XmY_eq0"><span class="id" title="lemma">poly_XmY_eq0</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#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#poly_XmY"><span class="id" title="definition">poly_XmY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</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.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</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>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="lead_coef_poly_XaY"><span class="id" title="lemma">lead_coef_poly_XaY</span></a> <span class="id" title="var">p</span> : <a class="idref" href="mathcomp.algebra.poly.html#lead_coef"><span class="id" title="definition">lead_coef</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#poly_XaY"><span class="id" title="definition">poly_XaY</span></a> <a class="idref" href="mathcomp.algebra.polyXY.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.algebra.poly.html#8b14e41ab5fcce2460b8672da1456d67"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.poly.html#lead_coef"><span class="id" title="definition">lead_coef</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</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>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="sub_annihilant_in_ideal"><span class="id" title="lemma">sub_annihilant_in_ideal</span></a> <span class="id" title="var">p</span> <span class="id" title="var">q</span> :<br/> - 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.algebra.polyXY.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.algebra.polyXY.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.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">{</span></a><span class="id" title="var">uv</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">:</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.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.algebra.polyXY.html#PolyXY_Idomain.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> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">×</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.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.algebra.polyXY.html#PolyXY_Idomain.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/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><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.algebra.polyXY.html#uv"><span class="id" title="variable">uv</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e0817251e7d67ad994b4d9b1aa82a412"><span class="id" title="notation">.1</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.algebra.polyXY.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#ba2b0e492d2b4675a0acf3ea92aabadd"><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.algebra.polyXY.html#uv"><span class="id" title="variable">uv</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#675082cc4d4538da052b547bdc6ea4c9"><span class="id" title="notation">.2</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#00fe0eaf5e6949f0a31725357afa4bba"><span class="id" title="notation"><</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.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.Init.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">&</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>,<br/> - <a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#sub_annihilant"><span class="id" title="definition">sub_annihilant</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.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="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.polyXY.html#uv"><span class="id" title="variable">uv</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e0817251e7d67ad994b4d9b1aa82a412"><span class="id" title="notation">.1</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><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.polyXY.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.algebra.polyXY.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.algebra.polyXY.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.ssralg.html#c7f78cf1f6a5e4f664654f7d671ca752"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#uv"><span class="id" title="variable">uv</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#675082cc4d4538da052b547bdc6ea4c9"><span class="id" title="notation">.2</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><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.polyXY.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.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.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="sub_annihilantP"><span class="id" title="lemma">sub_annihilantP</span></a> <span class="id" title="var">p</span> <span class="id" title="var">q</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span> :<br/> - <a class="idref" href="mathcomp.algebra.polyXY.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.algebra.polyXY.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.polyXY.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.algebra.polyXY.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> 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.polyXY.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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><br/> - <a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#sub_annihilant"><span class="id" title="definition">sub_annihilant</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#51dc792c356ca1a71a3094b50d6bb2fb"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.algebra.polyXY.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="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="sub_annihilant_neq0"><span class="id" title="lemma">sub_annihilant_neq0</span></a> <span class="id" title="var">p</span> <span class="id" title="var">q</span> : <a class="idref" href="mathcomp.algebra.polyXY.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.algebra.polyXY.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.polyXY.html#sub_annihilant"><span class="id" title="definition">sub_annihilant</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.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.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="div_annihilant_in_ideal"><span class="id" title="lemma">div_annihilant_in_ideal</span></a> <span class="id" title="var">p</span> <span class="id" title="var">q</span> :<br/> - 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.algebra.polyXY.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.algebra.polyXY.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.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">{</span></a><span class="id" title="var">uv</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">:</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.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.algebra.polyXY.html#PolyXY_Idomain.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> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac4"><span class="id" title="notation">×</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.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.algebra.polyXY.html#PolyXY_Idomain.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/> - <a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><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.algebra.polyXY.html#uv"><span class="id" title="variable">uv</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e0817251e7d67ad994b4d9b1aa82a412"><span class="id" title="notation">.1</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.algebra.polyXY.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#ba2b0e492d2b4675a0acf3ea92aabadd"><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.algebra.polyXY.html#uv"><span class="id" title="variable">uv</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#675082cc4d4538da052b547bdc6ea4c9"><span class="id" title="notation">.2</span></a> <a class="idref" href="mathcomp.ssreflect.ssrnat.html#00fe0eaf5e6949f0a31725357afa4bba"><span class="id" title="notation"><</span></a> <a class="idref" href="mathcomp.ssreflect.seq.html#size"><span class="id" title="definition">size</span></a> <a class="idref" href="mathcomp.algebra.polyXY.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.Init.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">&</span></a> <span class="id" title="keyword">∀</span> <span class="id" title="var">x</span> <span class="id" title="var">y</span>,<br/> - <a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#div_annihilant"><span class="id" title="definition">div_annihilant</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.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="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.polyXY.html#uv"><span class="id" title="variable">uv</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#e0817251e7d67ad994b4d9b1aa82a412"><span class="id" title="notation">.1</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><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.polyXY.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.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#2d0cfb150261028f4ebd2ba355623dcc"><span class="id" title="notation">×</span></a> <a class="idref" href="mathcomp.algebra.polyXY.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.ssralg.html#c7f78cf1f6a5e4f664654f7d671ca752"><span class="id" title="notation">+</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#uv"><span class="id" title="variable">uv</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.ssr.ssrfun.html#675082cc4d4538da052b547bdc6ea4c9"><span class="id" title="notation">.2</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><span class="id" title="notation">,</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#75e8653873c0aafbaa165b85523fbcc0"><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.polyXY.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.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.Specif.html#f92718946b2f68c8f7100be4d6b45f82"><span class="id" title="notation">}</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="div_annihilant_neq0"><span class="id" title="lemma">div_annihilant_neq0</span></a> <span class="id" title="var">p</span> <span class="id" title="var">q</span> : <a class="idref" href="mathcomp.algebra.polyXY.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.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">.[</span></a>0<a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><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#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">→</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#div_annihilant"><span class="id" title="definition">div_annihilant</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.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.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Idomain"><span class="id" title="section">PolyXY_Idomain</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Section</span> <a name="PolyXY_Field"><span class="id" title="section">PolyXY_Field</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Variables</span> (<a name="PolyXY_Field.F"><span class="id" title="variable">F</span></a> <a name="PolyXY_Field.E"><span class="id" title="variable">E</span></a> : <a class="idref" href="mathcomp.algebra.ssralg.html#GRing.Field.Exports.fieldType"><span class="id" title="abbreviation">fieldType</span></a>) (<a name="PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</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.algebra.polyXY.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.algebra.polyXY.html#E"><span class="id" title="variable">E</span></a><a class="idref" href="mathcomp.algebra.ssralg.html#d531732ed602c7af62b88c7cfce824e5"><span class="id" title="notation">}</span></a>).<br/> - -<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="div_annihilantP"><span class="id" title="lemma">div_annihilantP</span></a> (<span class="id" title="var">p</span> <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.algebra.polyXY.html#PolyXY_Field.E"><span class="id" title="variable">E</span></a><a class="idref" href="mathcomp.algebra.poly.html#c2ef4fdf7ae62c36654f85f0d2a6c874"><span class="id" title="notation">}</span></a>) (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.E"><span class="id" title="variable">E</span></a>) :<br/> - <a class="idref" href="mathcomp.algebra.polyXY.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.algebra.polyXY.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.polyXY.html#y"><span class="id" title="variable">y</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.polyXY.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.algebra.polyXY.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> 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.polyXY.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">.[</span></a><a class="idref" href="mathcomp.algebra.polyXY.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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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><br/> - <a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#div_annihilant"><span class="id" title="definition">div_annihilant</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#69c431a9c94f6f30a655bd7ddb59037b"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.polyXY.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="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="map_sub_annihilantP"><span class="id" title="lemma">map_sub_annihilantP</span></a> (<span class="id" title="var">p</span> <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.algebra.polyXY.html#PolyXY_Field.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>) (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.E"><span class="id" title="variable">E</span></a>) :<br/> - <a class="idref" href="mathcomp.algebra.polyXY.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.algebra.polyXY.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#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#11a706273cccd094dd42b3c7d6457ef8"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.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> 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#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#11a706273cccd094dd42b3c7d6457ef8"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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><br/> - <a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#sub_annihilant"><span class="id" title="definition">sub_annihilant</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#11a706273cccd094dd42b3c7d6457ef8"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#51dc792c356ca1a71a3094b50d6bb2fb"><span class="id" title="notation">-</span></a> <a class="idref" href="mathcomp.algebra.polyXY.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="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="map_div_annihilantP"><span class="id" title="lemma">map_div_annihilantP</span></a> (<span class="id" title="var">p</span> <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.algebra.polyXY.html#PolyXY_Field.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>) (<span class="id" title="var">x</span> <span class="id" title="var">y</span> : <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.E"><span class="id" title="variable">E</span></a>) :<br/> - <a class="idref" href="mathcomp.algebra.polyXY.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.algebra.polyXY.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.polyXY.html#y"><span class="id" title="variable">y</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#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#11a706273cccd094dd42b3c7d6457ef8"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.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> 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#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#11a706273cccd094dd42b3c7d6457ef8"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.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="http://coq.inria.fr/distrib/V8.9.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><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><br/> - <a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#div_annihilant"><span class="id" title="definition">div_annihilant</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#q"><span class="id" title="variable">q</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#11a706273cccd094dd42b3c7d6457ef8"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="mathcomp.algebra.ssralg.html#69c431a9c94f6f30a655bd7ddb59037b"><span class="id" title="notation">/</span></a> <a class="idref" href="mathcomp.algebra.polyXY.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="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="root_annihilant"><span class="id" title="lemma">root_annihilant</span></a> <span class="id" title="var">x</span> <span class="id" title="var">p</span> (<span class="id" title="var">pEx</span> := <a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#11a706273cccd094dd42b3c7d6457ef8"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#pFtoE"><span class="id" title="abbreviation">pFtoE</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.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.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a>) :<br/> - <a class="idref" href="mathcomp.algebra.polyXY.html#pEx"><span class="id" title="variable">pEx</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.mxpoly.html#algebraicOver"><span class="id" title="definition">algebraicOver</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a> <a class="idref" href="mathcomp.algebra.polyXY.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="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">r</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.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.algebra.polyXY.html#PolyXY_Field.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><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.algebra.polyXY.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 <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> <span class="id" title="keyword">∀</span> <span class="id" title="var">y</span>, <a class="idref" href="mathcomp.algebra.poly.html#root"><span class="id" title="definition">root</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#pEx"><span class="id" title="variable">pEx</span></a> <a class="idref" href="mathcomp.algebra.polyXY.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.algebra.poly.html#root"><span class="id" title="definition">root</span></a> (<a class="idref" href="mathcomp.algebra.polyXY.html#r"><span class="id" title="variable">r</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#11a706273cccd094dd42b3c7d6457ef8"><span class="id" title="notation">^</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a>) <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a>.<br/> - -<br/> -<span class="id" title="keyword">Lemma</span> <a name="algebraic_root_polyXY"><span class="id" title="lemma">algebraic_root_polyXY</span></a> <span class="id" title="var">x</span> <span class="id" title="var">y</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">let</span> <span class="id" title="var">pEx</span> <span class="id" title="var">p</span> := <a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">(</span></a><a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#11a706273cccd094dd42b3c7d6457ef8"><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.algebra.polyXY.html#PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a><a class="idref" href="mathcomp.algebra.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">).[</span></a><a class="idref" href="mathcomp.algebra.polyXY.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.poly.html#e4361ce58e4de0a4b9786d0011b61316"><span class="id" title="notation">]</span></a> <span class="id" title="tactic">in</span><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">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.algebra.polyXY.html#pEx"><span class="id" title="variable">pEx</span></a> <a class="idref" href="mathcomp.algebra.polyXY.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#3df228c109f14f0423b4fccc967ee1ac"><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.polyXY.html#pEx"><span class="id" title="variable">pEx</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#p"><span class="id" title="variable">p</span></a>) <a class="idref" href="mathcomp.algebra.polyXY.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="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.algebra.mxpoly.html#algebraicOver"><span class="id" title="definition">algebraicOver</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a> <a class="idref" href="mathcomp.algebra.polyXY.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.algebra.mxpoly.html#algebraicOver"><span class="id" title="definition">algebraicOver</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field.FtoE"><span class="id" title="variable">FtoE</span></a> <a class="idref" href="mathcomp.algebra.polyXY.html#y"><span class="id" title="variable">y</span></a>.<br/> - -<br/> -<span class="id" title="keyword">End</span> <a class="idref" href="mathcomp.algebra.polyXY.html#PolyXY_Field"><span class="id" title="section">PolyXY_Field</span></a>.<br/> -</div> -</div> - -<div id="footer"> -<hr/><a href="index.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a> -</div> - -</div> - -</body> -</html>
\ No newline at end of file |