Definition df-zring 20777

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 20776	. 2 class ℤring
2		ccnfld 20703	. . 3 class ℂfld
3		cz 12420	. . 3 class ℤ
4		cress 17038	. . 3 class ↾s
5	2, 3, 4	co 7337	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1540	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is referenced by:  zringcrng  20778  zringbas  20782  zringplusg  20783  zringmulg  20784  zringmulr  20785  zring0  20786  zring1  20787  zringlpirlem1  20790  zringunit  20794  zringcyg  20797  zringsubgval  20798  zringmpg  20799  prmirred  20802  zndvds  20863  zringnrg  24057  zlmclm  24381  zclmncvs  24418  lgseisenlem4  26632  zringnm  32206