Definition df-zring 21666

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 21665	. 2 class ℤring
2		ccnfld 21591	. . 3 class ℂfld
3		cz 12619	. . 3 class ℤ
4		cress 17328	. . 3 class ↾s
5	2, 3, 4	co 7417	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1570	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is used by:  zringcrng  21667  zringbas  21672  zringplusg  21673  zringsub  21674  zringmulg  21675  zringmulr  21676  zring0  21677  zring1  21678  zringlpirlem1  21681  zringunit  21685  zringcyg  21688  zringsubgval  21689  zringmpg  21690  prmirred  21693  zndvds  21768  zringnrg  25020  zlmclm  25346  zclmncvs  25382  lgseisenlem4  27622  gsumzrsum  33513  zringnm  34476