English
There is an equivalence between the primitive element condition and the degree equality between the minimal polynomial and the extension degree: F⟮α⟯ = ⊤ iff minpoly F α has degree equal to finrank F E.
Русский
Условие примитивного элемента эквивалентно тому, что степень минимального многочлена α равна размерности расширения E над F.
LaTeX
$$$\operatorname{primitive\ element\ degree\ equality}:\ (F\langle \alpha\rangle = \top) \iff (\deg\ minpoly F \alpha) = \operatorname{finrank} F E$$$
Lean4
@[simp]
theorem card (K : Type*) [Field K] [IsAlgClosed K] [Algebra F K] : Fintype.card (E →ₐ[F] K) = finrank F E :=
AlgHom.card_of_splits _ _ _ (fun _ ↦ IsAlgClosed.splits_codomain _)
