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 21458
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 21457 . 2 class ring
2 ccnfld 21364 . . 3 class fld
3 cz 12613 . . 3 class
4 cress 17274 . . 3 class s
52, 3, 4co 7431 . 2 class (ℂflds ℤ)
61, 5wceq 1540 1 wff ring = (ℂflds ℤ)
Colors of variables: wff setvar class
This definition is referenced by:  zringcrng  21459  zringbas  21464  zringplusg  21465  zringsub  21466  zringmulg  21467  zringmulr  21468  zring0  21469  zring1  21470  zringlpirlem1  21473  zringunit  21477  zringcyg  21480  zringsubgval  21481  zringmpg  21482  prmirred  21485  zndvds  21568  zringnrg  24809  zlmclm  25145  zclmncvs  25182  lgseisenlem4  27422  gsumzrsum  33062  zringnm  33957
  Copyright terms: Public domain W3C validator