Definition df-zring 21018

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 21017	. 2 class ℤring
2		ccnfld 20944	. . 3 class ℂfld
3		cz 12558	. . 3 class ℤ
4		cress 17173	. . 3 class ↾s
5	2, 3, 4	co 7409	. 2 class (ℂfld ↾s ℤ)
6	1, 5	wceq 1542	1 wff ℤring = (ℂfld ↾s ℤ)

This definition is referenced by:  zringcrng  21019  zringbas  21023  zringplusg  21024  zringsub  21025  zringmulg  21026  zringmulr  21027  zring0  21028  zring1  21029  zringlpirlem1  21032  zringunit  21036  zringcyg  21039  zringsubgval  21040  zringmpg  21041  prmirred  21044  zndvds  21105  zringnrg  24304  zlmclm  24628  zclmncvs  24665  lgseisenlem4  26881  zringnm  32938