Definition df-zring 21759

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 21758	. 2 class ℤring
2		ccnfld 21684	. . 3 class ℂfld
3		cz 12697	. . 3 class ℤ
4		cress 17414	. . 3 class ↾s
5	2, 3, 4	co 7421	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1569	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is used by:  zringcrng  21760  zringbas  21765  zringplusg  21766  zringsub  21767  zringmulg  21768  zringmulr  21769  zring0  21770  zring1  21771  zringlpirlem1  21774  zringunit  21778  zringcyg  21781  zringsubgval  21782  zringmpg  21783  prmirred  21786  zndvds  21861  zringnrg  25113  zlmclm  25439  zclmncvs  25475  lgseisenlem4  27711  gsumzrsum  33673  zringnm  34637