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

Definition df-zring 17887
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 17886 . 2  classring
2 ccnfld 17821 . . 3  classfld
3 cz 10649 . . 3  class  ZZ
4 cress 14178 . . 3  classs
52, 3, 4co 6094 . 2  class  (flds  ZZ )
61, 5wceq 1369 1  wffring  =  (flds  ZZ )
Colors of variables: wff setvar class
This definition is referenced by:  zringcrng  17888  zringbas  17892  zringplusg  17893  zringmulg  17894  zringmulr  17895  zring0  17896  zring1  17897  zringlpirlem1  17906  zringcyg  17910  zringunit  17917  zringmpg  17919  prmirred  17922  zndvds  17985  zringnrg  20368  zlmclm  20670  lgseisenlem4  22694  zringnm  26391  zringsubgval  30858
  Copyright terms: Public domain W3C validator