Metamath Proof Explorer

Syntax definition czn

Description: The ring of integers modulo n .

Ref Expression
Assertion czn 
class Z/nZ