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 19867
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 zring 19866 . 2 class ring
2 ccnfld 19794 . . 3 class fld
3 cz 11415 . . 3 class
4 cress 15905 . . 3 class s
52, 3, 4co 6690 . 2 class (ℂflds ℤ)
61, 5wceq 1523 1 wff ring = (ℂflds ℤ)
Colors of variables: wff setvar class
This definition is referenced by:  zringcrng  19868  zringbas  19872  zringplusg  19873  zringmulg  19874  zringmulr  19875  zring0  19876  zring1  19877  zringlpirlem1  19880  zringunit  19884  zringcyg  19887  zringmpg  19888  prmirred  19891  zndvds  19946  zringnrg  22638  zlmclm  22958  zclmncvs  22994  lgseisenlem4  25148  zringnm  30132  zringsubgval  42508
  Copyright terms: Public domain W3C validator