Definition df-zring 19638

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 19637	. 2 class ℤring
2		ccnfld 19567	. . 3 class ℂfld
3		cz 11254	. . 3 class ℤ
4		cress 15696	. . 3 class ↾s
5	2, 3, 4	co 6549	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1475	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is referenced by:  zringcrng  19639  zringbas  19643  zringplusg  19644  zringmulg  19645  zringmulr  19646  zring0  19647  zring1  19648  zringlpirlem1  19651  zringunit  19655  zringcyg  19658  zringmpg  19659  prmirred  19662  zndvds  19717  zringnrg  22399  zlmclm  22720  zclmncvs  22756  lgseisenlem4  24903  zringnm  29332  zringsubgval  41977