Definition df-zring 21797

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 21796	. 2 class ℤring
2		ccnfld 21720	. . 3 class ℂfld
3		cz 12731	. . 3 class ℤ
4		cress 17449	. . 3 class ↾s
5	2, 3, 4	co 7449	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1570	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is used by:  zringcrng  21798  zringbas  21803  zringplusg  21804  zringsub  21805  zringmulg  21806  zringmulr  21807  zring0  21808  zring1  21809  zringlpirlem1  21812  zringunit  21816  zringcyg  21819  zringsubgval  21820  zringmpg  21821  prmirred  21824  zndvds  21899  zringnrg  25151  zlmclm  25477  zclmncvs  25513  lgseisenlem4  27751  gsumzrsum  33715  zringnm  34694