Definition df-zring 21479

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 21478	. 2 class ℤring
2		ccnfld 21404	. . 3 class ℂfld
3		cz 12565	. . 3 class ℤ
4		cress 17249	. . 3 class ↾s
5	2, 3, 4	co 7392	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1559	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is referenced by:  zringcrng  21480  zringbas  21485  zringplusg  21486  zringsub  21487  zringmulg  21488  zringmulr  21489  zring0  21490  zring1  21491  zringlpirlem1  21494  zringunit  21498  zringcyg  21501  zringsubgval  21502  zringmpg  21503  prmirred  21506  zndvds  21581  zringnrg  24828  zlmclm  25154  zclmncvs  25190  lgseisenlem4  27419  gsumzrsum  33206  zringnm  34216