![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-zring | Structured version Visualization version 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 21429 | . 2 class ℤring | |
2 | ccnfld 21336 | . . 3 class ℂfld | |
3 | cz 12601 | . . 3 class ℤ | |
4 | cress 17234 | . . 3 class ↾s | |
5 | 2, 3, 4 | co 7413 | . 2 class (ℂfld ↾s ℤ) |
6 | 1, 5 | wceq 1534 | 1 wff ℤring = (ℂfld ↾s ℤ) |
Colors of variables: wff setvar class |
This definition is referenced by: zringcrng 21431 zringbas 21436 zringplusg 21437 zringsub 21438 zringmulg 21439 zringmulr 21440 zring0 21441 zring1 21442 zringlpirlem1 21445 zringunit 21449 zringcyg 21452 zringsubgval 21453 zringmpg 21454 prmirred 21457 zndvds 21540 zringnrg 24789 zlmclm 25124 zclmncvs 25161 lgseisenlem4 27401 zringnm 33783 |
Copyright terms: Public domain | W3C validator |