Definition df-zring 21372

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 21371	. 2 class ℤring
2		ccnfld 21279	. . 3 class ℂfld
3		cz 12489	. . 3 class ℤ
4		cress 17159	. . 3 class ↾s
5	2, 3, 4	co 7353	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1540	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is referenced by:  zringcrng  21373  zringbas  21378  zringplusg  21379  zringsub  21380  zringmulg  21381  zringmulr  21382  zring0  21383  zring1  21384  zringlpirlem1  21387  zringunit  21391  zringcyg  21394  zringsubgval  21395  zringmpg  21396  prmirred  21399  zndvds  21474  zringnrg  24692  zlmclm  25028  zclmncvs  25064  lgseisenlem4  27305  gsumzrsum  33025  zringnm  33924