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 20548
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 20547 . 2 class ring
2 ccnfld 20475 . . 3 class fld
3 cz 11970 . . 3 class
4 cress 16474 . . 3 class s
52, 3, 4co 7145 . 2 class (ℂflds ℤ)
61, 5wceq 1528 1 wff ring = (ℂflds ℤ)
Colors of variables: wff setvar class
This definition is referenced by:  zringcrng  20549  zringbas  20553  zringplusg  20554  zringmulg  20555  zringmulr  20556  zring0  20557  zring1  20558  zringlpirlem1  20561  zringunit  20565  zringcyg  20568  zringmpg  20569  prmirred  20572  zndvds  20626  zringnrg  23325  zlmclm  23645  zclmncvs  23681  lgseisenlem4  25882  zringnm  31101  zringsubgval  44347
  Copyright terms: Public domain W3C validator