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

Definition df-deg1 19981
Description: Define the degree of a univariate polynomial. (Contributed by Stefan O'Rear, 23-Mar-2015.)
Assertion
Ref Expression
df-deg1  |- deg1  =  (
r  e.  _V  |->  ( 1o mDeg  r ) )

Detailed syntax breakdown of Definition df-deg1
StepHypRef Expression
1 cdg1 19979 . 2  class deg1
2 vr . . 3  set  r
3 cvv 2958 . . 3  class  _V
4 c1o 6719 . . . 4  class  1o
52cv 1652 . . . 4  class  r
6 cmdg 19978 . . . 4  class mDeg
74, 5, 6co 6083 . . 3  class  ( 1o mDeg 
r )
82, 3, 7cmpt 4268 . 2  class  ( r  e.  _V  |->  ( 1o mDeg 
r ) )
91, 8wceq 1653 1  wff deg1  =  (
r  e.  _V  |->  ( 1o mDeg  r ) )
Colors of variables: wff set class
This definition is referenced by:  deg1fval  20005
  Copyright terms: Public domain W3C validator