Definition df-zring 21382

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 21381	. 2 class ℤring
2		ccnfld 21289	. . 3 class ℂfld
3		cz 12465	. . 3 class ℤ
4		cress 17138	. . 3 class ↾s
5	2, 3, 4	co 7346	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1541	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is referenced by:  zringcrng  21383  zringbas  21388  zringplusg  21389  zringsub  21390  zringmulg  21391  zringmulr  21392  zring0  21393  zring1  21394  zringlpirlem1  21397  zringunit  21401  zringcyg  21404  zringsubgval  21405  zringmpg  21406  prmirred  21409  zndvds  21484  zringnrg  24701  zlmclm  25037  zclmncvs  25073  lgseisenlem4  27314  gsumzrsum  33034  zringnm  33966