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

Definition df-zring 13857
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 13856 . 2 class ring
2 ccnfld 13831 . . 3 class fld
3 cz 9272 . . 3 class
4 cress 12487 . . 3 class s
52, 3, 4co 5891 . 2 class (ℂflds ℤ)
61, 5wceq 1364 1 wff ring = (ℂflds ℤ)
Colors of variables: wff set class
This definition is referenced by:  zringcrng  13858  zringbas  13862  zringplusg  13863  zringmulg  13864  zringmulr  13865  zring0  13866  zring1  13867  zringsubgval  13871  zringmpg  13872
  Copyright terms: Public domain W3C validator