Definition df-zring 20618

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 20617	. 2 class ℤring
2		ccnfld 20545	. . 3 class ℂfld
3		cz 11982	. . 3 class ℤ
4		cress 16484	. . 3 class ↾s
5	2, 3, 4	co 7156	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1537	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is referenced by:  zringcrng  20619  zringbas  20623  zringplusg  20624  zringmulg  20625  zringmulr  20626  zring0  20627  zring1  20628  zringlpirlem1  20631  zringunit  20635  zringcyg  20638  zringmpg  20639  prmirred  20642  zndvds  20696  zringnrg  23396  zlmclm  23716  zclmncvs  23752  lgseisenlem4  25954  zringnm  31201  zringsubgval  44469