Definition df-zring 21634

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 21633	. 2 class ℤring
2		ccnfld 21559	. . 3 class ℂfld
3		cz 12609	. . 3 class ℤ
4		cress 17315	. . 3 class ↾s
5	2, 3, 4	co 7423	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1570	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is used by:  zringcrng  21635  zringbas  21640  zringplusg  21641  zringsub  21642  zringmulg  21643  zringmulr  21644  zring0  21645  zring1  21646  zringlpirlem1  21649  zringunit  21653  zringcyg  21656  zringsubgval  21657  zringmpg  21658  prmirred  21661  zndvds  21736  zringnrg  24982  zlmclm  25308  zclmncvs  25344  lgseisenlem4  27579  gsumzrsum  33416  zringnm  34379