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 20173
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 20172 . 2 class ring
2 ccnfld 20100 . . 3 class fld
3 cz 11980 . . 3 class
4 cress 16486 . . 3 class s
52, 3, 4co 7151 . 2 class (ℂflds ℤ)
61, 5wceq 1538 1 wff ring = (ℂflds ℤ)
Colors of variables: wff setvar class
This definition is referenced by:  zringcrng  20174  zringbas  20178  zringplusg  20179  zringmulg  20180  zringmulr  20181  zring0  20182  zring1  20183  zringlpirlem1  20186  zringunit  20190  zringcyg  20193  zringmpg  20194  prmirred  20197  zndvds  20250  zringnrg  23402  zlmclm  23726  zclmncvs  23762  lgseisenlem4  25971  zringnm  31286  zringsubgval  44756
  Copyright terms: Public domain W3C validator