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

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

Detailed syntax breakdown of Definition df-0p
StepHypRef Expression
1 c0p 20988 . 2  class  0p
2 cc 9267 . . 3  class  CC
3 cc0 9269 . . . 4  class  0
43csn 3865 . . 3  class  { 0 }
52, 4cxp 4825 . 2  class  ( CC 
X.  { 0 } )
61, 5wceq 1362 1  wff  0p  =  ( CC  X.  { 0 } )
Colors of variables: wff setvar class
This definition is referenced by:  0pval  20990  0plef  20991  0pledm  20992  itg1ge0  21005  mbfi1fseqlem5  21038  itg2addlem  21077  ply0  21560  coeeulem  21576  coe0  21607  dgr0  21613  dgreq0  21616  dgrmulc  21622  plymul0or  21631  plydiveu  21648  fta1lem  21657  fta1  21658  quotcan  21659  plyexmo  21663  elqaalem3  21671  aaliou2  21690  plymul02  26794  dgrnznn  29334  mpaaeu  29349
  Copyright terms: Public domain W3C validator