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 20019
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 20018 . 2 class ring
2 ccnfld 19946 . . 3 class fld
3 cz 11567 . . 3 class
4 cress 16058 . . 3 class s
52, 3, 4co 6811 . 2 class (ℂflds ℤ)
61, 5wceq 1630 1 wff ring = (ℂflds ℤ)
Colors of variables: wff setvar class
This definition is referenced by:  zringcrng  20020  zringbas  20024  zringplusg  20025  zringmulg  20026  zringmulr  20027  zring0  20028  zring1  20029  zringlpirlem1  20032  zringunit  20036  zringcyg  20039  zringmpg  20040  prmirred  20043  zndvds  20098  zringnrg  22790  zlmclm  23110  zclmncvs  23146  lgseisenlem4  25300  zringnm  30311  zringsubgval  42691
  Copyright terms: Public domain W3C validator