Metamath Proof Explorer

Table of Contents - 11.3. Abstract multivariate polynomials

1. Definition and basic properties
   1. cmps
   2. cmvr
   3. cmpl
   4. cltb
   5. copws
   6. df-psr
   7. df-mvr
   8. df-mpl
   9. df-ltbag
   10. df-opsr
   11. reldmpsr
   12. psrval
   13. psrvalstr
   14. psrbag
   15. psrbagf
   16. psrbagfsupp
   17. snifpsrbag
   18. fczpsrbag
   19. psrbaglesupp
   20. psrbaglecl
   21. psrbagaddcl
   22. psrbagcon
   23. psrbaglefi
   24. psrbagconcl
   25. psrbagleadd1
   26. psrbagconf1o
   27. gsumbagdiaglem
   28. gsumbagdiag
   29. psrass1lem
   30. psrbas
   31. psrelbas
   32. psrelbasfun
   33. psrplusg
   34. psradd
   35. psraddcl
   36. psraddclOLD
   37. rhmpsrlem1
   38. rhmpsrlem2
   39. psrmulr
   40. psrmulfval
   41. psrmulval
   42. psrmulcllem
   43. psrmulcl
   44. psrsca
   45. psrvscafval
   46. psrvsca
   47. psrvscaval
   48. psrvscacl
   49. psr0cl
   50. psr0lid
   51. psrnegcl
   52. psrlinv
   53. psrgrp
   54. psr0
   55. psrneg
   56. psrlmod
   57. psr1cl
   58. psrlidm
   59. psrridm
   60. psrass1
   61. psrdi
   62. psrdir
   63. psrass23l
   64. psrcom
   65. psrass23
   66. psrring
   67. psr1
   68. psrcrng
   69. psrassa
   70. resspsrbas
   71. resspsradd
   72. resspsrmul
   73. resspsrvsca
   74. subrgpsr
   75. psrascl
   76. psrasclcl
   77. mvrfval
   78. mvrval
   79. mvrval2
   80. mvrid
   81. mvrf
   82. mvrf1
   83. mvrcl2
   84. reldmmpl
   85. mplval
   86. mplbas
   87. mplelbas
   88. mvrcl
   89. mvrf2
   90. mplrcl
   91. mplelsfi
   92. mplval2
   93. mplbasss
   94. mplelf
   95. mplsubglem
   96. mpllsslem
   97. mplsubglem2
   98. mplsubg
   99. mpllss
   100. mplsubrglem
   101. mplsubrg
   102. mpl0
   103. mplplusg
   104. mplmulr
   105. mpladd
   106. mplneg
   107. mplmul
   108. mpl1
   109. mplsca
   110. mplvsca2
   111. mplvsca
   112. mplvscaval
   113. mplgrp
   114. mpllmod
   115. mplring
   116. mpllvec
   117. mplcrng
   118. mplassa
   119. mplringd
   120. mpllmodd
   121. mplascl0
   122. mplascl1
   123. ressmplbas2
   124. ressmplbas
   125. ressmpladd
   126. ressmplmul
   127. ressmplvsca
   128. subrgmpl
   129. subrgmvr
   130. subrgmvrf
   131. mplmon
   132. mplmonmul
   133. mplcoe1
   134. mplcoe3
   135. mplcoe5lem
   136. mplcoe5
   137. mplcoe2
   138. mplbas2
   139. ltbval
   140. ltbwe
   141. reldmopsr
   142. opsrval
   143. opsrle
   144. opsrval2
   145. opsrbaslem
   146. opsrbas
   147. opsrplusg
   148. opsrmulr
   149. opsrvsca
   150. opsrsca
   151. opsrtoslem1
   152. opsrtoslem2
   153. opsrtos
   154. opsrso
   155. opsrcrng
   156. opsrassa
   157. mplmon2
   158. psrbag0
   159. psrbagsn
   160. mplascl
   161. mplasclf
   162. subrgascl
   163. subrgasclcl
   164. mplmon2cl
   165. mplmon2mul
   166. mplind
   167. mplcoe4
2. Polynomial evaluation
   1. ces
   2. cevl
   3. df-evls
   4. df-evl
   5. evlslem4
   6. psrbagev1
   7. psrbagev2
   8. evlslem2
   9. evlslem3
   10. evlslem6
   11. evlslem1
   12. evlseu
   13. reldmevls
   14. mpfrcl
   15. evlsval
   16. evlsval2
   17. evlsrhm
   18. evlsval3
   19. evlsvval
   20. evlsvvvallem
   21. evlsvvvallem2
   22. evlsvvval
   23. evlssca
   24. evlsvar
   25. evlsgsumadd
   26. evlsgsummul
   27. evlspw
   28. evlsvarpw
   29. evlval
   30. evlrhm
   31. evlcl
   32. evladdval
   33. evlmulval
   34. evlsscasrng
   35. evlsca
   36. evlsvarsrng
   37. evlvar
   38. mpfconst
   39. mpfproj
   40. mpfsubrg
   41. mpff
   42. mpfaddcl
   43. mpfmulcl
   44. mpfind
3. Additional definitions for (multivariate) polynomials
   1. cslv
   2. cmhp
   3. cpsd
   4. cai
   5. df-selv
   6. selvffval
   7. selvfval
   8. selvval
   9. df-mhp
   10. reldmmhp
   11. mhpfval
   12. mhpval
   13. ismhp
   14. ismhp2
   15. ismhp3
   16. mhprcl
   17. mhpmpl
   18. mhpdeg
   19. mhp0cl
   20. mhpsclcl
   21. mhpvarcl
   22. mhpmulcl
   23. mhppwdeg
   24. mhpaddcl
   25. mhpinvcl
   26. mhpsubg
   27. mhpvscacl
   28. mhplss
   29. df-psd
   30. psdffval
   31. psdfval
   32. psdval
   33. psdcoef
   34. psdcl
   35. psdmplcl
   36. psdadd
   37. psdvsca
   38. psdmullem
   39. psdmul
   40. psd1
   41. psdascl
   42. psdmvr
   43. psdpw
   44. df-algind
