Definition df-zring 21578

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 21577	. 2 class ℤring
2		ccnfld 21503	. . 3 class ℂfld
3		cz 12592	. . 3 class ℤ
4		cress 17291	. . 3 class ↾s
5	2, 3, 4	co 7412	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1570	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is referenced by:  zringcrng  21579  zringbas  21584  zringplusg  21585  zringsub  21586  zringmulg  21587  zringmulr  21588  zring0  21589  zring1  21590  zringlpirlem1  21593  zringunit  21597  zringcyg  21600  zringsubgval  21601  zringmpg  21602  prmirred  21605  zndvds  21680  zringnrg  24926  zlmclm  25252  zclmncvs  25288  lgseisenlem4  27523  gsumzrsum  33366  zringnm  34329