Definition df-zring 21427

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 21426	. 2 class ℤring
2		ccnfld 21352	. . 3 class ℂfld
3		cz 12524	. . 3 class ℤ
4		cress 17200	. . 3 class ↾s
5	2, 3, 4	co 7367	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1542	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is referenced by:  zringcrng  21428  zringbas  21433  zringplusg  21434  zringsub  21435  zringmulg  21436  zringmulr  21437  zring0  21438  zring1  21439  zringlpirlem1  21442  zringunit  21446  zringcyg  21449  zringsubgval  21450  zringmpg  21451  prmirred  21454  zndvds  21529  zringnrg  24753  zlmclm  25079  zclmncvs  25115  lgseisenlem4  27341  gsumzrsum  33126  zringnm  34102