Metamath Proof Explorer

Definition df-za

Description: Define an algebraic integer as a complex number which is the root of a monic integer polynomial. (Contributed by Stefan O'Rear, 30-Nov-2014)

Ref Expression
Assertion df-za 
|- _ZZ = ( IntgOver ` ZZ )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cza 
 |-  _ZZ
1 citgo 
 |-  IntgOver
2 cz 
 |-  ZZ
3 2 1 cfv 
 |-  ( IntgOver ` ZZ )
4 0 3 wceq 
 |-  _ZZ = ( IntgOver ` ZZ )