This article provides definitions and examples upon an integral element of unital commutative rings. An algebraic number is also treated as consequence of a concept of “integral”. Definitions for an integral closure, an algebraic integer and a transcendental numbers [14], [1], [10] and [7] are included as well. As an application of an algebraic number, this article includes a formal proof of a ring extension of rational number field ℚ induced by substitution of an algebraic number to the polynomial ring of ℚ[x] turns to be a field.
@article{bwmeta1.element.doi-10_1515_forma-2016-0025,
author = {Yasushige Watase},
title = {Algebraic Numbers},
journal = {Formalized Mathematics},
volume = {24},
year = {2016},
pages = {291-299},
zbl = {1357.11107},
language = {en},
url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_1515_forma-2016-0025}
}
Yasushige Watase. Algebraic Numbers. Formalized Mathematics, Tome 24 (2016) pp. 291-299. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_1515_forma-2016-0025/