Definition df-zring 21024

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 21023	. 2 class ℤring
2		ccnfld 20950	. . 3 class ℂfld
3		cz 12560	. . 3 class ℤ
4		cress 17175	. . 3 class ↾s
5	2, 3, 4	co 7411	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1541	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is referenced by:  zringcrng  21025  zringbas  21029  zringplusg  21030  zringsub  21031  zringmulg  21032  zringmulr  21033  zring0  21034  zring1  21035  zringlpirlem1  21038  zringunit  21042  zringcyg  21045  zringsubgval  21046  zringmpg  21047  prmirred  21050  zndvds  21111  zringnrg  24311  zlmclm  24635  zclmncvs  24672  lgseisenlem4  26888  zringnm  33007