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. dgr0
80. coeidp
81. dgrid
82. dgreq0
83. dgrlt
84. dgradd
85. dgradd2
86. dgrmul2
87. dgrmul
88. dgrmulc
89. dgrsub
90. dgrcolem1
91. dgrcolem2
92. dgrco
93. plycjlem
94. plycj
95. coecj
96. plyrecj
97. plymul0or
98. ofmulrt
99. plyreres
100. dvply1
101. dvply2g
102. dvply2
103. dvnply2
104. dvnply
105. plycpn