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. 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. psrgrpOLD
55. psr0
56. psrneg
57. psrlmod
58. psr1cl
59. psrlidm
60. psrridm
61. psrass1
62. psrdi
63. psrdir
64. psrass23l
65. psrcom
66. psrass23
67. psrring
68. psr1
69. psrcrng
70. psrassa
71. resspsrbas
72. resspsradd
73. resspsrmul
74. resspsrvsca
75. subrgpsr
76. psrascl
77. psrasclcl
78. mvrfval
79. mvrval
80. mvrval2
81. mvrid
82. mvrf
83. mvrf1
84. mvrcl2
85. reldmmpl
86. mplval
87. mplbas
88. mplelbas
89. mvrcl
90. mvrf2
91. mplrcl
92. mplelsfi
93. mplval2
94. mplbasss
95. mplelf
96. mplsubglem
97. mpllsslem
98. mplsubglem2
99. mplsubg
100. mpllss
101. mplsubrglem
102. mplsubrg
103. mpl0
104. mplplusg
105. mplmulr
106. mpladd
107. mplneg
108. mplmul
109. mpl1
110. mplsca
111. mplvsca2
112. mplvsca
113. mplvscaval
114. mplgrp
115. mpllmod
116. mplring
117. mpllvec
118. mplcrng
119. mplassa
120. mplringd
121. mpllmodd
122. ressmplbas2
123. ressmplbas
124. ressmpladd
125. ressmplmul
126. ressmplvsca
127. subrgmpl
128. subrgmvr
129. subrgmvrf
130. mplmon
131. mplmonmul
132. mplcoe1
133. mplcoe3
134. mplcoe5lem
135. mplcoe5
136. mplcoe2
137. mplbas2
138. ltbval
139. ltbwe
140. reldmopsr
141. opsrval
142. opsrle
143. opsrval2
144. opsrbaslem
145. opsrbas
146. opsrplusg
147. opsrmulr
148. opsrvsca
149. opsrsca
150. opsrtoslem1
151. opsrtoslem2
152. opsrtos
153. opsrso
154. opsrcrng
155. opsrassa
156. mplmon2
157. psrbag0
158. psrbagsn
159. mplascl
160. mplasclf
161. subrgascl
162. subrgasclcl
163. mplmon2cl
164. mplmon2mul
165. mplind
166. 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. evlssca
19. evlsvar
20. evlsgsumadd
21. evlsgsummul
22. evlspw
23. evlsvarpw
24. evlval
25. evlrhm
26. evlsscasrng
27. evlsca
28. evlsvarsrng
29. evlvar
30. mpfconst
31. mpfproj
32. mpfsubrg
33. mpff
34. mpfaddcl
35. mpfmulcl
36. mpfind
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
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. ply1idvr1
124. ply1idvr1OLD
125. cply1mul
126. ply1coefsupp
127. ply1coe
128. eqcoe1ply1eq
129. ply1coe1eq
130. cply1coe0
131. cply1coe0bi
132. coe1fzgsumdlem
133. coe1fzgsumd
134. ply1scleq
135. ply1chr
136. gsumsmonply1
137. gsummoncoe1
138. gsumply1eq
139. lply1binom
140. lply1binomsc
141. 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