Definition df-zring 20617

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 20616	. 2 class ℤring
2		ccnfld 20544	. . 3 class ℂfld
3		cz 11980	. . 3 class ℤ
4		cress 16483	. . 3 class ↾s
5	2, 3, 4	co 7155	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1533	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is referenced by:  zringcrng  20618  zringbas  20622  zringplusg  20623  zringmulg  20624  zringmulr  20625  zring0  20626  zring1  20627  zringlpirlem1  20630  zringunit  20634  zringcyg  20637  zringmpg  20638  prmirred  20641  zndvds  20695  zringnrg  23395  zlmclm  23715  zclmncvs  23751  lgseisenlem4  25953  zringnm  31201  zringsubgval  44448