Classification of Algebraically closed fields #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file contains results related to classifying algebraically closed fields.
Main statements #
The cardinality of an algebraic extension is at most the maximum of the cardinality
of the base ring or
R to be
zmod (ring_char R) this result shows that if two algebraically
closed fields have equipotent transcendence bases and the same characteristic then they are
K is an uncountable algebraically closed field, then its
cardinality is the same as that of a transcendence basis.
Two uncountable algebraically closed fields of characteristic zero are isomorphic
if they have the same cardinality.
Two uncountable algebraically closed fields are isomorphic
if they have the same cardinality and the same characteristic.