Definition df-zring 21429

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 21428	. 2 class ℤring
2		ccnfld 21354	. . 3 class ℂfld
3		cz 12522	. . 3 class ℤ
4		cress 17198	. . 3 class ↾s
5	2, 3, 4	co 7363	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1547	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is referenced by:  zringcrng  21430  zringbas  21435  zringplusg  21436  zringsub  21437  zringmulg  21438  zringmulr  21439  zring0  21440  zring1  21441  zringlpirlem1  21444  zringunit  21448  zringcyg  21451  zringsubgval  21452  zringmpg  21453  prmirred  21456  zndvds  21531  zringnrg  24778  zlmclm  25104  zclmncvs  25140  lgseisenlem4  27366  gsumzrsum  33153  zringnm  34149