Definition df-zring 20680

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 20679	. 2 class ℤring
2		ccnfld 20606	. . 3 class ℂfld
3		cz 12328	. . 3 class ℤ
4		cress 16950	. . 3 class ↾s
5	2, 3, 4	co 7284	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1539	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is referenced by:  zringcrng  20681  zringbas  20685  zringplusg  20686  zringmulg  20687  zringmulr  20688  zring0  20689  zring1  20690  zringlpirlem1  20693  zringunit  20697  zringcyg  20700  zringsubgval  20701  zringmpg  20702  prmirred  20705  zndvds  20766  zringnrg  23960  zlmclm  24284  zclmncvs  24321  lgseisenlem4  26535  zringnm  31917