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

Definition df-zring 17843
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 17842 . 2  classring
2 ccnfld 17777 . . 3  classfld
3 cz 10642 . . 3  class  ZZ
4 cress 14171 . . 3  classs
52, 3, 4co 6090 . 2  class  (flds  ZZ )
61, 5wceq 1364 1  wffring  =  (flds  ZZ )
Colors of variables: wff setvar class
This definition is referenced by:  zringcrng  17844  zringbas  17848  zringplusg  17849  zringmulg  17850  zringmulr  17851  zring0  17852  zring1  17853  zringlpirlem1  17862  zringcyg  17866  zringunit  17873  zringmpg  17875  prmirred  17878  zndvds  17941  zringnrg  20324  zlmclm  20626  lgseisenlem4  22650  zringnm  26324  zringsubgval  30740
  Copyright terms: Public domain W3C validator