Metamath Proof Explorer

Table of Contents - 14.1.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. mon1pid
30. q1pval
31. q1peqb
32. q1pcl
33. r1pval
34. r1pcl
35. r1pdeglt
36. r1pid
37. r1pid2
38. dvdsq1p
39. dvdsr1p
40. ply1remlem
41. ply1rem
42. facth1
43. fta1glem1
44. fta1glem2
45. fta1g
46. fta1blem
47. fta1b
48. idomrootle
49. drnguc1p
50. ig1peu
51. ig1pval
52. ig1pval2
53. ig1pval3
54. ig1pcl
55. ig1pdvds
56. ig1prsp
57. ply1lpir
58. ply1pid