Theorems · Theorem · field theory

IsAlgClosed.ringEquiv_of_equiv_of_char_eq

∀ {K : Type u} {L : Type v} [inst : Field K] [inst_1 : Field L] [IsAlgClosed K] [IsAlgClosed L] (p : ℕ) [CharP K p]
  [CharP L p], Cardinal.aleph0 < Cardinal.mk K → Nonempty (K ≃ L) → Nonempty (K ≃+* L)

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

Defined in

Mathlib.FieldTheory.IsAlgClosed.Classification

Cited by

1 results in Mathlib

Foundations

Depth 157 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldIsAlgClosedIsAlgClosedCharPCharP