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. 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