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. snifpsrbag
    17. fczpsrbag
    18. psrbaglesupp
    19. psrbaglecl
    20. psrbagaddcl
    21. psrbagcon
    22. psrbaglefi
    23. psrbagconcl
    24. psrbagconf1o
    25. gsumbagdiaglem
    26. gsumbagdiag
    27. psrass1lem
    28. psrbas
    29. psrelbas
    30. psrelbasfun
    31. psrplusg
    32. psradd
    33. psraddcl
    34. psrmulr
    35. psrmulfval
    36. psrmulval
    37. psrmulcllem
    38. psrmulcl
    39. psrsca
    40. psrvscafval
    41. psrvsca
    42. psrvscaval
    43. psrvscacl
    44. psr0cl
    45. psr0lid
    46. psrnegcl
    47. psrlinv
    48. psrgrp
    49. psr0
    50. psrneg
    51. psrlmod
    52. psr1cl
    53. psrlidm
    54. psrridm
    55. psrass1
    56. psrdi
    57. psrdir
    58. psrass23l
    59. psrcom
    60. psrass23
    61. psrring
    62. psr1
    63. psrcrng
    64. psrassa
    65. resspsrbas
    66. resspsradd
    67. resspsrmul
    68. resspsrvsca
    69. subrgpsr
    70. mvrfval
    71. mvrval
    72. mvrval2
    73. mvrid
    74. mvrf
    75. mvrf1
    76. mvrcl2
    77. reldmmpl
    78. mplval
    79. mplbas
    80. mplelbas
    81. mplval2
    82. mplbasss
    83. mplelf
    84. mplsubglem
    85. mpllsslem
    86. mplsubglem2
    87. mplsubg
    88. mpllss
    89. mplsubrglem
    90. mplsubrg
    91. mpl0
    92. mpladd
    93. mplneg
    94. mplmul
    95. mpl1
    96. mplsca
    97. mplvsca2
    98. mplvsca
    99. mplvscaval
    100. mvrcl
    101. mplgrp
    102. mpllmod
    103. mplring
    104. mpllvec
    105. mplcrng
    106. mplassa
    107. ressmplbas2
    108. ressmplbas
    109. ressmpladd
    110. ressmplmul
    111. ressmplvsca
    112. subrgmpl
    113. subrgmvr
    114. subrgmvrf
    115. mplmon
    116. mplmonmul
    117. mplcoe1
    118. mplcoe3
    119. mplcoe5lem
    120. mplcoe5
    121. mplcoe2
    122. mplbas2
    123. ltbval
    124. ltbwe
    125. reldmopsr
    126. opsrval
    127. opsrle
    128. opsrval2
    129. opsrbaslem
    130. opsrbas
    131. opsrplusg
    132. opsrmulr
    133. opsrvsca
    134. opsrsca
    135. opsrtoslem1
    136. opsrtoslem2
    137. opsrtos
    138. opsrso
    139. opsrcrng
    140. opsrassa
    141. mplrcl
    142. mplelsfi
    143. mvrf2
    144. mplmon2
    145. psrbag0
    146. psrbagsn
    147. mplascl
    148. mplasclf
    149. subrgascl
    150. subrgasclcl
    151. mplmon2cl
    152. mplmon2mul
    153. mplind
    154. mplcoe4
  2. Polynomial evaluation
    1. ces
    2. cevl
    3. df-evls
    4. df-evl
    5. evlslem4
    6. psrbagfsupp
    7. psrbagev1
    8. psrbagev2
    9. evlslem2
    10. evlslem3
    11. evlslem6
    12. evlslem1
    13. evlseu
    14. reldmevls
    15. mpfrcl
    16. evlsval
    17. evlsval2
    18. evlsrhm
    19. evlssca
    20. evlsvar
    21. evlsgsumadd
    22. evlsgsummul
    23. evlspw
    24. evlsvarpw
    25. evlval
    26. evlrhm
    27. evlsscasrng
    28. evlsca
    29. evlsvarsrng
    30. evlvar
    31. mpfconst
    32. mpfproj
    33. mpfsubrg
    34. mpff
    35. mpfaddcl
    36. mpfmulcl
    37. mpfind
  3. Additional definitions for (multivariate) polynomials
    1. cslv
    2. cmhp
    3. cpsd
    4. cai
    5. df-selv
    6. df-mhp
    7. df-psd
    8. df-algind
    9. selvffval
    10. selvfval
    11. selvval
    12. mhpfval
    13. mhpval
    14. ismhp
    15. ismhp2
    16. mhpmpl
    17. mhpdeg
    18. mhp0cl
    19. mhpvarcl
    20. mhpaddcl
    21. mhpinvcl
    22. mhpsubg
    23. mhpvscacl
    24. mhplss
  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. ply1lss
    23. ply1subrg
    24. ply1crng
    25. ply1assa
    26. psr1bascl
    27. psr1basf
    28. ply1basf
    29. ply1bascl
    30. ply1bascl2
    31. coe1fval
    32. coe1fv
    33. fvcoe1
    34. coe1fval3
    35. coe1f2
    36. coe1fval2
    37. coe1f
    38. coe1fvalcl
    39. coe1sfi
    40. coe1fsupp
    41. mptcoe1fsupp
    42. coe1ae0
    43. vr1cl
    44. opsr0
    45. opsr1
    46. mplplusg
    47. mplmulr
    48. psr1plusg
    49. psr1vsca
    50. psr1mulr
    51. ply1plusg
    52. ply1vsca
    53. ply1mulr
    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. ply1mpl0
    82. ply10s0
    83. ply1mpl1
    84. ply1ascl
    85. subrg1ascl
    86. subrg1asclcl
    87. subrgvr1
    88. subrgvr1cl
    89. coe1z
    90. coe1add
    91. coe1addfv
    92. coe1subfv
    93. coe1mul2lem1
    94. coe1mul2lem2
    95. coe1mul2
    96. coe1mul
    97. ply1moncl
    98. ply1tmcl
    99. coe1tm
    100. coe1tmfv1
    101. coe1tmfv2
    102. coe1tmmul2
    103. coe1tmmul
    104. coe1tmmul2fv
    105. coe1pwmul
    106. coe1pwmulfv
    107. ply1scltm
    108. coe1sclmul
    109. coe1sclmulfv
    110. coe1sclmul2
    111. ply1sclf
    112. ply1sclcl
    113. coe1scl
    114. ply1sclid
    115. ply1sclf1
    116. ply1scl0
    117. ply1scln0
    118. ply1scl1
    119. ply1idvr1
    120. cply1mul
    121. ply1coefsupp
    122. ply1coe
    123. eqcoe1ply1eq
    124. ply1coe1eq
    125. cply1coe0
    126. cply1coe0bi
    127. coe1fzgsumdlem
    128. coe1fzgsumd
    129. gsumsmonply1
    130. gsummoncoe1
    131. gsumply1eq
    132. lply1binom
    133. lply1binomsc
  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