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. psrbagfOLD
17. psrbagfsupp
18. psrbagfsuppOLD
19. snifpsrbag
20. fczpsrbag
21. psrbaglesupp
22. psrbaglesuppOLD
23. psrbaglecl
24. psrbagleclOLD
25. psrbagaddcl
26. psrbagaddclOLD
27. psrbagcon
28. psrbagconOLD
29. psrbaglefi
30. psrbaglefiOLD
31. psrbagconcl
32. psrbagconclOLD
33. psrbagconf1o
34. psrbagconf1oOLD
35. gsumbagdiaglemOLD
36. gsumbagdiagOLD
37. psrass1lemOLD
38. gsumbagdiaglem
39. gsumbagdiag
40. psrass1lem
41. psrbas
42. psrelbas
43. psrelbasfun
44. psrplusg
45. psradd
46. psraddcl
47. psrmulr
48. psrmulfval
49. psrmulval
50. psrmulcllem
51. psrmulcl
52. psrsca
53. psrvscafval
54. psrvsca
55. psrvscaval
56. psrvscacl
57. psr0cl
58. psr0lid
59. psrnegcl
60. psrlinv
61. psrgrp
62. psr0
63. psrneg
64. psrlmod
65. psr1cl
66. psrlidm
67. psrridm
68. psrass1
69. psrdi
70. psrdir
71. psrass23l
72. psrcom
73. psrass23
74. psrring
75. psr1
76. psrcrng
77. psrassa
78. resspsrbas
79. resspsradd
80. resspsrmul
81. resspsrvsca
82. subrgpsr
83. mvrfval
84. mvrval
85. mvrval2
86. mvrid
87. mvrf
88. mvrf1
89. mvrcl2
90. reldmmpl
91. mplval
92. mplbas
93. mplelbas
94. mplrcl
95. mplelsfi
96. mplval2
97. mplbasss
98. mplelf
99. mplsubglem
100. mpllsslem
101. mplsubglem2
102. mplsubg
103. mpllss
104. mplsubrglem
105. mplsubrg
106. mpl0
107. mpladd
108. mplneg
109. mplmul
110. mpl1
111. mplsca
112. mplvsca2
113. mplvsca
114. mplvscaval
115. mvrcl
116. mplgrp
117. mpllmod
118. mplring
119. mpllvec
120. mplcrng
121. mplassa
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. opsrbaslemOLD
146. opsrbas
147. opsrbasOLD
148. opsrplusg
149. opsrplusgOLD
150. opsrmulr
151. opsrmulrOLD
152. opsrvsca
153. opsrvscaOLD
154. opsrsca
155. opsrscaOLD
156. opsrtoslem1
157. opsrtoslem2
158. opsrtos
159. opsrso
160. opsrcrng
161. opsrassa
162. mvrf2
163. mplmon2
164. psrbag0
165. psrbagsn
166. mplascl
167. mplasclf
168. subrgascl
169. subrgasclcl
170. mplmon2cl
171. mplmon2mul
172. mplind
173. mplcoe4
Polynomial evaluation
1. ces
2. cevl
3. df-evls
4. df-evl
5. evlslem4
6. psrbagev1
7. psrbagev1OLD
8. psrbagev2
9. psrbagev2OLD
10. evlslem2
11. evlslem3
12. evlslem6
13. evlslem1
14. evlseu
15. reldmevls
16. mpfrcl
17. evlsval
18. evlsval2
19. evlsrhm
20. evlssca
21. evlsvar
22. evlsgsumadd
23. evlsgsummul
24. evlspw
25. evlsvarpw
26. evlval
27. evlrhm
28. evlsscasrng
29. evlsca
30. evlsvarsrng
31. evlvar
32. mpfconst
33. mpfproj
34. mpfsubrg
35. mpff
36. mpfaddcl
37. mpfmulcl
38. mpfind
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. ismhp3
17. mhpmpl
18. mhpdeg
19. mhp0cl
20. mhpsclcl
21. mhpvarcl
22. mhpmulcl
23. mhppwdeg
24. mhpaddcl
25. mhpinvcl
26. mhpsubg
27. mhpvscacl
28. mhplss
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
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