![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-zring | GIF version |
Description: The (unital) ring of integers. (Contributed by Alexander van der Vekens, 9-Jun-2019.) |
Ref | Expression |
---|---|
df-zring | ⊢ ℤring = (ℂfld ↾s ℤ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | czring 13856 | . 2 class ℤring | |
2 | ccnfld 13831 | . . 3 class ℂfld | |
3 | cz 9272 | . . 3 class ℤ | |
4 | cress 12487 | . . 3 class ↾s | |
5 | 2, 3, 4 | co 5891 | . 2 class (ℂfld ↾s ℤ) |
6 | 1, 5 | wceq 1364 | 1 wff ℤring = (ℂfld ↾s ℤ) |
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 |