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

Definition df-mpaa 27316
 Description: Define the minimal polynomial of an algebraic number as the unique monic polynomial which achieves the minimum of degAA. (Contributed by Stefan O'Rear, 25-Nov-2014.)
Assertion
Ref Expression
df-mpaa minPolyAA Polydeg degAA coeffdegAA
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-mpaa
StepHypRef Expression
1 cmpaa 27314 . 2 minPolyAA
2 vx . . 3
3 caa 20223 . . 3
4 vp . . . . . . . 8
54cv 1651 . . . . . . 7
6 cdgr 20098 . . . . . . 7 deg
75, 6cfv 5446 . . . . . 6 deg
82cv 1651 . . . . . . 7
9 cdgraa 27313 . . . . . . 7 degAA
108, 9cfv 5446 . . . . . 6 degAA
117, 10wceq 1652 . . . . 5 deg degAA
128, 5cfv 5446 . . . . . 6
13 cc0 8982 . . . . . 6
1412, 13wceq 1652 . . . . 5
15 ccoe 20097 . . . . . . . 8 coeff
165, 15cfv 5446 . . . . . . 7 coeff
1710, 16cfv 5446 . . . . . 6 coeffdegAA
18 c1 8983 . . . . . 6
1917, 18wceq 1652 . . . . 5 coeffdegAA
2011, 14, 19w3a 936 . . . 4 deg degAA coeffdegAA
21 cq 10566 . . . . 5
22 cply 20095 . . . . 5 Poly
2321, 22cfv 5446 . . . 4 Poly
2420, 4, 23crio 6534 . . 3 Polydeg degAA coeffdegAA
252, 3, 24cmpt 4258 . 2 Polydeg degAA coeffdegAA
261, 25wceq 1652 1 minPolyAA Polydeg degAA coeffdegAA
 Colors of variables: wff set class This definition is referenced by:  mpaaval  27324
 Copyright terms: Public domain W3C validator