Mathbox for Stefan O'Rear |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-mzp | Structured version Visualization version Unicode version |
Description: Polynomials over 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.) |
Ref | Expression |
---|---|
df-mzp | mzPoly mzPolyCld |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cmzp 37285 | . 2 mzPoly | |
2 | vv | . . 3 | |
3 | cvv 3200 | . . 3 | |
4 | 2 | cv 1482 | . . . . 5 |
5 | cmzpcl 37284 | . . . . 5 mzPolyCld | |
6 | 4, 5 | cfv 5888 | . . . 4 mzPolyCld |
7 | 6 | cint 4475 | . . 3 mzPolyCld |
8 | 2, 3, 7 | cmpt 4729 | . 2 mzPolyCld |
9 | 1, 8 | wceq 1483 | 1 mzPoly mzPolyCld |
Colors of variables: wff setvar class |
This definition is referenced by: mzpval 37295 dmmzp 37296 |
Copyright terms: Public domain | W3C validator |