# Documentation

Mathlib.FieldTheory.IsAlgClosed.Classification

# Classification of Algebraically closed fields #

This file contains results related to classifying algebraically closed fields.

## Main statements #

• IsAlgClosed.equivOfTranscendenceBasis Two algebraically closed fields with the same characteristic and the same cardinality of transcendence basis are isomorphic.
• IsAlgClosed.ringEquivOfCardinalEqOfCharEq Two uncountable algebraically closed fields are isomorphic if they have the same characteristic and the same cardinality.
theorem Algebra.IsAlgebraic.cardinal_mk_le_sigma_polynomial (R : Type u) (L : Type u) [] [] [] [Algebra R L] [] (halg : ) :
Cardinal.mk ((p : ) × { x // x })
theorem Algebra.IsAlgebraic.cardinal_mk_le_max (R : Type u) (L : Type u) [] [] [] [Algebra R L] [] (halg : ) :

The cardinality of an algebraic extension is at most the maximum of the cardinality of the base ring or ℵ₀

theorem IsAlgClosed.isAlgClosure_of_transcendence_basis {R : Type u_1} {K : Type u_3} [] [] [Algebra R K] {ι : Type u_4} (v : ιK) [] (hv : ) :
IsAlgClosure { x // x } K
def IsAlgClosed.equivOfTranscendenceBasis {R : Type u_1} {L : Type u_2} {K : Type u_3} [] [] [Algebra R K] [] [Algebra R L] {ι : Type u_4} (v : ιK) {κ : Type u_5} (w : κL) [] [] (e : ι κ) (hv : ) (hw : ) :
K ≃+* L

setting R to be ZMod (ringChar R) this result shows that if two algebraically closed fields have equipotent transcendence bases and the same characteristic then they are isomorphic.

Instances For
theorem IsAlgClosed.cardinal_le_max_transcendence_basis {R : Type u} {K : Type u} [] [] [Algebra R K] [] {ι : Type u} (v : ιK) (hv : ) :
theorem IsAlgClosed.cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt {R : Type u} {K : Type u} [] [] [Algebra R K] [] {ι : Type u} (v : ιK) [] (hv : ) (hR : ) (hK : ) :

If K is an uncountable algebraically closed field, then its cardinality is the same as that of a transcendence basis.

theorem IsAlgClosed.ringEquivOfCardinalEqOfCharZero {K : Type} {L : Type} [] [] [] [] [] [] (hK : ) (hKL : ) :

Two uncountable algebraically closed fields of characteristic zero are isomorphic if they have the same cardinality.

theorem IsAlgClosed.ringEquivOfCardinalEqOfCharEq {K : Type} {L : Type} [] [] [] [] (p : ) [CharP K p] [CharP L p] (hK : ) (hKL : ) :

Two uncountable algebraically closed fields are isomorphic if they have the same cardinality and the same characteristic.