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

Definition df-zring 18250
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 18249 . 2  classring
2 ccnfld 18184 . . 3  classfld
3 cz 10853 . . 3  class  ZZ
4 cress 14480 . . 3  classs
52, 3, 4co 6275 . 2  class  (flds  ZZ )
61, 5wceq 1374 1  wffring  =  (flds  ZZ )
Colors of variables: wff setvar class
This definition is referenced by:  zringcrng  18251  zringbas  18255  zringplusg  18256  zringmulg  18257  zringmulr  18258  zring0  18259  zring1  18260  zringlpirlem1  18269  zringcyg  18273  zringunit  18280  zringmpg  18282  prmirred  18285  zndvds  18348  zringnrg  21021  zlmclm  21323  lgseisenlem4  23348  zringnm  27562  zringsubgval  31943
  Copyright terms: Public domain W3C validator