Renamings and a condition-free formalization of Kronecker's construction

DOI10.2478/FORMA-2020-0012MaRDI QIDQ2113831zbMATH OpenOpenAlexFDO

Authors Christoph Schwarzweller

Publication date 14 March 2022

Published in Formalized Mathematics (Search for Journal in Brave)

Copyright license Creative Commons Attribution-ShareAlike 4.0 International

Full work available at URL https://doi.org/10.2478/forma-2020-0012

zbMATH Keywords

field extensionsroots of polynomialsKronecker's construction

Mathematics Subject Classification ID

Polynomials in general fields (irreducibility, etc.) (12E05) Algebraic field extensions (12F05) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Field extensions and Kronecker's construction
• On roots of polynomials over \(F[X]/

  \)

• On the intersection of fields \(F\) with \(F[X]\)
• On monomorphisms and subfields
• Ring and field adjunctions, algebraic elements and minimal polynomials

Cites work

• scientific article; zbMATH DE number 3887879 (Why is no real title available?)
• scientific article; zbMATH DE number 1301895 (Why is no real title available?)
• Field extensions and Kronecker's construction
• Mizar: state-of-the-art and beyond
• On monomorphisms and subfields
• On roots of polynomials over \(F[X]/

  \)

• The role of the Mizar mathematical library for interactive proof development in Mizar

Cited in

(5)

• Introduction to algebraic geometry
• Simple extensions
• Splitting fields for the rational polynomials \(X^2 -2\), \(X^2+X+1\), \(X^3 -1\), and \(X^3 -2\)
• The divergence of the sum of prime reciprocals
• Ring and field adjunctions, algebraic elements and minimal polynomials

Describes a project that uses

Uses Software

• Mizar

This page was built for publication: Renamings and a condition-free formalization of Kronecker's construction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2113831)