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	$$⊢\bar{\mathbb{Z}}=\mathrm{IntgOver}\left(\mathbb{Z}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cza	$$class\bar{\mathbb{Z}}$$
1		citgo	$$class\mathrm{IntgOver}$$
2		cz	$$class\mathbb{Z}$$
3	2 1	cfv	$$class\mathrm{IntgOver}\left(\mathbb{Z}\right)$$
4	0 3	wceq	$$wff\bar{\mathbb{Z}}=\mathrm{IntgOver}\left(\mathbb{Z}\right)$$