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
_version_ 1783551866865451008
author de Vilhena, Paulo Emílio
Paulson, Lawrence C.
author_facet de Vilhena, Paulo Emílio
Paulson, Lawrence C.
author_sort de Vilhena, Paulo Emílio
collection PubMed
description 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.
format Online
Article
Text
id pubmed-7324028
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-73240282020-06-30 Algebraically Closed Fields in Isabelle/HOL de Vilhena, Paulo Emílio Paulson, Lawrence C. Automated Reasoning Article 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. 2020-06-06 /pmc/articles/PMC7324028/ http://dx.doi.org/10.1007/978-3-030-51054-1_12 Text en © Springer Nature Switzerland AG 2020 This article is made available via the PMC Open Access Subset for unrestricted research re-use and secondary analysis in any form or by any means with acknowledgement of the original source. These permissions are granted for the duration of the World Health Organization (WHO) declaration of COVID-19 as a global pandemic.
spellingShingle Article
de Vilhena, Paulo Emílio
Paulson, Lawrence C.
Algebraically Closed Fields in Isabelle/HOL
title Algebraically Closed Fields in Isabelle/HOL
title_full Algebraically Closed Fields in Isabelle/HOL
title_fullStr Algebraically Closed Fields in Isabelle/HOL
title_full_unstemmed Algebraically Closed Fields in Isabelle/HOL
title_short Algebraically Closed Fields in Isabelle/HOL
title_sort algebraically closed fields in isabelle/hol
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7324028/
http://dx.doi.org/10.1007/978-3-030-51054-1_12
work_keys_str_mv AT devilhenapauloemilio algebraicallyclosedfieldsinisabellehol
AT paulsonlawrencec algebraicallyclosedfieldsinisabellehol

Ejemplares similares