Definition df-zring 21481

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 21480	. 2 class ℤring
2		ccnfld 21387	. . 3 class ℂfld
3		cz 12639	. . 3 class ℤ
4		cress 17287	. . 3 class ↾s
5	2, 3, 4	co 7448	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1537	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is referenced by:  zringcrng  21482  zringbas  21487  zringplusg  21488  zringsub  21489  zringmulg  21490  zringmulr  21491  zring0  21492  zring1  21493  zringlpirlem1  21496  zringunit  21500  zringcyg  21503  zringsubgval  21504  zringmpg  21505  prmirred  21508  zndvds  21591  zringnrg  24829  zlmclm  25164  zclmncvs  25201  lgseisenlem4  27440  zringnm  33904