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

Definition df-mdeg 19931
 Description: Define the degree of a polynomial. Note (SO): as an experiment I am using a definition which makes the degree of the zero polynomial , contrary to the convention used in df-dgr 20063. (Contributed by Stefan O'Rear, 19-Mar-2015.)
Assertion
Ref Expression
df-mdeg mDeg mPoly fld g
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-mdeg
StepHypRef Expression
1 cmdg 19929 . 2 mDeg
2 vi . . 3
3 vr . . 3
4 cvv 2916 . . 3
5 vf . . . 4
62cv 1648 . . . . . 6
73cv 1648 . . . . . 6
8 cmpl 16363 . . . . . 6 mPoly
96, 7, 8co 6040 . . . . 5 mPoly
10 cbs 13424 . . . . 5
119, 10cfv 5413 . . . 4 mPoly
12 vh . . . . . . 7
135cv 1648 . . . . . . . . 9
1413ccnv 4836 . . . . . . . 8
15 c0g 13678 . . . . . . . . . . 11
167, 15cfv 5413 . . . . . . . . . 10
1716csn 3774 . . . . . . . . 9
184, 17cdif 3277 . . . . . . . 8
1914, 18cima 4840 . . . . . . 7
20 ccnfld 16658 . . . . . . . 8 fld
2112cv 1648 . . . . . . . 8
22 cgsu 13679 . . . . . . . 8 g
2320, 21, 22co 6040 . . . . . . 7 fld g
2412, 19, 23cmpt 4226 . . . . . 6 fld g
2524crn 4838 . . . . 5 fld g
26 cxr 9075 . . . . 5
27 clt 9076 . . . . 5
2825, 26, 27csup 7403 . . . 4 fld g
295, 11, 28cmpt 4226 . . 3 mPoly fld g
302, 3, 4, 4, 29cmpt2 6042 . 2 mPoly fld g
311, 30wceq 1649 1 mDeg mPoly fld g
 Colors of variables: wff set class This definition is referenced by:  reldmmdeg  19933  mdegfval  19938
 Copyright terms: Public domain W3C validator