4. Univariate polynomials
   1. cps1
   2. cv1
   3. cpl1
   4. cco1
   5. ctp1
   6. df-psr1
   7. df-vr1
   8. df-ply1
   9. df-coe1
   10. df-toply1
   11. psr1baslem
   12. psr1val
   13. psr1crng
   14. psr1assa
   15. psr1tos
   16. psr1bas2
   17. psr1bas
   18. vr1val
   19. vr1cl2
   20. ply1val
   21. ply1bas
   22. ply1basOLD
   23. ply1lss
   24. ply1subrg
   25. ply1crng
   26. ply1assa
   27. psr1bascl
   28. psr1basf
   29. ply1basf
   30. ply1bascl
   31. ply1bascl2
   32. coe1fval
   33. coe1fv
   34. fvcoe1
   35. coe1fval3
   36. coe1f2
   37. coe1fval2
   38. coe1f
   39. coe1fvalcl
   40. coe1sfi
   41. coe1fsupp
   42. mptcoe1fsupp
   43. coe1ae0
   44. vr1cl
   45. opsr0
   46. opsr1
   47. psr1plusg
   48. psr1vsca
   49. psr1mulr
   50. ply1plusg
   51. ply1vsca
   52. ply1mulr
   53. ply1ass23l
   54. ressply1bas2
   55. ressply1bas
   56. ressply1add
   57. ressply1mul
   58. ressply1vsca
   59. subrgply1
   60. gsumply1subr
   61. psrbaspropd
   62. psrplusgpropd
   63. mplbaspropd
   64. psropprmul
   65. ply1opprmul
   66. 00ply1bas
   67. ply1basfvi
   68. ply1plusgfvi
   69. ply1baspropd
   70. ply1plusgpropd
   71. opsrring
   72. opsrlmod
   73. psr1ring
   74. ply1ring
   75. psr1lmod
   76. psr1sca
   77. psr1sca2
   78. ply1lmod
   79. ply1sca
   80. ply1sca2
   81. ply1ascl0
   82. ply1ascl1
   83. ply1mpl0
   84. ply10s0
   85. ply1mpl1
   86. ply1ascl
   87. subrg1ascl
   88. subrg1asclcl
   89. subrgvr1
   90. subrgvr1cl
   91. coe1z
   92. coe1add
   93. coe1addfv
   94. coe1subfv
   95. coe1mul2lem1
   96. coe1mul2lem2
   97. coe1mul2
   98. coe1mul
   99. ply1moncl
   100. ply1tmcl
   101. coe1tm
   102. coe1tmfv1
   103. coe1tmfv2
   104. coe1tmmul2
   105. coe1tmmul
   106. coe1tmmul2fv
   107. coe1pwmul
   108. coe1pwmulfv
   109. ply1scltm
   110. coe1sclmul
   111. coe1sclmulfv
   112. coe1sclmul2
   113. ply1sclf
   114. ply1sclcl
   115. coe1scl
   116. ply1sclid
   117. ply1sclf1
   118. ply1scl0
   119. ply1scl0OLD
   120. ply1scln0
   121. ply1scl1
   122. ply1scl1OLD
   123. coe1id
   124. ply1idvr1
   125. ply1idvr1OLD
   126. cply1mul
   127. ply1coefsupp
   128. ply1coe
   129. eqcoe1ply1eq
   130. ply1coe1eq
   131. cply1coe0
   132. cply1coe0bi
   133. coe1fzgsumdlem
   134. coe1fzgsumd
   135. ply1scleq
   136. ply1chr
   137. gsumsmonply1
   138. gsummoncoe1
   139. gsumply1eq
   140. lply1binom
   141. lply1binomsc
   142. ply1fermltlchr
5. Univariate polynomial evaluation
   1. ces1
   2. ce1
   3. df-evls1
   4. df-evl1
   5. reldmevls1
   6. ply1frcl
   7. evls1fval
   8. evls1val
   9. evls1rhmlem
   10. evls1rhm
   11. evls1sca
   12. evls1gsumadd
   13. evls1gsummul
   14. evls1pw
   15. evls1varpw
   16. evl1fval
   17. evl1val
   18. evl1fval1lem
   19. evl1fval1
   20. evl1rhm
   21. fveval1fvcl
   22. evl1sca
   23. evl1scad
   24. evl1var
   25. evl1vard
   26. evls1var
   27. evls1scasrng
   28. evls1varsrng
   29. evl1addd
   30. evl1subd
   31. evl1muld
   32. evl1vsd
   33. evl1expd
   34. pf1const
   35. pf1id
   36. pf1subrg
   37. pf1rcl
   38. pf1f
   39. mpfpf1
   40. pf1mpf
   41. pf1addcl
   42. pf1mulcl
   43. pf1ind
   44. evl1gsumdlem
   45. evl1gsumd
   46. evl1gsumadd
   47. evl1gsumaddval
   48. evl1gsummul
   49. evl1varpw
   50. evl1varpwval
   51. evl1scvarpw
   52. evl1scvarpwval
   53. evl1gsummon
   54. Specialization of polynomial evaluation as a ring homomorphism