Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-uc1p Structured version   Unicode version

Definition df-uc1p 20046
 Description: Define the set of unitic univariate polynomials, as the polynomials with an invertible leading coefficient. This is not a standard concept but is useful to us as the set of polynomials which can be used as the divisor in the polynomial division theorem ply1divalg 20052. (Contributed by Stefan O'Rear, 28-Mar-2015.)
Assertion
Ref Expression
df-uc1p Unic1p Poly1 Poly1 coe1 deg1 Unit
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-uc1p
StepHypRef Expression
1 cuc1p 20041 . 2 Unic1p
2 vr . . 3
3 cvv 2948 . . 3
4 vf . . . . . . 7
54cv 1651 . . . . . 6
62cv 1651 . . . . . . . 8
7 cpl1 16563 . . . . . . . 8 Poly1
86, 7cfv 5446 . . . . . . 7 Poly1
9 c0g 13715 . . . . . . 7
108, 9cfv 5446 . . . . . 6 Poly1
115, 10wne 2598 . . . . 5 Poly1
12 cdg1 19969 . . . . . . . . 9 deg1
136, 12cfv 5446 . . . . . . . 8 deg1
145, 13cfv 5446 . . . . . . 7 deg1
15 cco1 16566 . . . . . . . 8 coe1
165, 15cfv 5446 . . . . . . 7 coe1
1714, 16cfv 5446 . . . . . 6 coe1 deg1
18 cui 15736 . . . . . . 7 Unit
196, 18cfv 5446 . . . . . 6 Unit
2017, 19wcel 1725 . . . . 5 coe1 deg1 Unit
2111, 20wa 359 . . . 4 Poly1 coe1 deg1 Unit
22 cbs 13461 . . . . 5
238, 22cfv 5446 . . . 4 Poly1
2421, 4, 23crab 2701 . . 3 Poly1 Poly1 coe1 deg1 Unit
252, 3, 24cmpt 4258 . 2 Poly1 Poly1 coe1 deg1 Unit
261, 25wceq 1652 1 Unic1p Poly1 Poly1 coe1 deg1 Unit
 Colors of variables: wff set class This definition is referenced by:  uc1pval  20054
 Copyright terms: Public domain W3C validator