Definition df-za 44256

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.)

Assertion

Ref	Expression
df-za	⊢ ℤ = (IntgOver‘ℤ)

Detailed syntax breakdown of Definition df-za

Step	Hyp	Ref	Expression
1		cza 44254	. 2 class ℤ
2		cz 12697	. . 3 class ℤ
3		citgo 44253	. . 3 class IntgOver
4	2, 3	cfv 6539	. 2 class (IntgOver‘ℤ)
5	1, 4	wceq 1569	1 wff ℤ = (IntgOver‘ℤ)

This definition is used by: (None)