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

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

Detailed syntax breakdown of Definition df-zp
StepHypRef Expression
1 czp 33607 . 2 class Zp
2 czr 33601 . . 3 class ZRing
3 cqp 33606 . . 3 class Qp
42, 3ccom 5594 . 2 class (ZRing ∘ Qp)
51, 4wceq 1542 1 wff Zp = (ZRing ∘ Qp)
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator