![]() |
Metamath
Proof Explorer Theorem List (p. 259 of 480) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cmdg 25801 | Multivariate polynomial degree. |
class mDeg | ||
Syntax | cdg1 25802 | Univariate polynomial degree. |
class deg1 | ||
Definition | df-mdeg 25803* | Define the degree of a polynomial. Note (SO): as an experiment I am using a definition which makes the degree of the zero polynomial -β, contrary to the convention used in df-dgr 25938. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Revised by AV, 25-Jun-2019.) |
β’ mDeg = (π β V, π β V β¦ (π β (Baseβ(π mPoly π)) β¦ sup(ran (β β (π supp (0gβπ)) β¦ (βfld Ξ£g β)), β*, < ))) | ||
Definition | df-deg1 25804 | Define the degree of a univariate polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ deg1 = (π β V β¦ (1o mDeg π)) | ||
Theorem | reldmmdeg 25805 | Multivariate degree is a binary operation. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ Rel dom mDeg | ||
Theorem | tdeglem1 25806* | Functionality of the total degree helper function. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) Remove sethood antecedent. (Revised by SN, 7-Aug-2024.) |
β’ π΄ = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π» = (β β π΄ β¦ (βfld Ξ£g β)) β β’ π»:π΄βΆβ0 | ||
Theorem | tdeglem1OLD 25807* | Obsolete version of tdeglem1 25806 as of 7-Aug-2024. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π΄ = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π» = (β β π΄ β¦ (βfld Ξ£g β)) β β’ (πΌ β π β π»:π΄βΆβ0) | ||
Theorem | tdeglem3 25808* | Additivity of the total degree helper function. (Contributed by Stefan O'Rear, 26-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) Remove a sethood antecedent. (Revised by SN, 7-Aug-2024.) |
β’ π΄ = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π» = (β β π΄ β¦ (βfld Ξ£g β)) β β’ ((π β π΄ β§ π β π΄) β (π»β(π βf + π)) = ((π»βπ) + (π»βπ))) | ||
Theorem | tdeglem3OLD 25809* | Obsolete version of tdeglem3 25808 as of 7-Aug-2024. (Contributed by Stefan O'Rear, 26-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π΄ = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π» = (β β π΄ β¦ (βfld Ξ£g β)) β β’ ((πΌ β π β§ π β π΄ β§ π β π΄) β (π»β(π βf + π)) = ((π»βπ) + (π»βπ))) | ||
Theorem | tdeglem4 25810* | There is only one multi-index with total degree 0. (Contributed by Stefan O'Rear, 29-Mar-2015.) Remove a sethood antecedent. (Revised by SN, 7-Aug-2024.) |
β’ π΄ = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π» = (β β π΄ β¦ (βfld Ξ£g β)) β β’ (π β π΄ β ((π»βπ) = 0 β π = (πΌ Γ {0}))) | ||
Theorem | tdeglem4OLD 25811* | Obsolete version of tdeglem4 25810 as of 7-Aug-2024. (Contributed by Stefan O'Rear, 29-Mar-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π΄ = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π» = (β β π΄ β¦ (βfld Ξ£g β)) β β’ ((πΌ β π β§ π β π΄) β ((π»βπ) = 0 β π = (πΌ Γ {0}))) | ||
Theorem | tdeglem2 25812 | Simplification of total degree for the univariate case. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ (β β (β0 βm 1o) β¦ (βββ )) = (β β (β0 βm 1o) β¦ (βfld Ξ£g β)) | ||
Theorem | mdegfval 25813* | Value of the multivariate degree function. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Revised by AV, 25-Jun-2019.) |
β’ π· = (πΌ mDeg π ) & β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ π΄ = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π» = (β β π΄ β¦ (βfld Ξ£g β)) β β’ π· = (π β π΅ β¦ sup((π» β (π supp 0 )), β*, < )) | ||
Theorem | mdegval 25814* | Value of the multivariate degree function at some particular polynomial. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Revised by AV, 25-Jun-2019.) |
β’ π· = (πΌ mDeg π ) & β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ π΄ = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π» = (β β π΄ β¦ (βfld Ξ£g β)) β β’ (πΉ β π΅ β (π·βπΉ) = sup((π» β (πΉ supp 0 )), β*, < )) | ||
Theorem | mdegleb 25815* | Property of being of limited degree. (Contributed by Stefan O'Rear, 19-Mar-2015.) |
β’ π· = (πΌ mDeg π ) & β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ π΄ = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π» = (β β π΄ β¦ (βfld Ξ£g β)) β β’ ((πΉ β π΅ β§ πΊ β β*) β ((π·βπΉ) β€ πΊ β βπ₯ β π΄ (πΊ < (π»βπ₯) β (πΉβπ₯) = 0 ))) | ||
Theorem | mdeglt 25816* | If there is an upper limit on the degree of a polynomial that is lower than the degree of some exponent bag, then that exponent bag is unrepresented in the polynomial. (Contributed by Stefan O'Rear, 26-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) |
β’ π· = (πΌ mDeg π ) & β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ π΄ = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π» = (β β π΄ β¦ (βfld Ξ£g β)) & β’ (π β πΉ β π΅) & β’ (π β π β π΄) & β’ (π β (π·βπΉ) < (π»βπ)) β β’ (π β (πΉβπ) = 0 ) | ||
Theorem | mdegldg 25817* | A nonzero polynomial has some coefficient which witnesses its degree. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ π· = (πΌ mDeg π ) & β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ π΄ = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π» = (β β π΄ β¦ (βfld Ξ£g β)) & β’ π = (0gβπ) β β’ ((π β Ring β§ πΉ β π΅ β§ πΉ β π) β βπ₯ β π΄ ((πΉβπ₯) β 0 β§ (π»βπ₯) = (π·βπΉ))) | ||
Theorem | mdegxrcl 25818 | Closure of polynomial degree in the extended reals. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) |
β’ π· = (πΌ mDeg π ) & β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) β β’ (πΉ β π΅ β (π·βπΉ) β β*) | ||
Theorem | mdegxrf 25819 | Functionality of polynomial degree in the extended reals. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) |
β’ π· = (πΌ mDeg π ) & β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) β β’ π·:π΅βΆβ* | ||
Theorem | mdegcl 25820 | Sharp closure for multivariate polynomials. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ π· = (πΌ mDeg π ) & β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) β β’ (πΉ β π΅ β (π·βπΉ) β (β0 βͺ {-β})) | ||
Theorem | mdeg0 25821 | Degree of the zero polynomial. (Contributed by Stefan O'Rear, 20-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) |
β’ π· = (πΌ mDeg π ) & β’ π = (πΌ mPoly π ) & β’ 0 = (0gβπ) β β’ ((πΌ β π β§ π β Ring) β (π·β 0 ) = -β) | ||
Theorem | mdegnn0cl 25822 | Degree of a nonzero polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ π· = (πΌ mDeg π ) & β’ π = (πΌ mPoly π ) & β’ 0 = (0gβπ) & β’ π΅ = (Baseβπ) β β’ ((π β Ring β§ πΉ β π΅ β§ πΉ β 0 ) β (π·βπΉ) β β0) | ||
Theorem | degltlem1 25823 | Theorem on arithmetic of extended reals useful for degrees. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ ((π β (β0 βͺ {-β}) β§ π β β€) β (π < π β π β€ (π β 1))) | ||
Theorem | degltp1le 25824 | Theorem on arithmetic of extended reals useful for degrees. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
β’ ((π β (β0 βͺ {-β}) β§ π β β€) β (π < (π + 1) β π β€ π)) | ||
Theorem | mdegaddle 25825 | The degree of a sum is at most the maximum of the degrees of the factors. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
β’ π = (πΌ mPoly π ) & β’ π· = (πΌ mDeg π ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) β β’ (π β (π·β(πΉ + πΊ)) β€ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ))) | ||
Theorem | mdegvscale 25826 | The degree of a scalar multiple of a polynomial is at most the degree of the original polynomial. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
β’ π = (πΌ mPoly π ) & β’ π· = (πΌ mDeg π ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ π΅ = (Baseβπ) & β’ πΎ = (Baseβπ ) & β’ Β· = ( Β·π βπ) & β’ (π β πΉ β πΎ) & β’ (π β πΊ β π΅) β β’ (π β (π·β(πΉ Β· πΊ)) β€ (π·βπΊ)) | ||
Theorem | mdegvsca 25827 | The degree of a scalar multiple of a polynomial is exactly the degree of the original polynomial when the multiple is a nonzero-divisor. (Contributed by Stefan O'Rear, 28-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) |
β’ π = (πΌ mPoly π ) & β’ π· = (πΌ mDeg π ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ π΅ = (Baseβπ) & β’ πΈ = (RLRegβπ ) & β’ Β· = ( Β·π βπ) & β’ (π β πΉ β πΈ) & β’ (π β πΊ β π΅) β β’ (π β (π·β(πΉ Β· πΊ)) = (π·βπΊ)) | ||
Theorem | mdegle0 25828 | A polynomial has nonpositive degree iff it is a constant. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
β’ π = (πΌ mPoly π ) & β’ π· = (πΌ mDeg π ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ π΅ = (Baseβπ) & β’ π΄ = (algScβπ) & β’ (π β πΉ β π΅) β β’ (π β ((π·βπΉ) β€ 0 β πΉ = (π΄β(πΉβ(πΌ Γ {0}))))) | ||
Theorem | mdegmullem 25829* | Lemma for mdegmulle2 25830. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
β’ π = (πΌ mPoly π ) & β’ π· = (πΌ mDeg π ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ π΅ = (Baseβπ) & β’ Β· = (.rβπ) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ (π β π½ β β0) & β’ (π β πΎ β β0) & β’ (π β (π·βπΉ) β€ π½) & β’ (π β (π·βπΊ) β€ πΎ) & β’ π΄ = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ π» = (π β π΄ β¦ (βfld Ξ£g π)) β β’ (π β (π·β(πΉ Β· πΊ)) β€ (π½ + πΎ)) | ||
Theorem | mdegmulle2 25830 | The multivariate degree of a product of polynomials is at most the sum of the degrees of the polynomials. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
β’ π = (πΌ mPoly π ) & β’ π· = (πΌ mDeg π ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ π΅ = (Baseβπ) & β’ Β· = (.rβπ) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ (π β π½ β β0) & β’ (π β πΎ β β0) & β’ (π β (π·βπΉ) β€ π½) & β’ (π β (π·βπΊ) β€ πΎ) β β’ (π β (π·β(πΉ Β· πΊ)) β€ (π½ + πΎ)) | ||
Theorem | deg1fval 25831 | Relate univariate polynomial degree to multivariate. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by Mario Carneiro, 7-Oct-2015.) |
β’ π· = ( deg1 βπ ) β β’ π· = (1o mDeg π ) | ||
Theorem | deg1xrf 25832 | Functionality of univariate polynomial degree, weak range. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) β β’ π·:π΅βΆβ* | ||
Theorem | deg1xrcl 25833 | Closure of univariate polynomial degree in extended reals. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) β β’ (πΉ β π΅ β (π·βπΉ) β β*) | ||
Theorem | deg1cl 25834 | Sharp closure of univariate polynomial degree. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) β β’ (πΉ β π΅ β (π·βπΉ) β (β0 βͺ {-β})) | ||
Theorem | mdegpropd 25835* | Property deduction for polynomial degree. (Contributed by Stefan O'Rear, 28-Mar-2015.) (Proof shortened by AV, 27-Jul-2019.) |
β’ (π β π΅ = (Baseβπ )) & β’ (π β π΅ = (Baseβπ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπ )π¦) = (π₯(+gβπ)π¦)) β β’ (π β (πΌ mDeg π ) = (πΌ mDeg π)) | ||
Theorem | deg1fvi 25836 | Univariate polynomial degree respects protection. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ ( deg1 βπ ) = ( deg1 β( I βπ )) | ||
Theorem | deg1propd 25837* | Property deduction for polynomial degree. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ (π β π΅ = (Baseβπ )) & β’ (π β π΅ = (Baseβπ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπ )π¦) = (π₯(+gβπ)π¦)) β β’ (π β ( deg1 βπ ) = ( deg1 βπ)) | ||
Theorem | deg1z 25838 | Degree of the zero univariate polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ 0 = (0gβπ) β β’ (π β Ring β (π·β 0 ) = -β) | ||
Theorem | deg1nn0cl 25839 | Degree of a nonzero univariate polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015.) (Revised by Mario Carneiro, 7-Oct-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ 0 = (0gβπ) & β’ π΅ = (Baseβπ) β β’ ((π β Ring β§ πΉ β π΅ β§ πΉ β 0 ) β (π·βπΉ) β β0) | ||
Theorem | deg1n0ima 25840 | Degree image of a set of polynomials which does not include zero. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ 0 = (0gβπ) & β’ π΅ = (Baseβπ) β β’ (π β Ring β (π· β (π΅ β { 0 })) β β0) | ||
Theorem | deg1nn0clb 25841 | A polynomial is nonzero iff it has definite degree. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ 0 = (0gβπ) & β’ π΅ = (Baseβπ) β β’ ((π β Ring β§ πΉ β π΅) β (πΉ β 0 β (π·βπΉ) β β0)) | ||
Theorem | deg1lt0 25842 | A polynomial is zero iff it has negative degree. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ 0 = (0gβπ) & β’ π΅ = (Baseβπ) β β’ ((π β Ring β§ πΉ β π΅) β ((π·βπΉ) < 0 β πΉ = 0 )) | ||
Theorem | deg1ldg 25843 | A nonzero univariate polynomial always has a nonzero leading coefficient. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ 0 = (0gβπ) & β’ π΅ = (Baseβπ) & β’ π = (0gβπ ) & β’ π΄ = (coe1βπΉ) β β’ ((π β Ring β§ πΉ β π΅ β§ πΉ β 0 ) β (π΄β(π·βπΉ)) β π) | ||
Theorem | deg1ldgn 25844 | An index at which a polynomial is zero, cannot be its degree. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ 0 = (0gβπ) & β’ π΅ = (Baseβπ) & β’ π = (0gβπ ) & β’ π΄ = (coe1βπΉ) & β’ (π β π β Ring) & β’ (π β πΉ β π΅) & β’ (π β π β β0) & β’ (π β (π΄βπ) = π) β β’ (π β (π·βπΉ) β π) | ||
Theorem | deg1ldgdomn 25845 | A nonzero univariate polynomial over a domain always has a nonzero-divisor leading coefficient. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ 0 = (0gβπ) & β’ π΅ = (Baseβπ) & β’ πΈ = (RLRegβπ ) & β’ π΄ = (coe1βπΉ) β β’ ((π β Domn β§ πΉ β π΅ β§ πΉ β 0 ) β (π΄β(π·βπΉ)) β πΈ) | ||
Theorem | deg1leb 25846* | Property of being of limited degree. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ π΄ = (coe1βπΉ) β β’ ((πΉ β π΅ β§ πΊ β β*) β ((π·βπΉ) β€ πΊ β βπ₯ β β0 (πΊ < π₯ β (π΄βπ₯) = 0 ))) | ||
Theorem | deg1val 25847 | Value of the univariate degree as a supremum. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Revised by AV, 25-Jul-2019.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ π΄ = (coe1βπΉ) β β’ (πΉ β π΅ β (π·βπΉ) = sup((π΄ supp 0 ), β*, < )) | ||
Theorem | deg1lt 25848 | If the degree of a univariate polynomial is less than some index, then that coefficient must be zero. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ π΄ = (coe1βπΉ) β β’ ((πΉ β π΅ β§ πΊ β β0 β§ (π·βπΉ) < πΊ) β (π΄βπΊ) = 0 ) | ||
Theorem | deg1ge 25849 | Conversely, a nonzero coefficient sets a lower bound on the degree. (Contributed by Stefan O'Rear, 23-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ π΄ = (coe1βπΉ) β β’ ((πΉ β π΅ β§ πΊ β β0 β§ (π΄βπΊ) β 0 ) β πΊ β€ (π·βπΉ)) | ||
Theorem | coe1mul3 25850 | The coefficient vector of multiplication in the univariate polynomial ring, at indices high enough that at most one component can be active in the sum. (Contributed by Stefan O'Rear, 25-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ β = (.rβπ) & β’ Β· = (.rβπ ) & β’ π΅ = (Baseβπ) & β’ π· = ( deg1 βπ ) & β’ (π β π β Ring) & β’ (π β πΉ β π΅) & β’ (π β πΌ β β0) & β’ (π β (π·βπΉ) β€ πΌ) & β’ (π β πΊ β π΅) & β’ (π β π½ β β0) & β’ (π β (π·βπΊ) β€ π½) β β’ (π β ((coe1β(πΉ β πΊ))β(πΌ + π½)) = (((coe1βπΉ)βπΌ) Β· ((coe1βπΊ)βπ½))) | ||
Theorem | coe1mul4 25851 | Value of the "leading" coefficient of a product of two nonzero polynomials. This will fail to actually be the leading coefficient only if it is zero (requiring the basic ring to contain zero divisors). (Contributed by Stefan O'Rear, 25-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ β = (.rβπ) & β’ Β· = (.rβπ ) & β’ π΅ = (Baseβπ) & β’ π· = ( deg1 βπ ) & β’ 0 = (0gβπ) & β’ (π β π β Ring) & β’ (π β πΉ β π΅) & β’ (π β πΉ β 0 ) & β’ (π β πΊ β π΅) & β’ (π β πΊ β 0 ) β β’ (π β ((coe1β(πΉ β πΊ))β((π·βπΉ) + (π·βπΊ))) = (((coe1βπΉ)β(π·βπΉ)) Β· ((coe1βπΊ)β(π·βπΊ)))) | ||
Theorem | deg1addle 25852 | The degree of a sum is at most the maximum of the degrees of the factors. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π· = ( deg1 βπ ) & β’ (π β π β Ring) & β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) β β’ (π β (π·β(πΉ + πΊ)) β€ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ))) | ||
Theorem | deg1addle2 25853 | If both factors have degree bounded by πΏ, then the sum of the polynomials also has degree bounded by πΏ. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
β’ π = (Poly1βπ ) & β’ π· = ( deg1 βπ ) & β’ (π β π β Ring) & β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ (π β πΏ β β*) & β’ (π β (π·βπΉ) β€ πΏ) & β’ (π β (π·βπΊ) β€ πΏ) β β’ (π β (π·β(πΉ + πΊ)) β€ πΏ) | ||
Theorem | deg1add 25854 | Exact degree of a sum of two polynomials of unequal degree. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π· = ( deg1 βπ ) & β’ (π β π β Ring) & β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ (π β (π·βπΊ) < (π·βπΉ)) β β’ (π β (π·β(πΉ + πΊ)) = (π·βπΉ)) | ||
Theorem | deg1vscale 25855 | The degree of a scalar times a polynomial is at most the degree of the original polynomial. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π· = ( deg1 βπ ) & β’ (π β π β Ring) & β’ π΅ = (Baseβπ) & β’ πΎ = (Baseβπ ) & β’ Β· = ( Β·π βπ) & β’ (π β πΉ β πΎ) & β’ (π β πΊ β π΅) β β’ (π β (π·β(πΉ Β· πΊ)) β€ (π·βπΊ)) | ||
Theorem | deg1vsca 25856 | The degree of a scalar times a polynomial is exactly the degree of the original polynomial when the scalar is not a zero divisor. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π· = ( deg1 βπ ) & β’ (π β π β Ring) & β’ π΅ = (Baseβπ) & β’ πΈ = (RLRegβπ ) & β’ Β· = ( Β·π βπ) & β’ (π β πΉ β πΈ) & β’ (π β πΊ β π΅) β β’ (π β (π·β(πΉ Β· πΊ)) = (π·βπΊ)) | ||
Theorem | deg1invg 25857 | The degree of the negated polynomial is the same as the original. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π· = ( deg1 βπ ) & β’ (π β π β Ring) & β’ π΅ = (Baseβπ) & β’ π = (invgβπ) & β’ (π β πΉ β π΅) β β’ (π β (π·β(πβπΉ)) = (π·βπΉ)) | ||
Theorem | deg1suble 25858 | The degree of a difference of polynomials is bounded by the maximum of degrees. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π· = ( deg1 βπ ) & β’ (π β π β Ring) & β’ π΅ = (Baseβπ) & β’ β = (-gβπ) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) β β’ (π β (π·β(πΉ β πΊ)) β€ if((π·βπΉ) β€ (π·βπΊ), (π·βπΊ), (π·βπΉ))) | ||
Theorem | deg1sub 25859 | Exact degree of a difference of two polynomials of unequal degree. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π· = ( deg1 βπ ) & β’ (π β π β Ring) & β’ π΅ = (Baseβπ) & β’ β = (-gβπ) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ (π β (π·βπΊ) < (π·βπΉ)) β β’ (π β (π·β(πΉ β πΊ)) = (π·βπΉ)) | ||
Theorem | deg1mulle2 25860 | Produce a bound on the product of two univariate polynomials given bounds on the factors. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π· = ( deg1 βπ ) & β’ (π β π β Ring) & β’ π΅ = (Baseβπ) & β’ Β· = (.rβπ) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ (π β π½ β β0) & β’ (π β πΎ β β0) & β’ (π β (π·βπΉ) β€ π½) & β’ (π β (π·βπΊ) β€ πΎ) β β’ (π β (π·β(πΉ Β· πΊ)) β€ (π½ + πΎ)) | ||
Theorem | deg1sublt 25861 | Subtraction of two polynomials limited to the same degree with the same leading coefficient gives a polynomial with a smaller degree. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ β = (-gβπ) & β’ (π β πΏ β β0) & β’ (π β π β Ring) & β’ (π β πΉ β π΅) & β’ (π β (π·βπΉ) β€ πΏ) & β’ (π β πΊ β π΅) & β’ (π β (π·βπΊ) β€ πΏ) & β’ π΄ = (coe1βπΉ) & β’ πΆ = (coe1βπΊ) & β’ (π β ((coe1βπΉ)βπΏ) = ((coe1βπΊ)βπΏ)) β β’ (π β (π·β(πΉ β πΊ)) < πΏ) | ||
Theorem | deg1le0 25862 | A polynomial has nonpositive degree iff it is a constant. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ π΄ = (algScβπ) β β’ ((π β Ring β§ πΉ β π΅) β ((π·βπΉ) β€ 0 β πΉ = (π΄β((coe1βπΉ)β0)))) | ||
Theorem | deg1sclle 25863 | A scalar polynomial has nonpositive degree. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ πΎ = (Baseβπ ) & β’ π΄ = (algScβπ) β β’ ((π β Ring β§ πΉ β πΎ) β (π·β(π΄βπΉ)) β€ 0) | ||
Theorem | deg1scl 25864 | A nonzero scalar polynomial has zero degree. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ πΎ = (Baseβπ ) & β’ π΄ = (algScβπ) & β’ 0 = (0gβπ ) β β’ ((π β Ring β§ πΉ β πΎ β§ πΉ β 0 ) β (π·β(π΄βπΉ)) = 0) | ||
Theorem | deg1mul2 25865 | Degree of multiplication of two nonzero polynomials when the first leads with a nonzero-divisor coefficient. (Contributed by Stefan O'Rear, 26-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ πΈ = (RLRegβπ ) & β’ π΅ = (Baseβπ) & β’ Β· = (.rβπ) & β’ 0 = (0gβπ) & β’ (π β π β Ring) & β’ (π β πΉ β π΅) & β’ (π β πΉ β 0 ) & β’ (π β ((coe1βπΉ)β(π·βπΉ)) β πΈ) & β’ (π β πΊ β π΅) & β’ (π β πΊ β 0 ) β β’ (π β (π·β(πΉ Β· πΊ)) = ((π·βπΉ) + (π·βπΊ))) | ||
Theorem | deg1mul3 25866 | Degree of multiplication of a polynomial on the left by a nonzero-dividing scalar. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Proof shortened by AV, 25-Jul-2019.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ πΈ = (RLRegβπ ) & β’ π΅ = (Baseβπ) & β’ Β· = (.rβπ) & β’ π΄ = (algScβπ) β β’ ((π β Ring β§ πΉ β πΈ β§ πΊ β π΅) β (π·β((π΄βπΉ) Β· πΊ)) = (π·βπΊ)) | ||
Theorem | deg1mul3le 25867 | Degree of multiplication of a polynomial on the left by a scalar. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ πΎ = (Baseβπ ) & β’ π΅ = (Baseβπ) & β’ Β· = (.rβπ) & β’ π΄ = (algScβπ) β β’ ((π β Ring β§ πΉ β πΎ β§ πΊ β π΅) β (π·β((π΄βπΉ) Β· πΊ)) β€ (π·βπΊ)) | ||
Theorem | deg1tmle 25868 | Limiting degree of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ πΎ = (Baseβπ ) & β’ π = (Poly1βπ ) & β’ π = (var1βπ ) & β’ Β· = ( Β·π βπ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) β β’ ((π β Ring β§ πΆ β πΎ β§ πΉ β β0) β (π·β(πΆ Β· (πΉ β π))) β€ πΉ) | ||
Theorem | deg1tm 25869 | Exact degree of a polynomial term. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ πΎ = (Baseβπ ) & β’ π = (Poly1βπ ) & β’ π = (var1βπ ) & β’ Β· = ( Β·π βπ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) & β’ 0 = (0gβπ ) β β’ ((π β Ring β§ (πΆ β πΎ β§ πΆ β 0 ) β§ πΉ β β0) β (π·β(πΆ Β· (πΉ β π))) = πΉ) | ||
Theorem | deg1pwle 25870 | Limiting degree of a variable power. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ π = (var1βπ ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) β β’ ((π β Ring β§ πΉ β β0) β (π·β(πΉ β π)) β€ πΉ) | ||
Theorem | deg1pw 25871 | Exact degree of a variable power over a nontrivial ring. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ π = (var1βπ ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) β β’ ((π β NzRing β§ πΉ β β0) β (π·β(πΉ β π)) = πΉ) | ||
Theorem | ply1nz 25872 | Univariate polynomials over a nonzero ring are a nonzero ring. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
β’ π = (Poly1βπ ) β β’ (π β NzRing β π β NzRing) | ||
Theorem | ply1nzb 25873 | Univariate polynomials are nonzero iff the base is nonzero. Or in contraposition, the univariate polynomials over the zero ring are also zero. (Contributed by Mario Carneiro, 13-Jun-2015.) |
β’ π = (Poly1βπ ) β β’ (π β Ring β (π β NzRing β π β NzRing)) | ||
Theorem | ply1domn 25874 | Corollary of deg1mul2 25865: the univariate polynomials over a domain are a domain. This is true for multivariate but with a much more complicated proof. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π = (Poly1βπ ) β β’ (π β Domn β π β Domn) | ||
Theorem | ply1idom 25875 | The ring of univariate polynomials over an integral domain is itself an integral domain. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
β’ π = (Poly1βπ ) β β’ (π β IDomn β π β IDomn) | ||
Syntax | cmn1 25876 | Monic polynomials. |
class Monic1p | ||
Syntax | cuc1p 25877 | Unitic polynomials. |
class Unic1p | ||
Syntax | cq1p 25878 | Univariate polynomial quotient. |
class quot1p | ||
Syntax | cr1p 25879 | Univariate polynomial remainder. |
class rem1p | ||
Syntax | cig1p 25880 | Univariate polynomial ideal generator. |
class idlGen1p | ||
Definition | df-mon1 25881* | Define the set of monic univariate polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ Monic1p = (π β V β¦ {π β (Baseβ(Poly1βπ)) β£ (π β (0gβ(Poly1βπ)) β§ ((coe1βπ)β(( deg1 βπ)βπ)) = (1rβπ))}) | ||
Definition | df-uc1p 25882* | Define the set of unitic univariate polynomials, as the polynomials with an invertible leading coefficient. This is not a standard concept but is useful to us as the set of polynomials which can be used as the divisor in the polynomial division theorem ply1divalg 25888. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ Unic1p = (π β V β¦ {π β (Baseβ(Poly1βπ)) β£ (π β (0gβ(Poly1βπ)) β§ ((coe1βπ)β(( deg1 βπ)βπ)) β (Unitβπ))}) | ||
Definition | df-q1p 25883* | Define the quotient of two univariate polynomials, which is guaranteed to exist and be unique by ply1divalg 25888. We actually use the reversed version for better harmony with our divisibility df-dvdsr 20249. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ quot1p = (π β V β¦ β¦(Poly1βπ) / πβ¦β¦(Baseβπ) / πβ¦(π β π, π β π β¦ (β©π β π (( deg1 βπ)β(π(-gβπ)(π(.rβπ)π))) < (( deg1 βπ)βπ)))) | ||
Definition | df-r1p 25884* | Define the remainder after dividing two univariate polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ rem1p = (π β V β¦ β¦(Baseβ(Poly1βπ)) / πβ¦(π β π, π β π β¦ (π(-gβ(Poly1βπ))((π(quot1pβπ)π)(.rβ(Poly1βπ))π)))) | ||
Definition | df-ig1p 25885* | Define a choice function for generators of ideals over a division ring; this is the unique monic polynomial of minimal degree in the ideal. (Contributed by Stefan O'Rear, 29-Mar-2015.) (Revised by AV, 25-Sep-2020.) |
β’ idlGen1p = (π β V β¦ (π β (LIdealβ(Poly1βπ)) β¦ if(π = {(0gβ(Poly1βπ))}, (0gβ(Poly1βπ)), (β©π β (π β© (Monic1pβπ))(( deg1 βπ)βπ) = inf((( deg1 βπ) β (π β {(0gβ(Poly1βπ))})), β, < ))))) | ||
Theorem | ply1divmo 25886* | Uniqueness of a quotient in a polynomial division. For polynomials πΉ, πΊ such that πΊ β 0 and the leading coefficient of πΊ is not a zero divisor, there is at most one polynomial π which satisfies πΉ = (πΊ Β· π) + π where the degree of π is less than the degree of πΊ. (Contributed by Stefan O'Rear, 26-Mar-2015.) (Revised by NM, 17-Jun-2017.) |
β’ π = (Poly1βπ ) & β’ π· = ( deg1 βπ ) & β’ π΅ = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (.rβπ) & β’ (π β π β Ring) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ (π β πΊ β 0 ) & β’ (π β ((coe1βπΊ)β(π·βπΊ)) β πΈ) & β’ πΈ = (RLRegβπ ) β β’ (π β β*π β π΅ (π·β(πΉ β (πΊ β π))) < (π·βπΊ)) | ||
Theorem | ply1divex 25887* | Lemma for ply1divalg 25888: existence part. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π· = ( deg1 βπ ) & β’ π΅ = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (.rβπ) & β’ (π β π β Ring) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ (π β πΊ β 0 ) & β’ 1 = (1rβπ ) & β’ πΎ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ (π β πΌ β πΎ) & β’ (π β (((coe1βπΊ)β(π·βπΊ)) Β· πΌ) = 1 ) β β’ (π β βπ β π΅ (π·β(πΉ β (πΊ β π))) < (π·βπΊ)) | ||
Theorem | ply1divalg 25888* | The division algorithm for univariate polynomials over a ring. For polynomials πΉ, πΊ such that πΊ β 0 and the leading coefficient of πΊ is a unit, there are unique polynomials π and π = πΉ β (πΊ Β· π) such that the degree of π is less than the degree of πΊ. (Contributed by Stefan O'Rear, 27-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π· = ( deg1 βπ ) & β’ π΅ = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (.rβπ) & β’ (π β π β Ring) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ (π β πΊ β 0 ) & β’ (π β ((coe1βπΊ)β(π·βπΊ)) β π) & β’ π = (Unitβπ ) β β’ (π β β!π β π΅ (π·β(πΉ β (πΊ β π))) < (π·βπΊ)) | ||
Theorem | ply1divalg2 25889* | Reverse the order of multiplication in ply1divalg 25888 via the opposite ring. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π· = ( deg1 βπ ) & β’ π΅ = (Baseβπ) & β’ β = (-gβπ) & β’ 0 = (0gβπ) & β’ β = (.rβπ) & β’ (π β π β Ring) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ (π β πΊ β 0 ) & β’ (π β ((coe1βπΊ)β(π·βπΊ)) β π) & β’ π = (Unitβπ ) β β’ (π β β!π β π΅ (π·β(πΉ β (π β πΊ))) < (π·βπΊ)) | ||
Theorem | uc1pval 25890* | Value of the set of unitic polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ π· = ( deg1 βπ ) & β’ πΆ = (Unic1pβπ ) & β’ π = (Unitβπ ) β β’ πΆ = {π β π΅ β£ (π β 0 β§ ((coe1βπ)β(π·βπ)) β π)} | ||
Theorem | isuc1p 25891 | Being a unitic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ π· = ( deg1 βπ ) & β’ πΆ = (Unic1pβπ ) & β’ π = (Unitβπ ) β β’ (πΉ β πΆ β (πΉ β π΅ β§ πΉ β 0 β§ ((coe1βπΉ)β(π·βπΉ)) β π)) | ||
Theorem | mon1pval 25892* | Value of the set of monic polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ π· = ( deg1 βπ ) & β’ π = (Monic1pβπ ) & β’ 1 = (1rβπ ) β β’ π = {π β π΅ β£ (π β 0 β§ ((coe1βπ)β(π·βπ)) = 1 )} | ||
Theorem | ismon1p 25893 | Being a monic polynomial. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ π· = ( deg1 βπ ) & β’ π = (Monic1pβπ ) & β’ 1 = (1rβπ ) β β’ (πΉ β π β (πΉ β π΅ β§ πΉ β 0 β§ ((coe1βπΉ)β(π·βπΉ)) = 1 )) | ||
Theorem | uc1pcl 25894 | Unitic polynomials are polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ πΆ = (Unic1pβπ ) β β’ (πΉ β πΆ β πΉ β π΅) | ||
Theorem | mon1pcl 25895 | Monic polynomials are polynomials. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ π = (Monic1pβπ ) β β’ (πΉ β π β πΉ β π΅) | ||
Theorem | uc1pn0 25896 | Unitic polynomials are not zero. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ 0 = (0gβπ) & β’ πΆ = (Unic1pβπ ) β β’ (πΉ β πΆ β πΉ β 0 ) | ||
Theorem | mon1pn0 25897 | Monic polynomials are not zero. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π = (Poly1βπ ) & β’ 0 = (0gβπ) & β’ π = (Monic1pβπ ) β β’ (πΉ β π β πΉ β 0 ) | ||
Theorem | uc1pdeg 25898 | Unitic polynomials have nonnegative degrees. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ πΆ = (Unic1pβπ ) β β’ ((π β Ring β§ πΉ β πΆ) β (π·βπΉ) β β0) | ||
Theorem | uc1pldg 25899 | Unitic polynomials have unit leading coefficients. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ π = (Unitβπ ) & β’ πΆ = (Unic1pβπ ) β β’ (πΉ β πΆ β ((coe1βπΉ)β(π·βπΉ)) β π) | ||
Theorem | mon1pldg 25900 | Unitic polynomials have one leading coefficients. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π· = ( deg1 βπ ) & β’ 1 = (1rβπ ) & β’ π = (Monic1pβπ ) β β’ (πΉ β π β ((coe1βπΉ)β(π·βπΉ)) = 1 ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |