Metamath Proof Explorer
Table of Contents - 14.1.2. The division algorithm for univariate polynomials
- cmn1
- cuc1p
- cq1p
- cr1p
- cig1p
- df-mon1
- df-uc1p
- df-q1p
- df-r1p
- df-ig1p
- ply1divmo
- ply1divex
- ply1divalg
- ply1divalg2
- uc1pval
- isuc1p
- mon1pval
- ismon1p
- uc1pcl
- mon1pcl
- uc1pn0
- mon1pn0
- uc1pdeg
- uc1pldg
- mon1pldg
- mon1puc1p
- uc1pmon1p
- deg1submon1p
- q1pval
- q1peqb
- q1pcl
- r1pval
- r1pcl
- r1pdeglt
- r1pid
- dvdsq1p
- dvdsr1p
- ply1remlem
- ply1rem
- facth1
- fta1glem1
- fta1glem2
- fta1g
- fta1blem
- fta1b
- drnguc1p
- ig1peu
- ig1pval
- ig1pval2
- ig1pval3
- ig1pcl
- ig1pdvds
- ig1prsp
- ply1lpir
- ply1pid