Definition df-zring 20907

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 20906	. 2 class ℤring
2		ccnfld 20833	. . 3 class ℂfld
3		cz 12508	. . 3 class ℤ
4		cress 17123	. . 3 class ↾s
5	2, 3, 4	co 7362	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1541	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is referenced by:  zringcrng  20908  zringbas  20912  zringplusg  20913  zringmulg  20914  zringmulr  20915  zring0  20916  zring1  20917  zringlpirlem1  20920  zringunit  20924  zringcyg  20927  zringsubgval  20928  zringmpg  20929  prmirred  20932  zndvds  20993  zringnrg  24188  zlmclm  24512  zclmncvs  24549  lgseisenlem4  26763  zringnm  32628