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

Definition df-itgo 27343
 Description: A complex number is said to be integral over a subset if it is the root of a monic polynomial with coefficients from the subset. This definition is typically not used for fields but it works there, see aaitgo 27346. This definition could work for subsets of an arbitrary ring with a more general definition of polynomials. TODO: use (Contributed by Stefan O'Rear, 27-Nov-2014.)
Assertion
Ref Expression
df-itgo IntgOver Poly coeffdeg
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-itgo
StepHypRef Expression
1 citgo 27341 . 2 IntgOver
2 vs . . 3
3 cc 8990 . . . 4
43cpw 3801 . . 3
5 vx . . . . . . . . 9
65cv 1652 . . . . . . . 8
7 vp . . . . . . . . 9
87cv 1652 . . . . . . . 8
96, 8cfv 5456 . . . . . . 7
10 cc0 8992 . . . . . . 7
119, 10wceq 1653 . . . . . 6
12 cdgr 20108 . . . . . . . . 9 deg
138, 12cfv 5456 . . . . . . . 8 deg
14 ccoe 20107 . . . . . . . . 9 coeff
158, 14cfv 5456 . . . . . . . 8 coeff
1613, 15cfv 5456 . . . . . . 7 coeffdeg
17 c1 8993 . . . . . . 7
1816, 17wceq 1653 . . . . . 6 coeffdeg
1911, 18wa 360 . . . . 5 coeffdeg
202cv 1652 . . . . . 6
21 cply 20105 . . . . . 6 Poly
2220, 21cfv 5456 . . . . 5 Poly
2319, 7, 22wrex 2708 . . . 4 Poly coeffdeg
2423, 5, 3crab 2711 . . 3 Poly coeffdeg
252, 4, 24cmpt 4268 . 2 Poly coeffdeg
261, 25wceq 1653 1 IntgOver Poly coeffdeg
 Colors of variables: wff set class This definition is referenced by:  itgoval  27345  itgocn  27348
 Copyright terms: Public domain W3C validator