Definition df-zring 21364

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 21363	. 2 class ℤring
2		ccnfld 21271	. . 3 class ℂfld
3		cz 12536	. . 3 class ℤ
4		cress 17207	. . 3 class ↾s
5	2, 3, 4	co 7390	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1540	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is referenced by:  zringcrng  21365  zringbas  21370  zringplusg  21371  zringsub  21372  zringmulg  21373  zringmulr  21374  zring0  21375  zring1  21376  zringlpirlem1  21379  zringunit  21383  zringcyg  21386  zringsubgval  21387  zringmpg  21388  prmirred  21391  zndvds  21466  zringnrg  24683  zlmclm  25019  zclmncvs  25055  lgseisenlem4  27296  gsumzrsum  33006  zringnm  33955