Definition df-zring 20335

Description: The (unital) ring of integers. (Contributed by Alexander van der Vekens, 9-Jun-2019.)

Assertion

Ref	Expression
df-zring	⊢ ℤring = (ℂfld ↾s ℤ)

Detailed syntax breakdown of Definition df-zring

Step	Hyp	Ref	Expression
1		zring 20334	. 2 class ℤring
2		ccnfld 20262	. . 3 class ℂfld
3		cz 11799	. . 3 class ℤ
4		cress 16346	. . 3 class ↾s
5	2, 3, 4	co 6982	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1508	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is referenced by:  zringcrng  20336  zringbas  20340  zringplusg  20341  zringmulg  20342  zringmulr  20343  zring0  20344  zring1  20345  zringlpirlem1  20348  zringunit  20352  zringcyg  20355  zringmpg  20356  prmirred  20359  zndvds  20413  zringnrg  23114  zlmclm  23434  zclmncvs  23470  lgseisenlem4  25671  zringnm  30877  zringsubgval  43851