Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-gfoo Structured version   Unicode version

Definition df-gfoo 25090
 Description: Define the Galois field of order , as a direct limit of the Galois finite fields. (Contributed by Mario Carneiro, 2-Dec-2014.)
Assertion
Ref Expression
df-gfoo GF ℤ/n polySplitLim Poly1 var1 .gmulGrp
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-gfoo
StepHypRef Expression
1 cgfo 25081 . 2 GF
2 vp . . 3
3 cprime 13080 . . 3
4 vr . . . 4
52cv 1652 . . . . 5
6 czn 16782 . . . . 5 ℤ/n
75, 6cfv 5455 . . . 4 ℤ/n
84cv 1652 . . . . 5
9 vn . . . . . 6
10 cn 10001 . . . . . 6
11 vs . . . . . . . 8
12 cpl1 16572 . . . . . . . . 9 Poly1
138, 12cfv 5455 . . . . . . . 8 Poly1
14 vx . . . . . . . . 9
15 cv1 16571 . . . . . . . . . 10 var1
168, 15cfv 5455 . . . . . . . . 9 var1
179cv 1652 . . . . . . . . . . . 12
18 cexp 11383 . . . . . . . . . . . 12
195, 17, 18co 6082 . . . . . . . . . . 11
2014cv 1652 . . . . . . . . . . 11
2111cv 1652 . . . . . . . . . . . . 13
22 cmgp 15649 . . . . . . . . . . . . 13 mulGrp
2321, 22cfv 5455 . . . . . . . . . . . 12 mulGrp
24 cmg 14690 . . . . . . . . . . . 12 .g
2523, 24cfv 5455 . . . . . . . . . . 11 .gmulGrp
2619, 20, 25co 6082 . . . . . . . . . 10 .gmulGrp
27 csg 14689 . . . . . . . . . . 11
2821, 27cfv 5455 . . . . . . . . . 10
2926, 20, 28co 6082 . . . . . . . . 9 .gmulGrp
3014, 16, 29csb 3252 . . . . . . . 8 var1 .gmulGrp
3111, 13, 30csb 3252 . . . . . . 7 Poly1 var1 .gmulGrp
3231csn 3815 . . . . . 6 Poly1 var1 .gmulGrp
339, 10, 32cmpt 4267 . . . . 5 Poly1 var1 .gmulGrp
34 cpsl 25070 . . . . 5 polySplitLim
358, 33, 34co 6082 . . . 4 polySplitLim Poly1 var1 .gmulGrp
364, 7, 35csb 3252 . . 3 ℤ/n polySplitLim Poly1 var1 .gmulGrp
372, 3, 36cmpt 4267 . 2 ℤ/n polySplitLim Poly1 var1 .gmulGrp
381, 37wceq 1653 1 GF ℤ/n polySplitLim Poly1 var1 .gmulGrp
 Colors of variables: wff set class
 Copyright terms: Public domain W3C validator