Definition df-zring 20164

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 20163	. 2 class ℤring
2		ccnfld 20091	. . 3 class ℂfld
3		cz 11969	. . 3 class ℤ
4		cress 16476	. . 3 class ↾s
5	2, 3, 4	co 7135	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1538	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is referenced by:  zringcrng  20165  zringbas  20169  zringplusg  20170  zringmulg  20171  zringmulr  20172  zring0  20173  zring1  20174  zringlpirlem1  20177  zringunit  20181  zringcyg  20184  zringmpg  20185  prmirred  20188  zndvds  20241  zringnrg  23393  zlmclm  23717  zclmncvs  23753  lgseisenlem4  25962  zringnm  31311  zringsubgval  44803