Metamath Proof Explorer

Table of Contents - 11.3. Abstract multivariate polynomials

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. psrbagres
28. gsumbagdiaglem
29. gsumbagdiag
30. psrass1lem
31. psrbas
32. psrelbas
33. psrelbasfun
34. psrplusg
35. psradd
36. psraddcl
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. mplcrngd
121. mpllmodd
122. mplascl0
123. mplascl1
124. ressmplbas2
125. ressmplbas
126. ressmpladd
127. ressmplmul
128. ressmplvsca
129. subrgmpl
130. mplsubrgcl
131. subrgmvr
132. subrgmvrf
133. mplmon
134. mplmonmul
135. mplcoe1
136. mplcoe3
137. mplcoe5lem
138. mplcoe5
139. mplcoe2
140. mplbas2
141. ltbval
142. ltbwe
143. reldmopsr
144. opsrval
145. opsrle
146. opsrval2
147. opsrbaslem
148. opsrbas
149. opsrplusg
150. opsrmulr
151. opsrvsca
152. opsrsca
153. opsrtoslem1
154. opsrtoslem2
155. opsrtos
156. opsrso
157. opsrcrng
158. opsrassa
159. mplmon2
160. psrbag0
161. psrbagsn
162. mplascl
163. mplasclf
164. subrgascl
165. subrgasclcl
166. mplmon2cl
167. mplmon2mul
168. mplind
169. mplcoe4
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
The "variable selection" function
1. cslv
2. df-selv
3. selvffval
4. selvfval
5. selvval
6. mhmcompl
7. mplmapghm
8. mhmcoaddmpl
9. rhmcomulmpl
10. evlscl
11. evlsscaval
12. evlsvarval
13. evlsexpval
14. evlsaddval
15. evlsmulval
16. evlsmaprhm
17. evlsevl
18. evlvvval
19. selvcllem1
20. selvcllem2
21. selvcllem3
22. selvcllemh
23. selvcllem4
24. selvcllem5
25. selvcl
26. selvval2
27. selvvvval
28. selvadd
29. selvmul
Additional definitions for (multivariate) polynomials
1. cmhp
2. cpsd
3. cai
4. df-mhp
5. reldmmhp
6. mhpfval
7. mhpval
8. ismhp
9. ismhp2
10. ismhp3
11. mhprcl
12. mhpmpl
13. mhpdeg
14. mhp0cl
15. mhpsclcl
16. mhpvarcl
17. mhpmulcl
18. mhppwdeg
19. mhpaddcl
20. mhpinvcl
21. mhpsubg
22. mhpvscacl
23. mhplss
24. df-psd
25. psdffval
26. psdfval
27. psdval
28. psdcoef
29. psdcl
30. psdmplcl
31. psdadd
32. psdvsca
33. psdmullem
34. psdmul
35. psd1
36. psdascl
37. psdmvr
38. psdpw
39. df-algind
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. psr1plusg
47. psr1vsca
48. psr1mulr
49. ply1plusg
50. ply1vsca
51. ply1mulr
52. ply1ass23l
53. ressply1bas2
54. ressply1bas
55. ressply1add
56. ressply1mul
57. ressply1vsca
58. subrgply1
59. gsumply1subr
60. psrbaspropd
61. psrplusgpropd
62. mplbaspropd
63. psropprmul
64. ply1opprmul
65. 00ply1bas
66. ply1basfvi
67. ply1plusgfvi
68. ply1baspropd
69. ply1plusgpropd
70. opsrring
71. opsrlmod
72. psr1ring
73. ply1ring
74. psr1lmod
75. psr1sca
76. psr1sca2
77. ply1lmod
78. ply1sca
79. ply1sca2
80. ply1ascl0
81. ply1ascl1
82. ply1mpl0
83. ply10s0
84. ply1mpl1
85. ply1ascl
86. subrg1ascl
87. subrg1asclcl
88. subrgvr1
89. subrgvr1cl
90. coe1z
91. coe1add
92. coe1addfv
93. coe1subfv
94. coe1mul2lem1
95. coe1mul2lem2
96. coe1mul2
97. coe1mul
98. ply1moncl
99. ply1tmcl
100. coe1tm
101. coe1tmfv1
102. coe1tmfv2
103. coe1tmmul2
104. coe1tmmul
105. coe1tmmul2fv
106. coe1pwmul
107. coe1pwmulfv
108. ply1scltm
109. coe1sclmul
110. coe1sclmulfv
111. coe1sclmul2
112. ply1sclf
113. ply1sclcl
114. coe1scl
115. ply1sclid
116. ply1sclf1
117. ply1scl0
118. ply1scln0
119. ply1scl1
120. coe1id
121. ply1idvr1
122. cply1mul
123. ply1coefsupp
124. ply1coe
125. eqcoe1ply1eq
126. ply1coe1eq
127. cply1coe0
128. cply1coe0bi
129. coe1fzgsumdlem
130. coe1fzgsumd
131. ply1scleq
132. ply1chr
133. gsumsmonply1
134. gsummoncoe1
135. gsumply1eq
136. lply1binom
137. lply1binomsc
138. ply1fermltlchr
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