Database
BASIC ALGEBRAIC STRUCTURES
The complex numbers as an algebraic extensible structure
Ring of integers
zring
Next ⟩
df-zring
Metamath Proof Explorer
Ascii
Structured
Syntax definition
zring
Description:
Extend class notation with the (unital) ring of integers.
Ref
Expression
Assertion
zring
class
ℤ
_{ring}