English
If K is an algebraically closed field, then K is infinite.
Русский
Если K — алгебраически замкнутое поле, то K бесконечно.
LaTeX
$$$\forall K [\mathrm{Field\;K}] [IsAlgClosed\;K],\; \mathrm{Infinite}\;K$$$
Lean4
/-- Algebraically closed fields are infinite since `Xⁿ⁺¹ - 1` is separable when `#K = n` -/
instance (priority := 500) {K : Type*} [Field K] [IsAlgClosed K] : Infinite K :=
by
apply Infinite.of_not_fintype
intro hfin
set n := Fintype.card K
set f := (X : K[X]) ^ (n + 1) - 1
have hfsep : Separable f := separable_X_pow_sub_C 1 (by simp [n]) one_ne_zero
apply Nat.not_succ_le_self (Fintype.card K)
have hroot : n.succ = Fintype.card (f.rootSet K) :=
by
rw [card_rootSet_eq_natDegree hfsep (IsAlgClosed.splits_domain _)]
unfold f
rw [← C_1, natDegree_X_pow_sub_C]
rw [hroot]
exact Fintype.card_le_of_injective _ Subtype.coe_injective
