Definition df-zring 21402

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 21401	. 2 class ℤring
2		ccnfld 21309	. . 3 class ℂfld
3		cz 12488	. . 3 class ℤ
4		cress 17157	. . 3 class ↾s
5	2, 3, 4	co 7358	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1541	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is referenced by:  zringcrng  21403  zringbas  21408  zringplusg  21409  zringsub  21410  zringmulg  21411  zringmulr  21412  zring0  21413  zring1  21414  zringlpirlem1  21417  zringunit  21421  zringcyg  21424  zringsubgval  21425  zringmpg  21426  prmirred  21429  zndvds  21504  zringnrg  24732  zlmclm  25068  zclmncvs  25104  lgseisenlem4  27345  gsumzrsum  33148  zringnm  34115