In this article we extend the algebraic theory of polynomial rings, formalized in Mizar [1], based on [2], [3]. After introducing constant and monic polynomials we present the canonical embedding of R into R[X] and deal with both unit and irreducible elements. We also define polynomial GCDs and show that for fields F and irreducible polynomials p the field F[X]/ is isomorphic to the field of polynomials with degree smaller than the one of p.
@article{bwmeta1.element.doi-10_1515_forma-2016-0019,
author = {Christoph Schwarzweller and Artur Korni\l owicz},
title = {Some Algebraic Properties of Polynomial Rings},
journal = {Formalized Mathematics},
volume = {24},
year = {2016},
pages = {227-237},
zbl = {1357.12006},
language = {en},
url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_1515_forma-2016-0019}
}
Christoph Schwarzweller; Artur Korniłowicz. Some Algebraic Properties of Polynomial Rings. Formalized Mathematics, Tome 24 (2016) pp. 227-237. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_1515_forma-2016-0019/