Nearby theorems
|
|
Mathbox for Mario Carneiro |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > Mathboxes > df-zp | Structured version Visualization version Unicode version | ||
Description: Define the  -adic integers, as a subset
of the -adic
rationals. (Contributed by Mario Carneiro,
2-Dec-2014.) |
| Ref | Expression |
|---|---|
| df-zp |
 Zp   ZRing  Qp |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | czp 31545 |
. 2
Zp | |
| 2 | czr 31538 |
. . 3
ZRing | |
| 3 | cqp 31543 |
. . 3
Qp | |
| 4 | 2, 3 | ccom 5118 |
. 2
ZRing Qp |
| 5 | 1, 4 | wceq 1483 |
1
 Zp ZRing Qp |
| Colors of variables: wff setvar class |
| This definition is referenced by: (None) |
| Copyright terms: Public domain | W3C validator |