MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-zring Structured version   Unicode version

Definition df-zring 19036
Description: The (unital) ring of integers. (Contributed by Alexander van der Vekens, 9-Jun-2019.)
Assertion
Ref Expression
df-zring  |-ring  =  (flds  ZZ )

Detailed syntax breakdown of Definition df-zring
StepHypRef Expression
1 zring 19035 . 2  classring
2 ccnfld 18967 . . 3  classfld
3 cz 10943 . . 3  class  ZZ
4 cress 15119 . . 3  classs
52, 3, 4co 6304 . 2  class  (flds  ZZ )
61, 5wceq 1438 1  wffring  =  (flds  ZZ )
Colors of variables: wff setvar class
This definition is referenced by:  zringcrng  19037  zringbas  19041  zringplusg  19042  zringmulg  19043  zringmulr  19044  zring0  19045  zring1  19046  zringlpirlem1  19049  zringcyg  19056  zringunit  19058  zringmpg  19059  prmirred  19062  zndvds  19116  zringnrg  21802  zlmclm  22122  lgseisenlem4  24276  zringnm  28770  zringsubgval  39581
  Copyright terms: Public domain W3C validator