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

Definition df-0p 19515
Description: Define the zero polynomial. (Contributed by Mario Carneiro, 19-Jun-2014.)
Assertion
Ref Expression
df-0p  |-  0 p  =  ( CC  X.  { 0 } )

Detailed syntax breakdown of Definition df-0p
StepHypRef Expression
1 c0p 19514 . 2  class  0 p
2 cc 8944 . . 3  class  CC
3 cc0 8946 . . . 4  class  0
43csn 3774 . . 3  class  { 0 }
52, 4cxp 4835 . 2  class  ( CC 
X.  { 0 } )
61, 5wceq 1649 1  wff  0 p  =  ( CC  X.  { 0 } )
Colors of variables: wff set class
This definition is referenced by:  0pval  19516  0plef  19517  0pledm  19518  itg1ge0  19531  mbfi1fseqlem5  19564  itg2addlem  19603  ply0  20080  coeeulem  20096  coe0  20127  dgr0  20133  dgreq0  20136  dgrmulc  20142  plymul0or  20151  plydiveu  20168  fta1lem  20177  fta1  20178  quotcan  20179  plyexmo  20183  elqaalem3  20191  aaliou2  20210  dgrnznn  27208  mpaaeu  27223
  Copyright terms: Public domain W3C validator