Renamings and a Condition-free Formalization of Kronecker’s Construction

[1] Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-8_17.10.1007/978-3-319-20615-8_17Search in Google Scholar

[2] Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pąk. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9–32, 2018. doi:10.1007/s10817-017-9440-6.10.1007/s10817-017-9440-6604425130069070Search in Google Scholar

[3] Nathan Jacobson. Basic Algebra I. Dover Books on Mathematics, 1985.Search in Google Scholar

[4] Artur Korniłowicz. Quotient rings. Formalized Mathematics, 13(4):573–576, 2005.Search in Google Scholar

[5] Heinz Lüneburg. Gruppen, Ringe, Körper: Die grundlegenden Strukturen der Algebra. Oldenbourg Verlag, 1999.10.1524/9783486599022Search in Google Scholar

[6] Knut Radbruch. Algebra I. Lecture Notes, University of Kaiserslautern, Germany, 1991.Search in Google Scholar

[7] Christoph Schwarzweller. On roots of polynomials over F [X]/ 〈 p〉. Formalized Mathematics, 27(2):93–100, 2019. doi:10.2478/forma-2019-0010.10.2478/forma-2019-0010Search in Google Scholar

[8] Christoph Schwarzweller. On monomorphisms and subfields. Formalized Mathematics, 27(2):133–137, 2019. doi:10.2478/forma-2019-0014.10.2478/forma-2019-0014Search in Google Scholar

[9] Christoph Schwarzweller. Field extensions and Kronecker’s construction. Formalized Mathematics, 27(3):229–235, 2019. doi:10.2478/forma-2019-0022.10.2478/forma-2019-0022Search in Google Scholar

[10] Christoph Schwarzweller. Representation matters: An unexpected property of polynomial rings and its consequences for formalizing abstract field theory. In M. Ganzha, L. Maciaszek, and M. Paprzycki, editors, Proceedings of the 2018 Federated Conference on Computer Science and Information Systems, volume 15 of Annals of Computer Science and Information Systems, pages 67–72. IEEE, 2018. doi:10.15439/2018F88.10.15439/2018F88Search in Google Scholar