![]() |
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 13706 | . 2 class ℤring | |
2 | ccnfld 13681 | . . 3 class ℂfld | |
3 | cz 9266 | . . 3 class ℤ | |
4 | cress 12476 | . . 3 class ↾s | |
5 | 2, 3, 4 | co 5888 | . 2 class (ℂfld ↾s ℤ) |
6 | 1, 5 | wceq 1363 | 1 wff ℤring = (ℂfld ↾s ℤ) |
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 |