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

Definition df-zring 18602
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 18601 . 2  classring
2 ccnfld 18533 . . 3  classfld
3 cz 10781 . . 3  class  ZZ
4 cress 14635 . . 3  classs
52, 3, 4co 6196 . 2  class  (flds  ZZ )
61, 5wceq 1399 1  wffring  =  (flds  ZZ )
Colors of variables: wff setvar class
This definition is referenced by:  zringcrng  18603  zringbas  18607  zringplusg  18608  zringmulg  18609  zringmulr  18610  zring0  18611  zring1  18612  zringlpirlem1  18615  zringcyg  18619  zringunit  18621  zringmpg  18622  prmirred  18625  zndvds  18679  zringnrg  21378  zlmclm  21680  lgseisenlem4  23744  zringnm  28094  zringsubgval  33195
  Copyright terms: Public domain W3C validator