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 p = ℤRing p

Detailed syntax breakdown

Step Hyp Ref Expression
0 czp class p
1 czr class ℤRing
2 cqp class p
3 1 2 ccom class ℤRing p
4 0 3 wceq wff p = ℤRing p