Algebraically Closed Fields in Isabelle/HOL

A fundamental theorem states that every field admits an algebraically closed extension. Despite its central importance, this theorem has never before been formalised in a proof assistant. We fill this gap by documenting its formalisation in Isabelle/HOL, describing the difficulties that impeded this...

Descripción completa

Detalles Bibliográficos
Autores principales: de Vilhena, Paulo Emílio, Paulson, Lawrence C.
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Article
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324028/
http://dx.doi.org/10.1007/978-3-030-51054-1_12
Descripción
Sumario:A fundamental theorem states that every field admits an algebraically closed extension. Despite its central importance, this theorem has never before been formalised in a proof assistant. We fill this gap by documenting its formalisation in Isabelle/HOL, describing the difficulties that impeded this development and their solutions.

Ejemplares similares