Definition df-zring 21477

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 21476	. 2 class ℤring
2		ccnfld 21402	. . 3 class ℂfld
3		cz 12563	. . 3 class ℤ
4		cress 17247	. . 3 class ↾s
5	2, 3, 4	co 7390	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1559	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is referenced by:  zringcrng  21478  zringbas  21483  zringplusg  21484  zringsub  21485  zringmulg  21486  zringmulr  21487  zring0  21488  zring1  21489  zringlpirlem1  21492  zringunit  21496  zringcyg  21499  zringsubgval  21500  zringmpg  21501  prmirred  21504  zndvds  21579  zringnrg  24826  zlmclm  25152  zclmncvs  25188  lgseisenlem4  27417  gsumzrsum  33204  zringnm  34214