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 19587
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 19586 . 2 class ring
2 ccnfld 19516 . . 3 class fld
3 cz 11213 . . 3 class
4 cress 15645 . . 3 class s
52, 3, 4co 6527 . 2 class (ℂflds ℤ)
61, 5wceq 1474 1 wff ring = (ℂflds ℤ)
Colors of variables: wff setvar class
This definition is referenced by:  zringcrng  19588  zringbas  19592  zringplusg  19593  zringmulg  19594  zringmulr  19595  zring0  19596  zring1  19597  zringlpirlem1  19600  zringcyg  19604  zringunit  19606  zringmpg  19607  prmirred  19610  zndvds  19665  zringnrg  22347  zlmclm  22668  lgseisenlem4  24848  zringnm  29166  zringsubgval  41999
  Copyright terms: Public domain W3C validator