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

Definition df-zring 18363
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 18362 . 2  classring
2 ccnfld 18294 . . 3  classfld
3 cz 10870 . . 3  class  ZZ
4 cress 14510 . . 3  classs
52, 3, 4co 6281 . 2  class  (flds  ZZ )
61, 5wceq 1383 1  wffring  =  (flds  ZZ )
Colors of variables: wff setvar class
This definition is referenced by:  zringcrng  18364  zringbas  18368  zringplusg  18369  zringmulg  18370  zringmulr  18371  zring0  18372  zring1  18373  zringlpirlem1  18382  zringcyg  18386  zringunit  18393  zringmpg  18395  prmirred  18398  zndvds  18461  zringnrg  21166  zlmclm  21468  lgseisenlem4  23499  zringnm  27813  zringsubgval  32730
  Copyright terms: Public domain W3C validator