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

Definition df-0p 19025
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 19024 . 2  class  0 p
2 cc 8735 . . 3  class  CC
3 cc0 8737 . . . 4  class  0
43csn 3640 . . 3  class  { 0 }
52, 4cxp 4687 . 2  class  ( CC 
X.  { 0 } )
61, 5wceq 1623 1  wff  0 p  =  ( CC  X.  { 0 } )
Colors of variables: wff set class
This definition is referenced by:  0pval  19026  0plef  19027  0pledm  19028  itg1ge0  19041  mbfi1fseqlem5  19074  itg2addlem  19113  ply0  19590  coeeulem  19606  coe0  19637  dgr0  19643  dgreq0  19646  dgrmulc  19652  plymul0or  19661  plydiveu  19678  fta1lem  19687  fta1  19688  quotcan  19689  plyexmo  19693  elqaalem3  19701  aaliou2  19720  dgrnznn  27340  mpaaeu  27355
  Copyright terms: Public domain W3C validator