English
Two uncountable algebraically closed fields with the same characteristic p are isomorphic; the characteristic p case reduces to ringEquiv_of_equiv_of_charP or to char zero case.
Русский
Два невычислимых алгебраически замкнутых поля с одинаковой характеристикой p изоморфны; случай p сводится к соответствующему результату.
LaTeX
$$IsAlgClosed.ringEquiv_of_equiv_of_char_eq p hK hKL$$
Lean4
/-- Two uncountable algebraically closed fields are isomorphic
if they have the same cardinality and the same characteristic. -/
theorem ringEquiv_of_equiv_of_char_eq (p : ℕ) [CharP K p] [CharP L p] (hK : ℵ₀ < #K) (hKL : Nonempty (K ≃ L)) :
Nonempty (K ≃+* L) := by
rcases CharP.char_is_prime_or_zero K p with (hp | hp)
· haveI : Fact p.Prime := ⟨hp⟩
exact ringEquiv_of_Cardinal_eq_of_charP p hK hKL
· simp only [hp] at *
letI : CharZero K := CharP.charP_to_charZero K
letI : CharZero L := CharP.charP_to_charZero L
exact ringEquiv_of_equiv_of_charZero hK hKL
