# mathlibdocumentation

field_theory.is_alg_closed.classification

# Classification of Algebraically closed fields #

This file contains results related to classifying algebraically closed fields.

## Main statements #

• is_alg_closed.equiv_of_transcendence_basis Two fields with the same characteristic and the same cardinality of transcendence basis are isomorphic.
• is_alg_closed.ring_equiv_of_cardinal_eq_of_char_eq Two uncountable algebraically closed fields are isomorphic if they have the same characteristic and the same cardinality.
theorem algebra.is_algebraic.cardinal_mk_le_sigma_polynomial (R L : Type u) [comm_ring R] [comm_ring L] [is_domain L] [ L] (halg : L) :
cardinal.mk (Σ (p : , {x // x (polynomial.map L) p).roots})
theorem algebra.is_algebraic.cardinal_mk_le_max (R L : Type u) [comm_ring R] [comm_ring L] [is_domain L] [ L] (halg : L) :

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

theorem is_alg_closed.is_alg_closure_of_transcendence_basis {R : Type u_1} {K : Type u_3} [comm_ring R] [field K] [ K] {ι : Type u_4} (v : ι → K) (hv : v) :
K
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] [ K] [field L] [ L] {ι : Type u_4} (v : ι → K) {κ : Type u_5} (w : κ → L) (e : ι κ) (hv : v) (hw : 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.

Equations
• hw = let _inst : K := _, _inst_8 : L := _ in
theorem is_alg_closed.cardinal_le_max_transcendence_basis {R K : Type u} [comm_ring R] [field K] [ K] {ι : Type u} (v : ι → K) (hv : v) :
theorem is_alg_closed.cardinal_eq_cardinal_transcendence_basis_of_aleph_0_lt {R K : Type u} [comm_ring R] [field K] [ K] {ι : Type u} (v : ι → K) [nontrivial R] (hv : v) (hR : cardinal.aleph_0) (hK : cardinal.aleph_0 < ) :

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

@[nolint]
noncomputable theorem is_alg_closed.ring_equiv_of_cardinal_eq_of_char_zero {K L : Type} [field K] [field L] [char_zero K] [char_zero L] (hK : cardinal.aleph_0 < ) (hKL : = ) :
K ≃+* L

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

@[nolint]
noncomputable theorem is_alg_closed.ring_equiv_of_cardinal_eq_of_char_eq {K L : Type} [field K] [field L] (p : ) [ p] [ p] (hK : cardinal.aleph_0 < ) (hKL : = ) :
K ≃+* L

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