Definition df-zring 21406

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 21405	. 2 class ℤring
2		ccnfld 21313	. . 3 class ℂfld
3		cz 12586	. . 3 class ℤ
4		cress 17249	. . 3 class ↾s
5	2, 3, 4	co 7403	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1540	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is referenced by:  zringcrng  21407  zringbas  21412  zringplusg  21413  zringsub  21414  zringmulg  21415  zringmulr  21416  zring0  21417  zring1  21418  zringlpirlem1  21421  zringunit  21425  zringcyg  21428  zringsubgval  21429  zringmpg  21430  prmirred  21433  zndvds  21508  zringnrg  24725  zlmclm  25061  zclmncvs  25098  lgseisenlem4  27339  gsumzrsum  32999  zringnm  33935