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

Definition df-0p 19041
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 19040 . 2  class  0 p
2 cc 8751 . . 3  class  CC
3 cc0 8753 . . . 4  class  0
43csn 3653 . . 3  class  { 0 }
52, 4cxp 4703 . 2  class  ( CC 
X.  { 0 } )
61, 5wceq 1632 1  wff  0 p  =  ( CC  X.  { 0 } )
Colors of variables: wff set class
This definition is referenced by:  0pval  19042  0plef  19043  0pledm  19044  itg1ge0  19057  mbfi1fseqlem5  19090  itg2addlem  19129  ply0  19606  coeeulem  19622  coe0  19653  dgr0  19659  dgreq0  19662  dgrmulc  19668  plymul0or  19677  plydiveu  19694  fta1lem  19703  fta1  19704  quotcan  19705  plyexmo  19709  elqaalem3  19717  aaliou2  19736  dgrnznn  27442  mpaaeu  27457
  Copyright terms: Public domain W3C validator