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 21430
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 21429 . 2 class ring
2 ccnfld 21336 . . 3 class fld
3 cz 12601 . . 3 class
4 cress 17234 . . 3 class s
52, 3, 4co 7413 . 2 class (ℂflds ℤ)
61, 5wceq 1534 1 wff ring = (ℂflds ℤ)
Colors of variables: wff setvar class
This definition is referenced by:  zringcrng  21431  zringbas  21436  zringplusg  21437  zringsub  21438  zringmulg  21439  zringmulr  21440  zring0  21441  zring1  21442  zringlpirlem1  21445  zringunit  21449  zringcyg  21452  zringsubgval  21453  zringmpg  21454  prmirred  21457  zndvds  21540  zringnrg  24789  zlmclm  25124  zclmncvs  25161  lgseisenlem4  27401  zringnm  33783
  Copyright terms: Public domain W3C validator