Definition df-zring 21437

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 21436	. 2 class ℤring
2		ccnfld 21344	. . 3 class ℂfld
3		cz 12515	. . 3 class ℤ
4		cress 17191	. . 3 class ↾s
5	2, 3, 4	co 7360	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1542	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is referenced by:  zringcrng  21438  zringbas  21443  zringplusg  21444  zringsub  21445  zringmulg  21446  zringmulr  21447  zring0  21448  zring1  21449  zringlpirlem1  21452  zringunit  21456  zringcyg  21459  zringsubgval  21460  zringmpg  21461  prmirred  21464  zndvds  21539  zringnrg  24763  zlmclm  25089  zclmncvs  25125  lgseisenlem4  27355  gsumzrsum  33141  zringnm  34118