Definition df-zring 20583

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 20582	. 2 class ℤring
2		ccnfld 20510	. . 3 class ℂfld
3		cz 12249	. . 3 class ℤ
4		cress 16867	. . 3 class ↾s
5	2, 3, 4	co 7255	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1539	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is referenced by:  zringcrng  20584  zringbas  20588  zringplusg  20589  zringmulg  20590  zringmulr  20591  zring0  20592  zring1  20593  zringlpirlem1  20596  zringunit  20600  zringcyg  20603  zringsubgval  20604  zringmpg  20605  prmirred  20608  zndvds  20669  zringnrg  23857  zlmclm  24181  zclmncvs  24217  lgseisenlem4  26431  zringnm  31810