Definition df-zring 19819

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		zring 19818	. 2 class ℤring
2		ccnfld 19746	. . 3 class ℂfld
3		cz 11377	. . 3 class ℤ
4		cress 15858	. . 3 class ↾s
5	2, 3, 4	co 6650	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1483	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is referenced by:  zringcrng  19820  zringbas  19824  zringplusg  19825  zringmulg  19826  zringmulr  19827  zring0  19828  zring1  19829  zringlpirlem1  19832  zringunit  19836  zringcyg  19839  zringmpg  19840  prmirred  19843  zndvds  19898  zringnrg  22591  zlmclm  22912  zclmncvs  22948  lgseisenlem4  25103  zringnm  30004  zringsubgval  42183