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

Definition df-mdeg 19970
 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 20102. (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 19968 . 2 mDeg
2 vi . . 3
3 vr . . 3
4 cvv 2948 . . 3
5 vf . . . 4
62cv 1651 . . . . . 6
73cv 1651 . . . . . 6
8 cmpl 16400 . . . . . 6 mPoly
96, 7, 8co 6073 . . . . 5 mPoly
10 cbs 13461 . . . . 5
119, 10cfv 5446 . . . 4 mPoly
12 vh . . . . . . 7
135cv 1651 . . . . . . . . 9
1413ccnv 4869 . . . . . . . 8
15 c0g 13715 . . . . . . . . . . 11
167, 15cfv 5446 . . . . . . . . . 10
1716csn 3806 . . . . . . . . 9
184, 17cdif 3309 . . . . . . . 8
1914, 18cima 4873 . . . . . . 7
20 ccnfld 16695 . . . . . . . 8 fld
2112cv 1651 . . . . . . . 8
22 cgsu 13716 . . . . . . . 8 g
2320, 21, 22co 6073 . . . . . . 7 fld g
2412, 19, 23cmpt 4258 . . . . . 6 fld g
2524crn 4871 . . . . 5 fld g
26 cxr 9111 . . . . 5
27 clt 9112 . . . . 5
2825, 26, 27csup 7437 . . . 4 fld g
295, 11, 28cmpt 4258 . . 3 mPoly fld g
302, 3, 4, 4, 29cmpt2 6075 . 2 mPoly fld g
311, 30wceq 1652 1 mDeg mPoly fld g
 Colors of variables: wff set class This definition is referenced by:  reldmmdeg  19972  mdegfval  19977
 Copyright terms: Public domain W3C validator