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

Definition df-zring 21475
Description: The (unital) ring of integers. (Contributed by Alexander van der Vekens, 9-Jun-2019.)
Assertion
Ref Expression
df-zring ring = (ℂflds ℤ)

Detailed syntax breakdown of Definition df-zring
StepHypRef Expression
1 czring 21474 . 2 class ring
2 ccnfld 21381 . . 3 class fld
3 cz 12610 . . 3 class
4 cress 17273 . . 3 class s
52, 3, 4co 7430 . 2 class (ℂflds ℤ)
61, 5wceq 1536 1 wff ring = (ℂflds ℤ)
Colors of variables: wff setvar class
This definition is referenced by:  zringcrng  21476  zringbas  21481  zringplusg  21482  zringsub  21483  zringmulg  21484  zringmulr  21485  zring0  21486  zring1  21487  zringlpirlem1  21490  zringunit  21494  zringcyg  21497  zringsubgval  21498  zringmpg  21499  prmirred  21502  zndvds  21585  zringnrg  24823  zlmclm  25158  zclmncvs  25195  lgseisenlem4  27436  gsumzrsum  33044  zringnm  33918
  Copyright terms: Public domain W3C validator