ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-zring GIF version

Definition df-zring 13707
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 czring 13706 . 2 class ring
2 ccnfld 13681 . . 3 class fld
3 cz 9266 . . 3 class
4 cress 12476 . . 3 class s
52, 3, 4co 5888 . 2 class (ℂflds ℤ)
61, 5wceq 1363 1 wff ring = (ℂflds ℤ)
Colors of variables: wff set class
This definition is referenced by:  zringcrng  13708  zringbas  13712  zringplusg  13713  zringmulg  13714  zringmulr  13715  zring0  13716  zring1  13717  zringsubgval  13721  zringmpg  13722
  Copyright terms: Public domain W3C validator