Metamath Proof Explorer

Definition df-zp

Description: Define the p -adic integers, as a subset of the p -adic rationals. (Contributed by Mario Carneiro, 2-Dec-2014)

Ref Expression
Assertion df-zp 
|- Zp = ( ZRing o. Qp )

Detailed syntax breakdown

Step Hyp Ref Expression
0 czp 
 |-  Zp
1 czr 
 |-  ZRing
2 cqp 
 |-  Qp
3 1 2 ccom 
 |-  ( ZRing o. Qp )
4 0 3 wceq 
 |-  Zp = ( ZRing o. Qp )