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 ∘ Qp )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		czp	⊢ Zp
1		czr	⊢ ZRing
2		cqp	⊢ Qp
3	1 2	ccom	⊢ ( ZRing ∘ Qp )
4	0 3	wceq	⊢ Zp = ( ZRing ∘ Qp )