![]() |
Metamath
Proof Explorer Theorem List (p. 221 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mplind 22001* | Prove a property of polynomials by "structural" induction, under a simplified model of structure which loses the sum of products structure. The commutativity condition is stronger than strictly needed. (Contributed by Stefan O'Rear, 11-Mar-2015.) |
β’ πΎ = (Baseβπ ) & β’ π = (πΌ mVar π ) & β’ π = (πΌ mPoly π ) & β’ + = (+gβπ) & β’ Β· = (.rβπ) & β’ πΆ = (algScβπ) & β’ π΅ = (Baseβπ) & β’ ((π β§ (π₯ β π» β§ π¦ β π»)) β (π₯ + π¦) β π») & β’ ((π β§ (π₯ β π» β§ π¦ β π»)) β (π₯ Β· π¦) β π») & β’ ((π β§ π₯ β πΎ) β (πΆβπ₯) β π») & β’ ((π β§ π₯ β πΌ) β (πβπ₯) β π») & β’ (π β π β π΅) & β’ (π β πΌ β π) & β’ (π β π β CRing) β β’ (π β π β π») | ||
Theorem | mplcoe4 22002* | Decompose a polynomial into a finite sum of scaled monomials. (Contributed by Stefan O'Rear, 8-Mar-2015.) |
β’ π = (πΌ mPoly π ) & β’ π· = {π β (β0 βm πΌ) β£ (β‘π β β) β Fin} & β’ 0 = (0gβπ ) & β’ π΅ = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ (π β π β π΅) β β’ (π β π = (π Ξ£g (π β π· β¦ (π¦ β π· β¦ if(π¦ = π, (πβπ), 0 ))))) | ||
Syntax | ces 22003 | Evaluation of a multivariate polynomial in a subring. |
class evalSub | ||
Syntax | cevl 22004 | Evaluation of a multivariate polynomial. |
class eval | ||
Definition | df-evls 22005* | Define the evaluation map for the polynomial algebra. The function ((πΌ evalSub π)βπ ):πβΆ(π βm (π βm πΌ)) makes sense when πΌ is an index set, π is a ring, π is a subring of π, and where π is the set of polynomials in (πΌ mPoly π ). This function maps an element of the formal polynomial algebra (with coefficients in π ) to a function from assignments πΌβΆπ of the variables to elements of π formed by evaluating the polynomial with the given assignments. (Contributed by Stefan O'Rear, 11-Mar-2015.) |
β’ evalSub = (π β V, π β CRing β¦ β¦(Baseβπ ) / πβ¦(π β (SubRingβπ ) β¦ β¦(π mPoly (π βΎs π)) / π€β¦(β©π β (π€ RingHom (π βs (π βm π)))((π β (algScβπ€)) = (π₯ β π β¦ ((π βm π) Γ {π₯})) β§ (π β (π mVar (π βΎs π))) = (π₯ β π β¦ (π β (π βm π) β¦ (πβπ₯))))))) | ||
Definition | df-evl 22006* | A simplification of evalSub when the evaluation ring is the same as the coefficient ring. (Contributed by Stefan O'Rear, 19-Mar-2015.) |
β’ eval = (π β V, π β V β¦ ((π evalSub π)β(Baseβπ))) | ||
Theorem | evlslem4 22007* | The support of a tensor product of ring element families is contained in the product of the supports. (Contributed by Stefan O'Rear, 8-Mar-2015.) (Revised by AV, 18-Jul-2019.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β Ring) & β’ ((π β§ π₯ β πΌ) β π β π΅) & β’ ((π β§ π¦ β π½) β π β π΅) & β’ (π β πΌ β π) & β’ (π β π½ β π) β β’ (π β ((π₯ β πΌ, π¦ β π½ β¦ (π Β· π)) supp 0 ) β (((π₯ β πΌ β¦ π) supp 0 ) Γ ((π¦ β π½ β¦ π) supp 0 ))) | ||
Theorem | psrbagev1 22008* | A bag of multipliers provides the conditions for a valid sum. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 18-Jul-2019.) (Revised by AV, 11-Apr-2024.) Remove a sethood hypothesis. (Revised by SN, 7-Aug-2024.) |
β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ πΆ = (Baseβπ) & β’ Β· = (.gβπ) & β’ 0 = (0gβπ) & β’ (π β π β CMnd) & β’ (π β π΅ β π·) & β’ (π β πΊ:πΌβΆπΆ) β β’ (π β ((π΅ βf Β· πΊ):πΌβΆπΆ β§ (π΅ βf Β· πΊ) finSupp 0 )) | ||
Theorem | psrbagev1OLD 22009* | Obsolete version of psrbagev1 22008 as of 7-Aug-2024. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 18-Jul-2019.) (Revised by AV, 11-Apr-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ πΆ = (Baseβπ) & β’ Β· = (.gβπ) & β’ 0 = (0gβπ) & β’ (π β π β CMnd) & β’ (π β π΅ β π·) & β’ (π β πΊ:πΌβΆπΆ) & β’ (π β πΌ β π) β β’ (π β ((π΅ βf Β· πΊ):πΌβΆπΆ β§ (π΅ βf Β· πΊ) finSupp 0 )) | ||
Theorem | psrbagev2 22010* | Closure of a sum using a bag of multipliers. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Proof shortened by AV, 18-Jul-2019.) (Revised by AV, 11-Apr-2024.) Remove a sethood hypothesis. (Revised by SN, 7-Aug-2024.) |
β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ πΆ = (Baseβπ) & β’ Β· = (.gβπ) & β’ (π β π β CMnd) & β’ (π β π΅ β π·) & β’ (π β πΊ:πΌβΆπΆ) β β’ (π β (π Ξ£g (π΅ βf Β· πΊ)) β πΆ) | ||
Theorem | psrbagev2OLD 22011* | Obsolete version of psrbagev2 22010 as of 7-Aug-2024. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Proof shortened by AV, 18-Jul-2019.) (Revised by AV, 11-Apr-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ πΆ = (Baseβπ) & β’ Β· = (.gβπ) & β’ (π β π β CMnd) & β’ (π β π΅ β π·) & β’ (π β πΊ:πΌβΆπΆ) & β’ (π β πΌ β π) β β’ (π β (π Ξ£g (π΅ βf Β· πΊ)) β πΆ) | ||
Theorem | evlslem2 22012* | A linear function on the polynomial ring which is multiplicative on scaled monomials is generally multiplicative. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 11-Apr-2024.) |
β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ Β· = (.rβπ) & β’ 0 = (0gβπ ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β CRing) & β’ (π β πΈ β (π GrpHom π)) & β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π β π· β§ π β π·))) β (πΈβ(π β π· β¦ if(π = (π βf + π), ((π₯βπ)(.rβπ )(π¦βπ)), 0 ))) = ((πΈβ(π β π· β¦ if(π = π, (π₯βπ), 0 ))) Β· (πΈβ(π β π· β¦ if(π = π, (π¦βπ), 0 ))))) β β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΈβ(π₯(.rβπ)π¦)) = ((πΈβπ₯) Β· (πΈβπ¦))) | ||
Theorem | evlslem3 22013* | Lemma for evlseu 22016. Polynomial evaluation of a scaled monomial. (Contributed by Stefan O'Rear, 8-Mar-2015.) (Revised by AV, 11-Apr-2024.) |
β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ πΆ = (Baseβπ) & β’ πΎ = (Baseβπ ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ π = (mulGrpβπ) & β’ β = (.gβπ) & β’ Β· = (.rβπ) & β’ π = (πΌ mVar π ) & β’ πΈ = (π β π΅ β¦ (π Ξ£g (π β π· β¦ ((πΉβ(πβπ)) Β· (π Ξ£g (π βf β πΊ)))))) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β CRing) & β’ (π β πΉ β (π RingHom π)) & β’ (π β πΊ:πΌβΆπΆ) & β’ 0 = (0gβπ ) & β’ (π β π΄ β π·) & β’ (π β π» β πΎ) β β’ (π β (πΈβ(π₯ β π· β¦ if(π₯ = π΄, π», 0 ))) = ((πΉβπ») Β· (π Ξ£g (π΄ βf β πΊ)))) | ||
Theorem | evlslem6 22014* | Lemma for evlseu 22016. Finiteness and consistency of the top-level sum. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 26-Jul-2019.) (Revised by AV, 11-Apr-2024.) |
β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ πΆ = (Baseβπ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ π = (mulGrpβπ) & β’ β = (.gβπ) & β’ Β· = (.rβπ) & β’ π = (πΌ mVar π ) & β’ πΈ = (π β π΅ β¦ (π Ξ£g (π β π· β¦ ((πΉβ(πβπ)) Β· (π Ξ£g (π βf β πΊ)))))) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β CRing) & β’ (π β πΉ β (π RingHom π)) & β’ (π β πΊ:πΌβΆπΆ) & β’ (π β π β π΅) β β’ (π β ((π β π· β¦ ((πΉβ(πβπ)) Β· (π Ξ£g (π βf β πΊ)))):π·βΆπΆ β§ (π β π· β¦ ((πΉβ(πβπ)) Β· (π Ξ£g (π βf β πΊ)))) finSupp (0gβπ))) | ||
Theorem | evlslem1 22015* | Lemma for evlseu 22016, give a formula for (the unique) polynomial evaluation homomorphism. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Proof shortened by AV, 26-Jul-2019.) (Revised by AV, 11-Apr-2024.) |
β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ πΆ = (Baseβπ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ π = (mulGrpβπ) & β’ β = (.gβπ) & β’ Β· = (.rβπ) & β’ π = (πΌ mVar π ) & β’ πΈ = (π β π΅ β¦ (π Ξ£g (π β π· β¦ ((πΉβ(πβπ)) Β· (π Ξ£g (π βf β πΊ)))))) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β CRing) & β’ (π β πΉ β (π RingHom π)) & β’ (π β πΊ:πΌβΆπΆ) & β’ π΄ = (algScβπ) β β’ (π β (πΈ β (π RingHom π) β§ (πΈ β π΄) = πΉ β§ (πΈ β π) = πΊ)) | ||
Theorem | evlseu 22016* | For a given interpretation of the variables πΊ and of the scalars πΉ, this extends to a homomorphic interpretation of the polynomial ring in exactly one way. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 11-Apr-2024.) |
β’ π = (πΌ mPoly π ) & β’ πΆ = (Baseβπ) & β’ π΄ = (algScβπ) & β’ π = (πΌ mVar π ) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β CRing) & β’ (π β πΉ β (π RingHom π)) & β’ (π β πΊ:πΌβΆπΆ) β β’ (π β β!π β (π RingHom π)((π β π΄) = πΉ β§ (π β π) = πΊ)) | ||
Theorem | reldmevls 22017 | Well-behaved binary operation property of evalSub. (Contributed by Stefan O'Rear, 19-Mar-2015.) |
β’ Rel dom evalSub | ||
Theorem | mpfrcl 22018 | Reverse closure for the set of polynomial functions. (Contributed by Stefan O'Rear, 19-Mar-2015.) |
β’ π = ran ((πΌ evalSub π)βπ ) β β’ (π β π β (πΌ β V β§ π β CRing β§ π β (SubRingβπ))) | ||
Theorem | evlsval 22019* | Value of the polynomial evaluation map function. (Contributed by Stefan O'Rear, 11-Mar-2015.) (Revised by AV, 18-Sep-2021.) |
β’ π = ((πΌ evalSub π)βπ ) & β’ π = (πΌ mPoly π) & β’ π = (πΌ mVar π) & β’ π = (π βΎs π ) & β’ π = (π βs (π΅ βm πΌ)) & β’ π΅ = (Baseβπ) & β’ π΄ = (algScβπ) & β’ π = (π₯ β π β¦ ((π΅ βm πΌ) Γ {π₯})) & β’ π = (π₯ β πΌ β¦ (π β (π΅ βm πΌ) β¦ (πβπ₯))) β β’ ((πΌ β π β§ π β CRing β§ π β (SubRingβπ)) β π = (β©π β (π RingHom π)((π β π΄) = π β§ (π β π) = π))) | ||
Theorem | evlsval2 22020* | Characterizing properties of the polynomial evaluation map function. (Contributed by Stefan O'Rear, 12-Mar-2015.) (Revised by AV, 18-Sep-2021.) |
β’ π = ((πΌ evalSub π)βπ ) & β’ π = (πΌ mPoly π) & β’ π = (πΌ mVar π) & β’ π = (π βΎs π ) & β’ π = (π βs (π΅ βm πΌ)) & β’ π΅ = (Baseβπ) & β’ π΄ = (algScβπ) & β’ π = (π₯ β π β¦ ((π΅ βm πΌ) Γ {π₯})) & β’ π = (π₯ β πΌ β¦ (π β (π΅ βm πΌ) β¦ (πβπ₯))) β β’ ((πΌ β π β§ π β CRing β§ π β (SubRingβπ)) β (π β (π RingHom π) β§ ((π β π΄) = π β§ (π β π) = π))) | ||
Theorem | evlsrhm 22021 | Polynomial evaluation is a homomorphism (into the product ring). (Contributed by Stefan O'Rear, 12-Mar-2015.) |
β’ π = ((πΌ evalSub π)βπ ) & β’ π = (πΌ mPoly π) & β’ π = (π βΎs π ) & β’ π = (π βs (π΅ βm πΌ)) & β’ π΅ = (Baseβπ) β β’ ((πΌ β π β§ π β CRing β§ π β (SubRingβπ)) β π β (π RingHom π)) | ||
Theorem | evlssca 22022 | Polynomial evaluation maps scalars to constant functions. (Contributed by Stefan O'Rear, 13-Mar-2015.) (Proof shortened by AV, 18-Sep-2021.) |
β’ π = ((πΌ evalSub π)βπ ) & β’ π = (πΌ mPoly π) & β’ π = (π βΎs π ) & β’ π΅ = (Baseβπ) & β’ π΄ = (algScβπ) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β π ) β β’ (π β (πβ(π΄βπ)) = ((π΅ βm πΌ) Γ {π})) | ||
Theorem | evlsvar 22023* | Polynomial evaluation maps variables to projections. (Contributed by Stefan O'Rear, 12-Mar-2015.) (Proof shortened by AV, 18-Sep-2021.) |
β’ π = ((πΌ evalSub π)βπ ) & β’ π = (πΌ mVar π) & β’ π = (π βΎs π ) & β’ π΅ = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β πΌ) β β’ (π β (πβ(πβπ)) = (π β (π΅ βm πΌ) β¦ (πβπ))) | ||
Theorem | evlsgsumadd 22024* | Polynomial evaluation maps (additive) group sums to group sums. (Contributed by SN, 13-Feb-2024.) |
β’ π = ((πΌ evalSub π)βπ ) & β’ π = (πΌ mPoly π) & β’ 0 = (0gβπ) & β’ π = (π βΎs π ) & β’ π = (π βs (πΎ βm πΌ)) & β’ πΎ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ ((π β§ π₯ β π) β π β π΅) & β’ (π β π β β0) & β’ (π β (π₯ β π β¦ π) finSupp 0 ) β β’ (π β (πβ(π Ξ£g (π₯ β π β¦ π))) = (π Ξ£g (π₯ β π β¦ (πβπ)))) | ||
Theorem | evlsgsummul 22025* | Polynomial evaluation maps (multiplicative) group sums to group sums. (Contributed by SN, 13-Feb-2024.) |
β’ π = ((πΌ evalSub π)βπ ) & β’ π = (πΌ mPoly π) & β’ πΊ = (mulGrpβπ) & β’ 1 = (1rβπ) & β’ π = (π βΎs π ) & β’ π = (π βs (πΎ βm πΌ)) & β’ π» = (mulGrpβπ) & β’ πΎ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ ((π β§ π₯ β π) β π β π΅) & β’ (π β π β β0) & β’ (π β (π₯ β π β¦ π) finSupp 1 ) β β’ (π β (πβ(πΊ Ξ£g (π₯ β π β¦ π))) = (π» Ξ£g (π₯ β π β¦ (πβπ)))) | ||
Theorem | evlspw 22026 | Polynomial evaluation for subrings maps the exponentiation of a polynomial to the exponentiation of the evaluated polynomial. (Contributed by SN, 29-Feb-2024.) |
β’ π = ((πΌ evalSub π)βπ ) & β’ π = (πΌ mPoly π) & β’ πΊ = (mulGrpβπ) & β’ β = (.gβπΊ) & β’ π = (π βΎs π ) & β’ π = (π βs (πΎ βm πΌ)) & β’ π» = (mulGrpβπ) & β’ πΎ = (Baseβπ) & β’ π΅ = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β β0) & β’ (π β π β π΅) β β’ (π β (πβ(π β π)) = (π(.gβπ»)(πβπ))) | ||
Theorem | evlsvarpw 22027 | Polynomial evaluation for subrings maps the exponentiation of a variable to the exponentiation of the evaluated variable. (Contributed by SN, 21-Feb-2024.) |
β’ π = ((πΌ evalSub π)βπ ) & β’ π = (πΌ mPoly π) & β’ πΊ = (mulGrpβπ) & β’ β = (.gβπΊ) & β’ π = ((πΌ mVar π)βπ) & β’ π = (π βΎs π ) & β’ π = (π βs (π΅ βm πΌ)) & β’ π» = (mulGrpβπ) & β’ π΅ = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β πΌ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β β0) β β’ (π β (πβ(π β π)) = (π(.gβπ»)(πβπ))) | ||
Theorem | evlval 22028 | Value of the simple/same ring evaluation map. (Contributed by Stefan O'Rear, 19-Mar-2015.) (Revised by Mario Carneiro, 12-Jun-2015.) |
β’ π = (πΌ eval π ) & β’ π΅ = (Baseβπ ) β β’ π = ((πΌ evalSub π )βπ΅) | ||
Theorem | evlrhm 22029 | The simple evaluation map is a ring homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = (πΌ eval π ) & β’ π΅ = (Baseβπ ) & β’ π = (πΌ mPoly π ) & β’ π = (π βs (π΅ βm πΌ)) β β’ ((πΌ β π β§ π β CRing) β π β (π RingHom π)) | ||
Theorem | evlsscasrng 22030 | The evaluation of a scalar of a subring yields the same result as evaluated as a scalar over the ring itself. (Contributed by AV, 12-Sep-2019.) |
β’ π = ((πΌ evalSub π)βπ ) & β’ π = (πΌ eval π) & β’ π = (πΌ mPoly π) & β’ π = (π βΎs π ) & β’ π = (πΌ mPoly π) & β’ π΅ = (Baseβπ) & β’ π΄ = (algScβπ) & β’ πΆ = (algScβπ) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β π ) β β’ (π β (πβ(π΄βπ)) = (πβ(πΆβπ))) | ||
Theorem | evlsca 22031 | Simple polynomial evaluation maps scalars to constant functions. (Contributed by AV, 12-Sep-2019.) |
β’ π = (πΌ eval π) & β’ π = (πΌ mPoly π) & β’ π΅ = (Baseβπ) & β’ π΄ = (algScβπ) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β π΅) β β’ (π β (πβ(π΄βπ)) = ((π΅ βm πΌ) Γ {π})) | ||
Theorem | evlsvarsrng 22032 | The evaluation of the variable of polynomials over subring yields the same result as evaluated as variable of the polynomials over the ring itself. (Contributed by AV, 12-Sep-2019.) |
β’ π = ((πΌ evalSub π)βπ ) & β’ π = (πΌ eval π) & β’ π = (πΌ mVar π) & β’ π = (π βΎs π ) & β’ π΅ = (Baseβπ) & β’ (π β πΌ β π΄) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β πΌ) β β’ (π β (πβ(πβπ)) = (πβ(πβπ))) | ||
Theorem | evlvar 22033* | Simple polynomial evaluation maps variables to projections. (Contributed by AV, 12-Sep-2019.) |
β’ π = (πΌ eval π) & β’ π = (πΌ mVar π) & β’ π΅ = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β πΌ) β β’ (π β (πβ(πβπ)) = (π β (π΅ βm πΌ) β¦ (πβπ))) | ||
Theorem | mpfconst 22034 | Constants are multivariate polynomial functions. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ π΅ = (Baseβπ) & β’ π = ran ((πΌ evalSub π)βπ ) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β π ) β β’ (π β ((π΅ βm πΌ) Γ {π}) β π) | ||
Theorem | mpfproj 22035* | Projections are multivariate polynomial functions. (Contributed by Mario Carneiro, 20-Mar-2015.) |
β’ π΅ = (Baseβπ) & β’ π = ran ((πΌ evalSub π)βπ ) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π½ β πΌ) β β’ (π β (π β (π΅ βm πΌ) β¦ (πβπ½)) β π) | ||
Theorem | mpfsubrg 22036 | Polynomial functions are a subring. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.) (Revised by AV, 19-Sep-2021.) |
β’ π = ran ((πΌ evalSub π)βπ ) β β’ ((πΌ β π β§ π β CRing β§ π β (SubRingβπ)) β π β (SubRingβ(π βs ((Baseβπ) βm πΌ)))) | ||
Theorem | mpff 22037 | Polynomial functions are functions. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ π = ran ((πΌ evalSub π)βπ ) & β’ π΅ = (Baseβπ) β β’ (πΉ β π β πΉ:(π΅ βm πΌ)βΆπ΅) | ||
Theorem | mpfaddcl 22038 | The sum of multivariate polynomial functions. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ π = ran ((πΌ evalSub π)βπ ) & β’ + = (+gβπ) β β’ ((πΉ β π β§ πΊ β π) β (πΉ βf + πΊ) β π) | ||
Theorem | mpfmulcl 22039 | The product of multivariate polynomial functions. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ π = ran ((πΌ evalSub π)βπ ) & β’ Β· = (.rβπ) β β’ ((πΉ β π β§ πΊ β π) β (πΉ βf Β· πΊ) β π) | ||
Theorem | mpfind 22040* | Prove a property of polynomials by "structural" induction, under a simplified model of structure which loses the sum of products structure. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = (.rβπ) & β’ π = ran ((πΌ evalSub π)βπ ) & β’ ((π β§ ((π β π β§ π) β§ (π β π β§ π))) β π) & β’ ((π β§ ((π β π β§ π) β§ (π β π β§ π))) β π) & β’ (π₯ = ((π΅ βm πΌ) Γ {π}) β (π β π)) & β’ (π₯ = (π β (π΅ βm πΌ) β¦ (πβπ)) β (π β π)) & β’ (π₯ = π β (π β π)) & β’ (π₯ = π β (π β π)) & β’ (π₯ = (π βf + π) β (π β π)) & β’ (π₯ = (π βf Β· π) β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ ((π β§ π β π ) β π) & β’ ((π β§ π β πΌ) β π) & β’ (π β π΄ β π) β β’ (π β π) | ||
Syntax | cslv 22041 | Select a subset of variables in a multivariate polynomial. |
class selectVars | ||
Syntax | cmhp 22042 | Multivariate polynomials. |
class mHomP | ||
Syntax | cpsd 22043 | Power series partial derivative function. |
class mPSDer | ||
Syntax | cai 22044 | Algebraically independent. |
class AlgInd | ||
Definition | df-selv 22045* | Define the "variable selection" function. The function ((πΌ selectVars π )βπ½) maps elements of (πΌ mPoly π ) bijectively onto (π½ mPoly ((πΌ β π½) mPoly π )) in the natural way, for example if πΌ = {π₯, π¦} and π½ = {π¦} it would map 1 + π₯ + π¦ + π₯π¦ β ({π₯, π¦} mPoly β€) to (1 + π₯) + (1 + π₯)π¦ β ({π¦} mPoly ({π₯} mPoly β€)). This, for example, allows one to treat a multivariate polynomial as a univariate polynomial with coefficients in a polynomial ring with one less variable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ selectVars = (π β V, π β V β¦ (π β π« π β¦ (π β (Baseβ(π mPoly π)) β¦ β¦((π β π) mPoly π) / π’β¦β¦(π mPoly π’) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((π evalSub π‘)βran π)β(π β π))β(π₯ β π β¦ if(π₯ β π, ((π mVar π’)βπ₯), (πβ(((π β π) mVar π)βπ₯)))))))) | ||
Theorem | selvffval 22046* | Value of the "variable selection" function. (Contributed by SN, 4-Nov-2023.) |
β’ (π β πΌ β π) & β’ (π β π β π) β β’ (π β (πΌ selectVars π ) = (π β π« πΌ β¦ (π β (Baseβ(πΌ mPoly π )) β¦ β¦((πΌ β π) mPoly π ) / π’β¦β¦(π mPoly π’) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β π))β(π₯ β πΌ β¦ if(π₯ β π, ((π mVar π’)βπ₯), (πβ(((πΌ β π) mVar π )βπ₯)))))))) | ||
Theorem | selvfval 22047* | Value of the "variable selection" function. (Contributed by SN, 4-Nov-2023.) |
β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π½ β πΌ) β β’ (π β ((πΌ selectVars π )βπ½) = (π β (Baseβ(πΌ mPoly π )) β¦ β¦((πΌ β π½) mPoly π ) / π’β¦β¦(π½ mPoly π’) / π‘β¦β¦(algScβπ‘) / πβ¦β¦(π β (algScβπ’)) / πβ¦((((πΌ evalSub π‘)βran π)β(π β π))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π’)βπ₯), (πβ(((πΌ β π½) mVar π )βπ₯))))))) | ||
Theorem | selvval 22048* | Value of the "variable selection" function. (Contributed by SN, 4-Nov-2023.) |
β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ π = ((πΌ β π½) mPoly π ) & β’ π = (π½ mPoly π) & β’ πΆ = (algScβπ) & β’ π· = (πΆ β (algScβπ)) & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π½ β πΌ) & β’ (π β πΉ β π΅) β β’ (π β (((πΌ selectVars π )βπ½)βπΉ) = ((((πΌ evalSub π)βran π·)β(π· β πΉ))β(π₯ β πΌ β¦ if(π₯ β π½, ((π½ mVar π)βπ₯), (πΆβ(((πΌ β π½) mVar π )βπ₯)))))) | ||
Definition | df-mhp 22049* | Define the subspaces of order- π homogeneous polynomials. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ mHomP = (π β V, π β V β¦ (π β β0 β¦ {π β (Baseβ(π mPoly π)) β£ (π supp (0gβπ)) β {π β {β β (β0 βm π) β£ (β‘β β β) β Fin} β£ ((βfld βΎs β0) Ξ£g π) = π}})) | ||
Theorem | mhpfval 22050* | Value of the "homogeneous polynomial" function. (Contributed by Steven Nguyen, 25-Aug-2023.) |
β’ π» = (πΌ mHomP π ) & β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β πΌ β π) & β’ (π β π β π) β β’ (π β π» = (π β β0 β¦ {π β π΅ β£ (π supp 0 ) β {π β π· β£ ((βfld βΎs β0) Ξ£g π) = π}})) | ||
Theorem | mhpval 22051* | Value of the "homogeneous polynomial" function. (Contributed by Steven Nguyen, 25-Aug-2023.) |
β’ π» = (πΌ mHomP π ) & β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π β β0) β β’ (π β (π»βπ) = {π β π΅ β£ (π supp 0 ) β {π β π· β£ ((βfld βΎs β0) Ξ£g π) = π}}) | ||
Theorem | ismhp 22052* | Property of being a homogeneous polynomial. (Contributed by Steven Nguyen, 25-Aug-2023.) |
β’ π» = (πΌ mHomP π ) & β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π β β0) β β’ (π β (π β (π»βπ) β (π β π΅ β§ (π supp 0 ) β {π β π· β£ ((βfld βΎs β0) Ξ£g π) = π}))) | ||
Theorem | ismhp2 22053* | Deduce a homogeneous polynomial from its properties. (Contributed by SN, 25-May-2024.) |
β’ π» = (πΌ mHomP π ) & β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π β β0) & β’ (π β π β π΅) & β’ (π β (π supp 0 ) β {π β π· β£ ((βfld βΎs β0) Ξ£g π) = π}) β β’ (π β π β (π»βπ)) | ||
Theorem | ismhp3 22054* | A polynomial is homogeneous iff the degree of every nonzero term is the same. (Contributed by SN, 22-Jul-2024.) |
β’ π» = (πΌ mHomP π ) & β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π β β0) & β’ (π β π β π΅) β β’ (π β (π β (π»βπ) β βπ β π· ((πβπ) β 0 β ((βfld βΎs β0) Ξ£g π) = π))) | ||
Theorem | mhpmpl 22055 | A homogeneous polynomial is a polynomial. (Contributed by Steven Nguyen, 25-Aug-2023.) |
β’ π» = (πΌ mHomP π ) & β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π β β0) & β’ (π β π β (π»βπ)) β β’ (π β π β π΅) | ||
Theorem | mhpdeg 22056* | All nonzero terms of a homogeneous polynomial have degree π. (Contributed by Steven Nguyen, 25-Aug-2023.) |
β’ π» = (πΌ mHomP π ) & β’ 0 = (0gβπ ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π β β0) & β’ (π β π β (π»βπ)) β β’ (π β (π supp 0 ) β {π β π· β£ ((βfld βΎs β0) Ξ£g π) = π}) | ||
Theorem | mhp0cl 22057* | The zero polynomial is homogeneous. Under df-mhp 22049, it has any (nonnegative integer) degree which loosely corresponds to the value "undefined". The values -β and 0 are also used in Metamath (by df-mdeg 25975 and df-dgr 26112 respectively) and the literature: https://math.stackexchange.com/a/1796314/593843 26112. (Contributed by SN, 12-Sep-2023.) |
β’ π» = (πΌ mHomP π ) & β’ 0 = (0gβπ ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β πΌ β π) & β’ (π β π β Grp) & β’ (π β π β β0) β β’ (π β (π· Γ { 0 }) β (π»βπ)) | ||
Theorem | mhpsclcl 22058 | A scalar (or constant) polynomial has degree 0. Compare deg1scl 26036. In other contexts, there may be an exception for the zero polynomial, but under df-mhp 22049 the zero polynomial can be any degree (see mhp0cl 22057) so there is no exception. (Contributed by SN, 25-May-2024.) |
β’ π» = (πΌ mHomP π ) & β’ π = (πΌ mPoly π ) & β’ π΄ = (algScβπ) & β’ πΎ = (Baseβπ ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ (π β πΆ β πΎ) β β’ (π β (π΄βπΆ) β (π»β0)) | ||
Theorem | mhpvarcl 22059 | A power series variable is a polynomial of degree 1. (Contributed by SN, 25-May-2024.) |
β’ π» = (πΌ mHomP π ) & β’ π = (πΌ mVar π ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ (π β π β πΌ) β β’ (π β (πβπ) β (π»β1)) | ||
Theorem | mhpmulcl 22060 | A product of homogeneous polynomials is a homogeneous polynomial whose degree is the sum of the degrees of the factors. Compare mdegmulle2 26002 (which shows less-than-or-equal instead of equal). (Contributed by SN, 22-Jul-2024.) |
β’ π» = (πΌ mHomP π ) & β’ π = (πΌ mPoly π ) & β’ Β· = (.rβπ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ (π β π β β0) & β’ (π β π β β0) & β’ (π β π β (π»βπ)) & β’ (π β π β (π»βπ)) β β’ (π β (π Β· π) β (π»β(π + π))) | ||
Theorem | mhppwdeg 22061 | Degree of a homogeneous polynomial raised to a power. General version of deg1pw 26043. (Contributed by SN, 26-Jul-2024.) |
β’ π» = (πΌ mHomP π ) & β’ π = (πΌ mPoly π ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ (π β π β β0) & β’ (π β π β β0) & β’ (π β π β (π»βπ)) β β’ (π β (π β π) β (π»β(π Β· π))) | ||
Theorem | mhpaddcl 22062 | Homogeneous polynomials are closed under addition. (Contributed by SN, 26-Aug-2023.) |
β’ π» = (πΌ mHomP π ) & β’ π = (πΌ mPoly π ) & β’ + = (+gβπ) & β’ (π β πΌ β π) & β’ (π β π β Grp) & β’ (π β π β β0) & β’ (π β π β (π»βπ)) & β’ (π β π β (π»βπ)) β β’ (π β (π + π) β (π»βπ)) | ||
Theorem | mhpinvcl 22063 | Homogeneous polynomials are closed under taking the opposite. (Contributed by SN, 12-Sep-2023.) |
β’ π» = (πΌ mHomP π ) & β’ π = (πΌ mPoly π ) & β’ π = (invgβπ) & β’ (π β πΌ β π) & β’ (π β π β Grp) & β’ (π β π β β0) & β’ (π β π β (π»βπ)) β β’ (π β (πβπ) β (π»βπ)) | ||
Theorem | mhpsubg 22064 | Homogeneous polynomials form a subgroup of the polynomials. (Contributed by SN, 25-Sep-2023.) |
β’ π» = (πΌ mHomP π ) & β’ π = (πΌ mPoly π ) & β’ (π β πΌ β π) & β’ (π β π β Grp) & β’ (π β π β β0) β β’ (π β (π»βπ) β (SubGrpβπ)) | ||
Theorem | mhpvscacl 22065 | Homogeneous polynomials are closed under scalar multiplication. (Contributed by SN, 25-Sep-2023.) |
β’ π» = (πΌ mHomP π ) & β’ π = (πΌ mPoly π ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (Baseβπ ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ (π β π β β0) & β’ (π β π β πΎ) & β’ (π β πΉ β (π»βπ)) β β’ (π β (π Β· πΉ) β (π»βπ)) | ||
Theorem | mhplss 22066 | Homogeneous polynomials form a linear subspace of the polynomials. (Contributed by SN, 25-Sep-2023.) |
β’ π» = (πΌ mHomP π ) & β’ π = (πΌ mPoly π ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ (π β π β β0) β β’ (π β (π»βπ) β (LSubSpβπ)) | ||
Definition | df-psd 22067* | Define the differentiation operation on multivariate polynomials. (((πΌ mPSDer π )βπ)βπΉ) is the partial derivative of the polynomial πΉ with respect to π. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ mPSDer = (π β V, π β V β¦ (π₯ β π β¦ (π β (Baseβ(π mPwSer π)) β¦ (π β {β β (β0 βm π) β£ (β‘β β β) β Fin} β¦ (((πβπ₯) + 1)(.gβπ)(πβ(π βf + (π¦ β π β¦ if(π¦ = π₯, 1, 0))))))))) | ||
Theorem | psdffval 22068* | Value of the power series differentiation operation. (Contributed by SN, 11-Apr-2025.) |
β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β πΌ β π) & β’ (π β π β π) β β’ (π β (πΌ mPSDer π ) = (π₯ β πΌ β¦ (π β π΅ β¦ (π β π· β¦ (((πβπ₯) + 1)(.gβπ )(πβ(π βf + (π¦ β πΌ β¦ if(π¦ = π₯, 1, 0))))))))) | ||
Theorem | psdfval 22069* | Give a map between power series and their partial derivatives with respect to a given variable π. (Contributed by SN, 11-Apr-2025.) |
β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π β πΌ) β β’ (π β ((πΌ mPSDer π )βπ) = (π β π΅ β¦ (π β π· β¦ (((πβπ) + 1)(.gβπ )(πβ(π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0)))))))) | ||
Theorem | psdval 22070* | Evaluate the partial derivative of a power series. (Contributed by SN, 11-Apr-2025.) |
β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π β πΌ) & β’ (π β πΉ β π΅) β β’ (π β (((πΌ mPSDer π )βπ)βπΉ) = (π β π· β¦ (((πβπ) + 1)(.gβπ )(πΉβ(π βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0))))))) | ||
Theorem | psdcoef 22071* | Coefficient of a term of the derivative of a power series. (Contributed by SN, 12-Apr-2025.) |
β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ π· = {β β (β0 βm πΌ) β£ (β‘β β β) β Fin} & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π β πΌ) & β’ (π β πΉ β π΅) & β’ (π β πΎ β π·) β β’ (π β ((((πΌ mPSDer π )βπ)βπΉ)βπΎ) = (((πΎβπ) + 1)(.gβπ )(πΉβ(πΎ βf + (π¦ β πΌ β¦ if(π¦ = π, 1, 0)))))) | ||
Theorem | psdcl 22072 | The derivative of a power series is a power series. (Contributed by SN, 11-Apr-2025.) |
β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β Mgm) & β’ (π β π β πΌ) & β’ (π β πΉ β π΅) β β’ (π β (((πΌ mPSDer π )βπ)βπΉ) β π΅) | ||
Theorem | psdmplcl 22073 | The derivative of a polynomial is a polynomial. (Contributed by SN, 12-Apr-2025.) |
β’ π = (πΌ mPoly π ) & β’ π΅ = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β Mnd) & β’ (π β π β πΌ) & β’ (π β πΉ β π΅) β β’ (π β (((πΌ mPSDer π )βπ)βπΉ) β π΅) | ||
Theorem | psdadd 22074 | The derivative of a sum is the sum of the derivatives. (Contributed by SN, 12-Apr-2025.) |
β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ (π β πΌ β π) & β’ (π β π β CMnd) & β’ (π β π β πΌ) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) β β’ (π β (((πΌ mPSDer π )βπ)β(πΉ + πΊ)) = ((((πΌ mPSDer π )βπ)βπΉ) + (((πΌ mPSDer π )βπ)βπΊ))) | ||
Theorem | psdvsca 22075 | The derivative of a scaled power series is the scaled derivative. (Contributed by SN, 12-Apr-2025.) |
β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ πΎ = (Baseβπ ) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β πΌ) & β’ (π β πΉ β π΅) & β’ (π β πΆ β πΎ) β β’ (π β (((πΌ mPSDer π )βπ)β(πΆ Β· πΉ)) = (πΆ Β· (((πΌ mPSDer π )βπ)βπΉ))) | ||
Theorem | psdmullem 22076 | Lemma for psdmul 22077. Transitive law for union of class difference. (Contributed by SN, 5-May-2025.) |
β’ (π β πΆ β π΅) & β’ (π β π΅ β π΄) β β’ (π β ((π΄ β π΅) βͺ (π΅ β πΆ)) = (π΄ β πΆ)) | ||
Theorem | psdmul 22077 | Product rule for power series. An outline is available at https://github.com/icecream17/Stuff/blob/main/math/psdmul.pdf. (Contributed by SN, 25-Apr-2025.) |
β’ π = (πΌ mPwSer π ) & β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = (.rβπ) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β πΌ) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) β β’ (π β (((πΌ mPSDer π )βπ)β(πΉ Β· πΊ)) = (((((πΌ mPSDer π )βπ)βπΉ) Β· πΊ) + (πΉ Β· (((πΌ mPSDer π )βπ)βπΊ)))) | ||
Theorem | psd1 22078 | The derivative of one is zero. (Contributed by SN, 25-Apr-2025.) |
β’ π = (πΌ mPwSer π ) & β’ 1 = (1rβπ) & β’ 0 = (0gβπ) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β πΌ) β β’ (π β (((πΌ mPSDer π )βπ)β 1 ) = 0 ) | ||
Theorem | psdascl 22079 | The derivative of a constant polynomial is zero. (Contributed by SN, 25-Apr-2025.) |
β’ π = (πΌ mPwSer π ) & β’ 0 = (0gβπ) & β’ π΄ = (algScβπ) & β’ π΅ = (Baseβπ ) & β’ (π β πΌ β π) & β’ (π β π β CRing) & β’ (π β π β πΌ) & β’ (π β πΆ β π΅) β β’ (π β (((πΌ mPSDer π )βπ)β(π΄βπΆ)) = 0 ) | ||
Definition | df-algind 22080* | Define the predicate "the set π£ is algebraically independent in the algebra π€". A collection of vectors is algebraically independent if no nontrivial polynomial with elements from the subset evaluates to zero. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ AlgInd = (π€ β V, π β π« (Baseβπ€) β¦ {π£ β π« (Baseβπ€) β£ Fun β‘(π β (Baseβ(π£ mPoly (π€ βΎs π))) β¦ ((((π£ evalSub π€)βπ)βπ)β( I βΎ π£)))}) | ||
According to Wikipedia ("Polynomial", 23-Dec-2019, https://en.wikipedia.org/wiki/Polynomial) "A polynomial in one indeterminate is called a univariate polynomial, a polynomial in more than one indeterminate is called a multivariate polynomial." In this sense univariate polynomials are defined as multivariate polynomials restricted to one indeterminate/polynomial variable in the following, see ply1bascl2 22110. According to the definition in Wikipedia "a polynomial can either be zero or can be written as the sum of a finite number of nonzero terms. Each term consists of the product of a number - called the coefficient of the term - and a finite number of indeterminates, raised to nonnegative integer powers.". By this, a term of a univariate polynomial (often also called "polynomial term") is the product of a coefficient (usually a member of the underlying ring) and the variable, raised to a nonnegative integer power. A (univariate) polynomial which has only one term is called (univariate) monomial - therefore, the notions "term" and "monomial" are often used synonymously, see also the definition in [Lang] p. 102. Sometimes, however, a monomial is defined as power product, "a product of powers of variables with nonnegative integer exponents", see Wikipedia ("Monomial", 23-Dec-2019, https://en.wikipedia.org/wiki/Mononomial 22110). In [Lang] p. 101, such terms are called "primitive monomials". To avoid any ambiguity, the notion "primitive monomial" is used for such power products ("x^i") in the following, whereas the synonym for "term" ("ai x^i") will be "scaled monomial". | ||
Syntax | cps1 22081 | Univariate power series. |
class PwSer1 | ||
Syntax | cv1 22082 | The base variable of a univariate power series. |
class var1 | ||
Syntax | cpl1 22083 | Univariate polynomials. |
class Poly1 | ||
Syntax | cco1 22084 | Coefficient function for a univariate polynomial. |
class coe1 | ||
Syntax | ctp1 22085 | Convert a univariate polynomial representation to multivariate. |
class toPoly1 | ||
Definition | df-psr1 22086 | Define the algebra of univariate power series. (Contributed by Mario Carneiro, 29-Dec-2014.) |
β’ PwSer1 = (π β V β¦ ((1o ordPwSer π)ββ )) | ||
Definition | df-vr1 22087 | Define the base element of a univariate power series (the π element of the set π [π] of polynomials and also the π in the set π [[π]] of power series). (Contributed by Mario Carneiro, 8-Feb-2015.) |
β’ var1 = (π β V β¦ ((1o mVar π)ββ )) | ||
Definition | df-ply1 22088 | Define the algebra of univariate polynomials. (Contributed by Mario Carneiro, 9-Feb-2015.) |
β’ Poly1 = (π β V β¦ ((PwSer1βπ) βΎs (Baseβ(1o mPoly π)))) | ||
Definition | df-coe1 22089* | Define the coefficient function for a univariate polynomial. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
β’ coe1 = (π β V β¦ (π β β0 β¦ (πβ(1o Γ {π})))) | ||
Definition | df-toply1 22090* | Define a function which maps a coefficient function for a univariate polynomial to the corresponding polynomial object. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ toPoly1 = (π β V β¦ (π β (β0 βm 1o) β¦ (πβ(πββ )))) | ||
Theorem | psr1baslem 22091 | The set of finite bags on 1o is just the set of all functions from 1o to β0. (Contributed by Mario Carneiro, 9-Feb-2015.) |
β’ (β0 βm 1o) = {π β (β0 βm 1o) β£ (β‘π β β) β Fin} | ||
Theorem | psr1val 22092 | Value of the ring of univariate power series. (Contributed by Mario Carneiro, 8-Feb-2015.) |
β’ π = (PwSer1βπ ) β β’ π = ((1o ordPwSer π )ββ ) | ||
Theorem | psr1crng 22093 | The ring of univariate power series is a commutative ring. (Contributed by Mario Carneiro, 8-Feb-2015.) |
β’ π = (PwSer1βπ ) β β’ (π β CRing β π β CRing) | ||
Theorem | psr1assa 22094 | The ring of univariate power series is an associative algebra. (Contributed by Mario Carneiro, 8-Feb-2015.) |
β’ π = (PwSer1βπ ) β β’ (π β CRing β π β AssAlg) | ||
Theorem | psr1tos 22095 | The ordered power series structure is a totally ordered set. (Contributed by Mario Carneiro, 2-Jun-2015.) |
β’ π = (PwSer1βπ ) β β’ (π β Toset β π β Toset) | ||
Theorem | psr1bas2 22096 | The base set of the ring of univariate power series. (Contributed by Mario Carneiro, 3-Jul-2015.) |
β’ π = (PwSer1βπ ) & β’ π΅ = (Baseβπ) & β’ π = (1o mPwSer π ) β β’ π΅ = (Baseβπ) | ||
Theorem | psr1bas 22097 | The base set of the ring of univariate power series. (Contributed by Mario Carneiro, 8-Feb-2015.) |
β’ π = (PwSer1βπ ) & β’ π΅ = (Baseβπ) & β’ πΎ = (Baseβπ ) β β’ π΅ = (πΎ βm (β0 βm 1o)) | ||
Theorem | vr1val 22098 | The value of the generator of the power series algebra (the π in π [[π]]). Since all univariate polynomial rings over a fixed base ring π are isomorphic, we don't bother to pass this in as a parameter; internally we are actually using the empty set as this generator and 1o = {β } is the index set (but for most purposes this choice should not be visible anyway). (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by Mario Carneiro, 12-Jun-2015.) |
β’ π = (var1βπ ) β β’ π = ((1o mVar π )ββ ) | ||
Theorem | vr1cl2 22099 | The variable π is a member of the power series algebra π [[π]]. (Contributed by Mario Carneiro, 8-Feb-2015.) |
β’ π = (var1βπ ) & β’ π = (PwSer1βπ ) & β’ π΅ = (Baseβπ) β β’ (π β Ring β π β π΅) | ||
Theorem | ply1val 22100 | The value of the set of univariate polynomials. (Contributed by Mario Carneiro, 9-Feb-2015.) |
β’ π = (Poly1βπ ) & β’ π = (PwSer1βπ ) β β’ π = (π βΎs (Baseβ(1o mPoly π ))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |