Metamath Proof Explorer

Table of Contents - 14.1. Polynomials

1. Polynomial degrees
   1. cmdg
   2. cdg1
   3. df-mdeg
   4. df-deg1
   5. reldmmdeg
   6. tdeglem1
   7. tdeglem1OLD
   8. tdeglem3
   9. tdeglem3OLD
   10. tdeglem4
   11. tdeglem4OLD
   12. tdeglem2
   13. mdegfval
   14. mdegval
   15. mdegleb
   16. mdeglt
   17. mdegldg
   18. mdegxrcl
   19. mdegxrf
   20. mdegcl
   21. mdeg0
   22. mdegnn0cl
   23. degltlem1
   24. degltp1le
   25. mdegaddle
   26. mdegvscale
   27. mdegvsca
   28. mdegle0
   29. mdegmullem
   30. mdegmulle2
   31. deg1fval
   32. deg1xrf
   33. deg1xrcl
   34. deg1cl
   35. mdegpropd
   36. deg1fvi
   37. deg1propd
   38. deg1z
   39. deg1nn0cl
   40. deg1n0ima
   41. deg1nn0clb
   42. deg1lt0
   43. deg1ldg
   44. deg1ldgn
   45. deg1ldgdomn
   46. deg1leb
   47. deg1val
   48. deg1lt
   49. deg1ge
   50. coe1mul3
   51. coe1mul4
   52. deg1addle
   53. deg1addle2
   54. deg1add
   55. deg1vscale
   56. deg1vsca
   57. deg1invg
   58. deg1suble
   59. deg1sub
   60. deg1mulle2
   61. deg1sublt
   62. deg1le0
   63. deg1sclle
   64. deg1scl
   65. deg1mul2
   66. deg1mul3
   67. deg1mul3le
   68. deg1tmle
   69. deg1tm
   70. deg1pwle
   71. deg1pw
   72. ply1nz
   73. ply1nzb
   74. ply1domn
   75. ply1idom
2. The division algorithm for univariate polynomials
   1. cmn1
   2. cuc1p
   3. cq1p
   4. cr1p
   5. cig1p
   6. df-mon1
   7. df-uc1p
   8. df-q1p
   9. df-r1p
   10. df-ig1p
   11. ply1divmo
   12. ply1divex
   13. ply1divalg
   14. ply1divalg2
   15. uc1pval
   16. isuc1p
   17. mon1pval
   18. ismon1p
   19. uc1pcl
   20. mon1pcl
   21. uc1pn0
   22. mon1pn0
   23. uc1pdeg
   24. uc1pldg
   25. mon1pldg
   26. mon1puc1p
   27. uc1pmon1p
   28. deg1submon1p
   29. q1pval
   30. q1peqb
   31. q1pcl
   32. r1pval
   33. r1pcl
   34. r1pdeglt
   35. r1pid
   36. dvdsq1p
   37. dvdsr1p
   38. ply1remlem
   39. ply1rem
   40. facth1
   41. fta1glem1
   42. fta1glem2
   43. fta1g
   44. fta1blem
   45. fta1b
   46. drnguc1p
   47. ig1peu
   48. ig1pval
   49. ig1pval2
   50. ig1pval3
   51. ig1pcl
   52. ig1pdvds
   53. ig1prsp
   54. ply1lpir
   55. ply1pid
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
4. The division algorithm for polynomials
   1. cquot
   2. df-quot
   3. quotval
   4. plydivlem1
   5. plydivlem2
   6. plydivlem3
   7. plydivlem4
   8. plydivex
   9. plydiveu
   10. plydivalg
   11. quotlem
   12. quotcl
   13. quotcl2
   14. quotdgr
   15. plyremlem
   16. plyrem
   17. facth
   18. fta1lem
   19. fta1
   20. quotcan
   21. vieta1lem1
   22. vieta1lem2
   23. vieta1
   24. plyexmo
5. Algebraic numbers
   1. caa
   2. df-aa
   3. elaa
   4. aacn
   5. aasscn
   6. elqaalem1
   7. elqaalem2
   8. elqaalem3
   9. elqaa
   10. qaa
   11. qssaa
   12. iaa
   13. aareccl
   14. aacjcl
   15. aannenlem1
   16. aannenlem2
   17. aannenlem3
   18. aannen
6. Liouville's approximation theorem
   1. aalioulem1
   2. aalioulem2
   3. aalioulem3
   4. aalioulem4
   5. aalioulem5
   6. aalioulem6
   7. aaliou
   8. geolim3
   9. aaliou2
   10. aaliou2b
   11. aaliou3lem1
   12. aaliou3lem2
   13. aaliou3lem3
   14. aaliou3lem8
   15. aaliou3lem4
   16. aaliou3lem5
   17. aaliou3lem6
   18. aaliou3lem7
   19. aaliou3lem9
   20. aaliou3