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 20335
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 20334 . 2 class ring
2 ccnfld 20262 . . 3 class fld
3 cz 11799 . . 3 class
4 cress 16346 . . 3 class s
52, 3, 4co 6982 . 2 class (ℂflds ℤ)
61, 5wceq 1508 1 wff ring = (ℂflds ℤ)
Colors of variables: wff setvar class
This definition is referenced by:  zringcrng  20336  zringbas  20340  zringplusg  20341  zringmulg  20342  zringmulr  20343  zring0  20344  zring1  20345  zringlpirlem1  20348  zringunit  20352  zringcyg  20355  zringmpg  20356  prmirred  20359  zndvds  20413  zringnrg  23114  zlmclm  23434  zclmncvs  23470  lgseisenlem4  25671  zringnm  30877  zringsubgval  43851
  Copyright terms: Public domain W3C validator