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

Definition df-zp 25085
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 25076 . 2  class Zp
2 czr 25070 . . 3  class ZRing
3 cqp 25075 . . 3  class Qp
42, 3ccom 4874 . 2  class  (ZRing  o. Qp )
51, 4wceq 1652 1  wff Zp  =  (ZRing 
o. Qp )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator