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

Definition df-zp 24004
Description: Define the  p-adic integers, as a subset of the  p-adic rationals. (Contributed by Mario Carneiro, 2-Dec-2014.)
Assertion
Ref Expression
df-zp  |- Zp  =  (ZRing 
o. Qp )

Detailed syntax breakdown of Definition df-zp
StepHypRef Expression
1 czp 23995 . 2  class Zp
2 czr 23989 . . 3  class ZRing
3 cqp 23994 . . 3  class Qp
42, 3ccom 4709 . 2  class  (ZRing  o. Qp )
51, 4wceq 1632 1  wff Zp  =  (ZRing 
o. Qp )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator