Metamath Proof Explorer

Table of Contents - 14.1.3. Elementary properties of complex polynomials

1. cply
2. cidp
3. ccoe
4. cdgr
5. df-ply
6. df-idp
7. df-coe
8. df-dgr
9. plyco0
10. plyval
11. plybss
12. elply
13. elply2
14. plyun0
15. plyf
16. plyss
17. plyssc
18. elplyr
19. elplyd
20. ply1termlem
21. ply1term
22. plypow
23. plyconst
24. ne0p
25. ply0
26. plyid
27. plyeq0lem
28. plyeq0
29. plypf1
30. plyaddlem1
31. plymullem1
32. plyaddlem
33. plymullem
34. plyadd
35. plymul
36. plysub
37. plyaddcl
38. plymulcl
39. plysubcl
40. coeval
41. coeeulem
42. coeeu
43. coelem
44. coeeq
45. dgrval
46. dgrlem
47. coef
48. coef2
49. coef3
50. dgrcl
51. dgrub
52. dgrub2
53. dgrlb
54. coeidlem
55. coeid
56. coeid2
57. coeid3
58. plyco
59. coeeq2
60. dgrle
61. dgreq
62. 0dgr
63. 0dgrb
64. dgrnznn
65. coefv0
66. coeaddlem
67. coemullem
68. coeadd
69. coemul
70. coe11
71. coemulhi
72. coemulc
73. coe0
74. coesub
75. coe1termlem
76. coe1term
77. dgr1term
78. plycn
79. plycnOLD
80. dgr0
81. coeidp
82. dgrid
83. dgreq0
84. dgrlt
85. dgradd
86. dgradd2
87. dgrmul2
88. dgrmul
89. dgrmulc
90. dgrsub
91. dgrcolem1
92. dgrcolem2
93. dgrco
94. plycjlem
95. plycj
96. coecj
97. plycjOLD
98. coecjOLD
99. plyrecj
100. plymul0or
101. ofmulrt
102. plyreres
103. dvply1
104. dvply2g
105. dvply2gOLD
106. dvply2
107. dvnply2
108. dvnply
109. plycpn