Metamath Proof Explorer


Syntax definition czp

Description: The set of p -adic integers. (Not to be confused with czn .)

Ref Expression
Assertion czp class p