Definition df-zring 21733

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 21732	. 2 class ℤring
2		ccnfld 21658	. . 3 class ℂfld
3		cz 12674	. . 3 class ℤ
4		cress 17388	. . 3 class ↾s
5	2, 3, 4	co 7412	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1570	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is used by:  zringcrng  21734  zringbas  21739  zringplusg  21740  zringsub  21741  zringmulg  21742  zringmulr  21743  zring0  21744  zring1  21745  zringlpirlem1  21748  zringunit  21752  zringcyg  21755  zringsubgval  21756  zringmpg  21757  prmirred  21760  zndvds  21835  zringnrg  25087  zlmclm  25413  zclmncvs  25449  lgseisenlem4  27687  gsumzrsum  33608  zringnm  34572