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

Definition df-0p 19020
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 19019 . 2  class  0 p
2 cc 8731 . . 3  class  CC
3 cc0 8733 . . . 4  class  0
43csn 3642 . . 3  class  { 0 }
52, 4cxp 4687 . 2  class  ( CC 
X.  { 0 } )
61, 5wceq 1624 1  wff  0 p  =  ( CC  X.  { 0 } )
Colors of variables: wff set class
This definition is referenced by:  0pval  19021  0plef  19022  0pledm  19023  itg1ge0  19036  mbfi1fseqlem5  19069  itg2addlem  19108  ply0  19585  coeeulem  19601  coe0  19632  dgr0  19638  dgreq0  19641  dgrmulc  19647  plymul0or  19656  plydiveu  19673  fta1lem  19682  fta1  19683  quotcan  19684  plyexmo  19688  elqaalem3  19696  aaliou2  19715  dgrnznn  26740  mpaaeu  26755
  Copyright terms: Public domain W3C validator