Metamath Proof Explorer

Table of Contents - 10.9. 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. 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. mplmul
94. mpl1
95. mplsca
96. mplvsca2
97. mplvsca
98. mplvscaval
99. mvrcl
100. mplgrp
101. mpllmod
102. mplring
103. mpllvec
104. mplcrng
105. mplassa
106. ressmplbas2
107. ressmplbas
108. ressmpladd
109. ressmplmul
110. ressmplvsca
111. subrgmpl
112. subrgmvr
113. subrgmvrf
114. mplmon
115. mplmonmul
116. mplcoe1
117. mplcoe3
118. mplcoe5lem
119. mplcoe5
120. mplcoe2
121. mplbas2
122. ltbval
123. ltbwe
124. reldmopsr
125. opsrval
126. opsrle
127. opsrval2
128. opsrbaslem
129. opsrbas
130. opsrplusg
131. opsrmulr
132. opsrvsca
133. opsrsca
134. opsrtoslem1
135. opsrtoslem2
136. opsrtos
137. opsrso
138. opsrcrng
139. opsrassa
140. mplrcl
141. mplelsfi
142. mvrf2
143. mplmon2
144. psrbag0
145. psrbagsn
146. mplascl
147. mplasclf
148. subrgascl
149. subrgasclcl
150. mplmon2cl
151. mplmon2mul
152. mplind
153. mplcoe4
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
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. mhpmpl
16. mhpdeg
17. mhp0cl
18. mhpaddcl
19. mhpinvcl
20. mhpsubg
21. mhpvscacl
22. 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