Definition df-zring 21414

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		czring 21413	. 2 class ℤring
2		ccnfld 21321	. . 3 class ℂfld
3		cz 12500	. . 3 class ℤ
4		cress 17169	. . 3 class ↾s
5	2, 3, 4	co 7368	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1542	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is referenced by:  zringcrng  21415  zringbas  21420  zringplusg  21421  zringsub  21422  zringmulg  21423  zringmulr  21424  zring0  21425  zring1  21426  zringlpirlem1  21429  zringunit  21433  zringcyg  21436  zringsubgval  21437  zringmpg  21438  prmirred  21441  zndvds  21516  zringnrg  24744  zlmclm  25080  zclmncvs  25116  lgseisenlem4  27357  gsumzrsum  33158  zringnm  34135