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 20047
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 20046 . 2 class ring
2 ccnfld 19974 . . 3 class fld
3 cz 11663 . . 3 class
4 cress 16089 . . 3 class s
52, 3, 4co 6884 . 2 class (ℂflds ℤ)
61, 5wceq 1637 1 wff ring = (ℂflds ℤ)
Colors of variables: wff setvar class
This definition is referenced by:  zringcrng  20048  zringbas  20052  zringplusg  20053  zringmulg  20054  zringmulr  20055  zring0  20056  zring1  20057  zringlpirlem1  20060  zringunit  20064  zringcyg  20067  zringmpg  20068  prmirred  20071  zndvds  20125  zringnrg  22825  zlmclm  23145  zclmncvs  23181  lgseisenlem4  25340  zringnm  30352  zringsubgval  42769
  Copyright terms: Public domain W3C validator