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

Definition df-0p 19240
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 19239 . 2  class  0 p
2 cc 8882 . . 3  class  CC
3 cc0 8884 . . . 4  class  0
43csn 3729 . . 3  class  { 0 }
52, 4cxp 4790 . 2  class  ( CC 
X.  { 0 } )
61, 5wceq 1647 1  wff  0 p  =  ( CC  X.  { 0 } )
Colors of variables: wff set class
This definition is referenced by:  0pval  19241  0plef  19242  0pledm  19243  itg1ge0  19256  mbfi1fseqlem5  19289  itg2addlem  19328  ply0  19805  coeeulem  19821  coe0  19852  dgr0  19858  dgreq0  19861  dgrmulc  19867  plymul0or  19876  plydiveu  19893  fta1lem  19902  fta1  19903  quotcan  19904  plyexmo  19908  elqaalem3  19916  aaliou2  19935  dgrnznn  26846  mpaaeu  26861
  Copyright terms: Public domain W3C validator