Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mzp Unicode version

Definition df-mzp 26802
Description: Polynomials over  ZZ with an arbitrary index set, that is, the smallest ring of functions containing all constant functions and all projections. This is almost the most general reasonable definition; to reach full generality, we would need to be able to replace ZZ with an arbitrary (semi-)ring (and a coordinate subring), but rings have not been defined yet. (Contributed by Stefan O'Rear, 4-Oct-2014.)
Assertion
Ref Expression
df-mzp  |- mzPoly  =  ( v  e.  _V  |->  |^| (mzPolyCld `  v )
)

Detailed syntax breakdown of Definition df-mzp
StepHypRef Expression
1 cmzp 26800 . 2  class mzPoly
2 vv . . 3  set  v
3 cvv 2788 . . 3  class  _V
42cv 1622 . . . . 5  class  v
5 cmzpcl 26799 . . . . 5  class mzPolyCld
64, 5cfv 5255 . . . 4  class  (mzPolyCld `  v
)
76cint 3862 . . 3  class  |^| (mzPolyCld `  v )
82, 3, 7cmpt 4077 . 2  class  ( v  e.  _V  |->  |^| (mzPolyCld `  v ) )
91, 8wceq 1623 1  wff mzPoly  =  ( v  e.  _V  |->  |^| (mzPolyCld `  v )
)
Colors of variables: wff set class
This definition is referenced by:  mzpval  26810  dmmzp  26811
  Copyright terms: Public domain W3C validator