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 = IntgOver

Detailed syntax breakdown

Step Hyp Ref Expression
0 cza class
1 citgo class IntgOver
2 cz class
3 2 1 cfv class IntgOver
4 0 3 wceq wff = IntgOver