Definition df-zring 21354

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 21353	. 2 class ℤring
2		ccnfld 21261	. . 3 class ℂfld
3		cz 12471	. . 3 class ℤ
4		cress 17141	. . 3 class ↾s
5	2, 3, 4	co 7349	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1540	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is referenced by:  zringcrng  21355  zringbas  21360  zringplusg  21361  zringsub  21362  zringmulg  21363  zringmulr  21364  zring0  21365  zring1  21366  zringlpirlem1  21369  zringunit  21373  zringcyg  21376  zringsubgval  21377  zringmpg  21378  prmirred  21381  zndvds  21456  zringnrg  24674  zlmclm  25010  zclmncvs  25046  lgseisenlem4  27287  gsumzrsum  33013  zringnm  33931