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

Definition df-qpa 25094
 Description: Define the completion of the -adic rationals. Here we simply define it as the splitting field of a dense sequence of polynomials (using as the -th set the collection of polynomials with degree less than and with coefficients ). Krasner's lemma will then show that all monic polynomials have splitting fields isomorphic to a sufficiently close Eisenstein polynomial from the list, and unramified extensions are generated by the polynomial , which is in the list. Thus, every finite extension of Qp is a subfield of this field extension, so it is algebraically closed. (Contributed by Mario Carneiro, 2-Dec-2014.)
Assertion
Ref Expression
df-qpa _Qp Qp polySplitLim Poly1 deg1 coe1
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-qpa
StepHypRef Expression
1 cqpa 25085 . 2 _Qp
2 vp . . 3
3 cprime 13079 . . 3
4 vr . . . 4
52cv 1651 . . . . 5
6 cqp 25083 . . . . 5 Qp
75, 6cfv 5454 . . . 4 Qp
84cv 1651 . . . . 5
9 vn . . . . . 6
10 cn 10000 . . . . . 6
11 vf . . . . . . . . . . 11
1211cv 1651 . . . . . . . . . 10
13 cdg1 19977 . . . . . . . . . 10 deg1
148, 12, 13co 6081 . . . . . . . . 9 deg1
159cv 1651 . . . . . . . . 9
16 cle 9121 . . . . . . . . 9
1714, 15, 16wbr 4212 . . . . . . . 8 deg1
18 vd . . . . . . . . . . . . 13
1918cv 1651 . . . . . . . . . . . 12
2019ccnv 4877 . . . . . . . . . . 11
21 cz 10282 . . . . . . . . . . . 12
22 cc0 8990 . . . . . . . . . . . . 13
2322csn 3814 . . . . . . . . . . . 12
2421, 23cdif 3317 . . . . . . . . . . 11
2520, 24cima 4881 . . . . . . . . . 10
26 cfz 11043 . . . . . . . . . . 11
2722, 15, 26co 6081 . . . . . . . . . 10
2825, 27wss 3320 . . . . . . . . 9
29 cco1 16574 . . . . . . . . . . 11 coe1
3012, 29cfv 5454 . . . . . . . . . 10 coe1
3130crn 4879 . . . . . . . . 9 coe1
3228, 18, 31wral 2705 . . . . . . . 8 coe1
3317, 32wa 359 . . . . . . 7 deg1 coe1
34 cpl1 16571 . . . . . . . 8 Poly1
358, 34cfv 5454 . . . . . . 7 Poly1
3633, 11, 35crab 2709 . . . . . 6 Poly1 deg1 coe1
379, 10, 36cmpt 4266 . . . . 5 Poly1 deg1 coe1
38 cpsl 25069 . . . . 5 polySplitLim
398, 37, 38co 6081 . . . 4 polySplitLim Poly1 deg1 coe1
404, 7, 39csb 3251 . . 3 Qp polySplitLim Poly1 deg1 coe1
412, 3, 40cmpt 4266 . 2 Qp polySplitLim Poly1 deg1 coe1
421, 41wceq 1652 1 _Qp Qp polySplitLim Poly1 deg1 coe1
 Colors of variables: wff set class
 Copyright terms: Public domain W3C validator