mathlib3 documentation


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 ℵ₀

noncomputable def is_alg_closed.equiv_of_transcendence_basis {R : Type u_1} {L : Type u_2} {K : Type u_3} [comm_ring R] [field K] [algebra R K] [field L] [algebra R L] {ι : Type u_4} (v : ι K) {κ : Type u_5} (w : κ L) [is_alg_closed K] [is_alg_closed L] (e : ι κ) (hv : is_transcendence_basis R v) (hw : is_transcendence_basis R w) :
K ≃+* L

setting 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 isomorphic.


If 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.