Definition df-zring 21357

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 21356	. 2 class ℤring
2		ccnfld 21264	. . 3 class ℂfld
3		cz 12529	. . 3 class ℤ
4		cress 17200	. . 3 class ↾s
5	2, 3, 4	co 7387	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1540	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is referenced by:  zringcrng  21358  zringbas  21363  zringplusg  21364  zringsub  21365  zringmulg  21366  zringmulr  21367  zring0  21368  zring1  21369  zringlpirlem1  21372  zringunit  21376  zringcyg  21379  zringsubgval  21380  zringmpg  21381  prmirred  21384  zndvds  21459  zringnrg  24676  zlmclm  25012  zclmncvs  25048  lgseisenlem4  27289  gsumzrsum  32999  zringnm  33948