Definition df-zring 21386

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 21385	. 2 class ℤring
2		ccnfld 21293	. . 3 class ℂfld
3		cz 12475	. . 3 class ℤ
4		cress 17143	. . 3 class ↾s
5	2, 3, 4	co 7352	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1541	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is referenced by:  zringcrng  21387  zringbas  21392  zringplusg  21393  zringsub  21394  zringmulg  21395  zringmulr  21396  zring0  21397  zring1  21398  zringlpirlem1  21401  zringunit  21405  zringcyg  21408  zringsubgval  21409  zringmpg  21410  prmirred  21413  zndvds  21488  zringnrg  24704  zlmclm  25040  zclmncvs  25076  lgseisenlem4  27317  gsumzrsum  33046  zringnm  33992