Definition df-zring 20047

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 20046	. 2 class ℤring
2		ccnfld 19974	. . 3 class ℂfld
3		cz 11663	. . 3 class ℤ
4		cress 16089	. . 3 class ↾s
5	2, 3, 4	co 6884	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1637	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is referenced by:  zringcrng  20048  zringbas  20052  zringplusg  20053  zringmulg  20054  zringmulr  20055  zring0  20056  zring1  20057  zringlpirlem1  20060  zringunit  20064  zringcyg  20067  zringmpg  20068  prmirred  20071  zndvds  20125  zringnrg  22825  zlmclm  23145  zclmncvs  23181  lgseisenlem4  25340  zringnm  30352  zringsubgval  42769